Merge pull request #13 from HEPLean/Flavor/CKM
feat (flavor physics): CKM matrix
This commit is contained in:
Joseph Tooby-Smith
GitHub
commit
cee60826d5
8 changed files with 2503 additions and 0 deletions
|
|
@ -47,3 +47,10 @@ import HepLean.AnomalyCancellation.SMNu.PlusU1.HyperCharge
|
|||
import HepLean.AnomalyCancellation.SMNu.PlusU1.PlaneNonSols
|
||||
import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSol
|
||||
import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSolToSol
|
||||
import HepLean.FlavorPhysics.CKMMatrix.Basic
|
||||
import HepLean.FlavorPhysics.CKMMatrix.Invariants
|
||||
import HepLean.FlavorPhysics.CKMMatrix.PhaseFreedom
|
||||
import HepLean.FlavorPhysics.CKMMatrix.Relations
|
||||
import HepLean.FlavorPhysics.CKMMatrix.Rows
|
||||
import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
|
||||
import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters
|
||||
|
|
|
|||
400
HepLean/FlavorPhysics/CKMMatrix/Basic.lean
Normal file
400
HepLean/FlavorPhysics/CKMMatrix/Basic.lean
Normal file
|
|
@ -0,0 +1,400 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import Mathlib.LinearAlgebra.UnitaryGroup
|
||||
import Mathlib.Data.Complex.Exponential
|
||||
import Mathlib.Tactic.Polyrith
|
||||
/-!
|
||||
# The CKM Matrix
|
||||
|
||||
The definition of the type of CKM matries as unitary $3×3$-matries.
|
||||
|
||||
An equivalence relation on CKM matrices is defined, where two matrices are equivalent if they are
|
||||
related by phase shifts.
|
||||
|
||||
The notation `[V]ud` etc can be used for the elements of a CKM matrix, and
|
||||
`[V]ud|us` etc for the ratios of elements.
|
||||
|
||||
|
||||
-/
|
||||
|
||||
open Matrix Complex
|
||||
|
||||
|
||||
noncomputable section
|
||||
|
||||
/-- Given three real numbers `a b c` the complex matrix with `exp (I * a)` etc on the
|
||||
leading diagonal. -/
|
||||
@[simp]
|
||||
def phaseShiftMatrix (a b c : ℝ) : Matrix (Fin 3) (Fin 3) ℂ :=
|
||||
![![cexp (I * a), 0, 0], ![0, cexp (I * b), 0], ![0, 0, cexp (I * c)]]
|
||||
|
||||
lemma phaseShiftMatrix_one : phaseShiftMatrix 0 0 0 = 1 := by
|
||||
ext i j
|
||||
fin_cases i <;> fin_cases j <;>
|
||||
simp [Matrix.one_apply, phaseShiftMatrix]
|
||||
rfl
|
||||
|
||||
lemma phaseShiftMatrix_star (a b c : ℝ) :
|
||||
(phaseShiftMatrix a b c)ᴴ = phaseShiftMatrix (- a) (- b) (- c) := by
|
||||
funext i j
|
||||
fin_cases i <;> fin_cases j <;>
|
||||
simp [← exp_conj, conj_ofReal]
|
||||
rfl
|
||||
rfl
|
||||
|
||||
lemma phaseShiftMatrix_mul (a b c d e f : ℝ) :
|
||||
phaseShiftMatrix a b c * phaseShiftMatrix d e f = phaseShiftMatrix (a + d) (b + e) (c + f) := by
|
||||
ext i j
|
||||
fin_cases i <;> fin_cases j <;>
|
||||
simp [Matrix.mul_apply, Fin.sum_univ_three]
|
||||
any_goals rw [mul_add, exp_add]
|
||||
change cexp (I * ↑c) * 0 = 0
|
||||
simp
|
||||
|
||||
/-- Given three real numbers `a b c` the unitary matrix with `exp (I * a)` etc on the
|
||||
leading diagonal. -/
|
||||
@[simps!]
|
||||
def phaseShift (a b c : ℝ) : unitaryGroup (Fin 3) ℂ :=
|
||||
⟨phaseShiftMatrix a b c,
|
||||
by
|
||||
rw [mem_unitaryGroup_iff]
|
||||
change _ * (phaseShiftMatrix a b c)ᴴ = 1
|
||||
rw [phaseShiftMatrix_star, phaseShiftMatrix_mul, ← phaseShiftMatrix_one]
|
||||
simp only [phaseShiftMatrix, add_right_neg, ofReal_zero, mul_zero, exp_zero]⟩
|
||||
|
||||
lemma phaseShift_coe_matrix (a b c : ℝ) : ↑(phaseShift a b c) = phaseShiftMatrix a b c := rfl
|
||||
|
||||
/-- The equivalence relation between CKM matrices. -/
|
||||
def phaseShiftRelation (U V : unitaryGroup (Fin 3) ℂ) : Prop :=
|
||||
∃ a b c e f g , U = phaseShift a b c * V * phaseShift e f g
|
||||
|
||||
lemma phaseShiftRelation_refl (U : unitaryGroup (Fin 3) ℂ) : phaseShiftRelation U U := by
|
||||
use 0, 0, 0, 0, 0, 0
|
||||
rw [Subtype.ext_iff_val]
|
||||
simp only [Submonoid.coe_mul, phaseShift_coe_matrix, ofReal_zero, mul_zero, exp_zero]
|
||||
rw [phaseShiftMatrix_one]
|
||||
simp only [one_mul, mul_one]
|
||||
|
||||
lemma phaseShiftRelation_symm {U V : unitaryGroup (Fin 3) ℂ} :
|
||||
phaseShiftRelation U V → phaseShiftRelation V U := by
|
||||
intro h
|
||||
obtain ⟨a, b, c, e, f, g, h⟩ := h
|
||||
use (- a), (- b), (- c), (- e), (- f), (- g)
|
||||
rw [Subtype.ext_iff_val]
|
||||
rw [h]
|
||||
repeat rw [mul_assoc]
|
||||
simp only [Submonoid.coe_mul, phaseShift_coe_matrix, ofReal_neg, mul_neg]
|
||||
rw [phaseShiftMatrix_mul]
|
||||
repeat rw [← mul_assoc]
|
||||
simp only [phaseShiftMatrix_mul, add_left_neg, phaseShiftMatrix_one, one_mul, add_right_neg,
|
||||
mul_one]
|
||||
|
||||
lemma phaseShiftRelation_trans {U V W : unitaryGroup (Fin 3) ℂ} :
|
||||
phaseShiftRelation U V → phaseShiftRelation V W → phaseShiftRelation U W := by
|
||||
intro hUV hVW
|
||||
obtain ⟨a, b, c, e, f, g, hUV⟩ := hUV
|
||||
obtain ⟨d, i, j, k, l, m, hVW⟩ := hVW
|
||||
use (a + d), (b + i), (c + j), (e + k), (f + l), (g + m)
|
||||
rw [Subtype.ext_iff_val]
|
||||
rw [hUV, hVW]
|
||||
simp only [Submonoid.coe_mul, phaseShift_coe_matrix]
|
||||
repeat rw [mul_assoc]
|
||||
rw [phaseShiftMatrix_mul]
|
||||
repeat rw [← mul_assoc]
|
||||
rw [phaseShiftMatrix_mul]
|
||||
rw [add_comm k e, add_comm l f, add_comm m g]
|
||||
|
||||
|
||||
lemma phaseShiftEquivRelation : Equivalence phaseShiftRelation where
|
||||
refl := phaseShiftRelation_refl
|
||||
symm := phaseShiftRelation_symm
|
||||
trans := phaseShiftRelation_trans
|
||||
|
||||
/-- The type of CKM matrices. -/
|
||||
def CKMMatrix : Type := unitaryGroup (Fin 3) ℂ
|
||||
|
||||
lemma CKMMatrix_ext {U V : CKMMatrix} (h : U.val = V.val) : U = V := by
|
||||
cases U; cases V
|
||||
simp at h
|
||||
subst h
|
||||
rfl
|
||||
|
||||
/-- The `ud`th element of the CKM matrix. -/
|
||||
scoped[CKMMatrix] notation (name := ud_element) "[" V "]ud" => V.1 0 0
|
||||
|
||||
/-- The `us`th element of the CKM matrix. -/
|
||||
scoped[CKMMatrix] notation (name := us_element) "[" V "]us" => V.1 0 1
|
||||
|
||||
/-- The `ub`th element of the CKM matrix. -/
|
||||
scoped[CKMMatrix] notation (name := ub_element) "[" V "]ub" => V.1 0 2
|
||||
|
||||
/-- The `cd`th element of the CKM matrix. -/
|
||||
scoped[CKMMatrix] notation (name := cd_element) "[" V "]cd" => V.1 1 0
|
||||
|
||||
/-- The `cs`th element of the CKM matrix. -/
|
||||
scoped[CKMMatrix] notation (name := cs_element) "[" V "]cs" => V.1 1 1
|
||||
|
||||
/-- The `cb`th element of the CKM matrix. -/
|
||||
scoped[CKMMatrix] notation (name := cb_element) "[" V "]cb" => V.1 1 2
|
||||
|
||||
/-- The `td`th element of the CKM matrix. -/
|
||||
scoped[CKMMatrix] notation (name := td_element) "[" V "]td" => V.1 2 0
|
||||
|
||||
/-- The `ts`th element of the CKM matrix. -/
|
||||
scoped[CKMMatrix] notation (name := ts_element) "[" V "]ts" => V.1 2 1
|
||||
|
||||
/-- The `tb`th element of the CKM matrix. -/
|
||||
scoped[CKMMatrix] notation (name := tb_element) "[" V "]tb" => V.1 2 2
|
||||
|
||||
instance CKMMatrixSetoid : Setoid CKMMatrix := ⟨phaseShiftRelation, phaseShiftEquivRelation⟩
|
||||
|
||||
/-- The matrix obtained from `V` by shifting the phases of the fermions. -/
|
||||
@[simps!]
|
||||
def phaseShiftApply (V : CKMMatrix) (a b c d e f : ℝ) : CKMMatrix :=
|
||||
phaseShift a b c * ↑V * phaseShift d e f
|
||||
|
||||
namespace phaseShiftApply
|
||||
lemma equiv (V : CKMMatrix) (a b c d e f : ℝ) :
|
||||
V ≈ phaseShiftApply V a b c d e f := by
|
||||
symm
|
||||
use a, b, c, d, e, f
|
||||
rfl
|
||||
|
||||
lemma ud (V : CKMMatrix) (a b c d e f : ℝ) :
|
||||
(phaseShiftApply V a b c d e f).1 0 0 = cexp (a * I + d * I) * V.1 0 0 := by
|
||||
simp only [Fin.isValue, phaseShiftApply_coe]
|
||||
rw [mul_apply, Fin.sum_univ_three]
|
||||
rw [mul_apply, mul_apply, mul_apply, Fin.sum_univ_three, Fin.sum_univ_three, Fin.sum_univ_three]
|
||||
simp only [Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one, vecCons_const,
|
||||
cons_val_one, head_cons, zero_mul, add_zero, cons_val_two, tail_cons, head_fin_const, mul_zero,
|
||||
tail_val', head_val']
|
||||
change _ + _ * _ * 0 = _
|
||||
rw [exp_add]
|
||||
ring_nf
|
||||
|
||||
lemma us (V : CKMMatrix) (a b c d e f : ℝ) :
|
||||
(phaseShiftApply V a b c d e f).1 0 1 = cexp (a * I + e * I) * V.1 0 1 := by
|
||||
simp only [Fin.isValue, phaseShiftApply_coe]
|
||||
rw [mul_apply, Fin.sum_univ_three]
|
||||
rw [mul_apply, mul_apply, mul_apply, Fin.sum_univ_three, Fin.sum_univ_three, Fin.sum_univ_three]
|
||||
simp only [Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one, vecCons_const,
|
||||
cons_val_one, head_cons, zero_mul, add_zero, cons_val_two, tail_cons, mul_zero, zero_add,
|
||||
head_fin_const]
|
||||
rw [exp_add]
|
||||
ring_nf
|
||||
|
||||
lemma ub (V : CKMMatrix) (a b c d e f : ℝ) :
|
||||
(phaseShiftApply V a b c d e f).1 0 2 = cexp (a * I + f * I) * V.1 0 2 := by
|
||||
simp only [Fin.isValue, phaseShiftApply_coe]
|
||||
rw [mul_apply, Fin.sum_univ_three]
|
||||
rw [mul_apply, mul_apply, mul_apply, Fin.sum_univ_three, Fin.sum_univ_three, Fin.sum_univ_three]
|
||||
simp only [Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one, vecCons_const,
|
||||
cons_val_one, head_cons, zero_mul, add_zero, cons_val_two, tail_cons, mul_zero, head_fin_const,
|
||||
zero_add]
|
||||
rw [exp_add]
|
||||
ring_nf
|
||||
|
||||
lemma cd (V : CKMMatrix) (a b c d e f : ℝ) :
|
||||
(phaseShiftApply V a b c d e f).1 1 0= cexp (b * I + d * I) * V.1 1 0 := by
|
||||
simp only [Fin.isValue, phaseShiftApply_coe]
|
||||
rw [mul_apply, Fin.sum_univ_three]
|
||||
rw [mul_apply, mul_apply, mul_apply, Fin.sum_univ_three, Fin.sum_univ_three, Fin.sum_univ_three]
|
||||
simp only [Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one, vecCons_const,
|
||||
cons_val_one, head_fin_const, zero_mul, head_cons, zero_add, cons_val_two, tail_cons, add_zero,
|
||||
mul_zero, tail_val', head_val']
|
||||
change _ + _ * _ * 0 = _
|
||||
rw [exp_add]
|
||||
ring_nf
|
||||
|
||||
lemma cs (V : CKMMatrix) (a b c d e f : ℝ) :
|
||||
(phaseShiftApply V a b c d e f).1 1 1 = cexp (b * I + e * I) * V.1 1 1 := by
|
||||
simp only [Fin.isValue, phaseShiftApply_coe]
|
||||
rw [mul_apply, Fin.sum_univ_three]
|
||||
rw [mul_apply, mul_apply, mul_apply, Fin.sum_univ_three, Fin.sum_univ_three, Fin.sum_univ_three]
|
||||
simp only [Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one, vecCons_const,
|
||||
cons_val_one, head_fin_const, zero_mul, head_cons, zero_add, cons_val_two, tail_cons, add_zero,
|
||||
mul_zero]
|
||||
rw [exp_add]
|
||||
ring_nf
|
||||
|
||||
lemma cb (V : CKMMatrix) (a b c d e f : ℝ) :
|
||||
(phaseShiftApply V a b c d e f).1 1 2 = cexp (b * I + f * I) * V.1 1 2 := by
|
||||
simp only [Fin.isValue, phaseShiftApply_coe]
|
||||
rw [mul_apply, Fin.sum_univ_three]
|
||||
rw [mul_apply, mul_apply, mul_apply, Fin.sum_univ_three, Fin.sum_univ_three, Fin.sum_univ_three]
|
||||
simp only [Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one, vecCons_const,
|
||||
cons_val_one, head_fin_const, zero_mul, head_cons, zero_add, cons_val_two, tail_cons, add_zero,
|
||||
mul_zero]
|
||||
rw [exp_add]
|
||||
ring_nf
|
||||
|
||||
lemma td (V : CKMMatrix) (a b c d e f : ℝ) :
|
||||
(phaseShiftApply V a b c d e f).1 2 0= cexp (c * I + d * I) * V.1 2 0 := by
|
||||
simp only [Fin.isValue, phaseShiftApply_coe]
|
||||
rw [mul_apply, Fin.sum_univ_three]
|
||||
rw [mul_apply, mul_apply, mul_apply, Fin.sum_univ_three, Fin.sum_univ_three, Fin.sum_univ_three]
|
||||
simp only [Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one, vecCons_const,
|
||||
cons_val_two, tail_val', head_val', cons_val_one, head_cons, tail_cons, head_fin_const,
|
||||
zero_mul, add_zero, mul_zero]
|
||||
change (0 * _ + _ ) * _ + (0 * _ + _ ) * 0 = _
|
||||
simp only [Fin.isValue, zero_mul, zero_add, mul_zero, add_zero]
|
||||
rw [exp_add]
|
||||
ring_nf
|
||||
|
||||
lemma ts (V : CKMMatrix) (a b c d e f : ℝ) :
|
||||
(phaseShiftApply V a b c d e f).1 2 1 = cexp (c * I + e * I) * V.1 2 1 := by
|
||||
simp only [Fin.isValue, phaseShiftApply_coe]
|
||||
rw [mul_apply, Fin.sum_univ_three]
|
||||
rw [mul_apply, mul_apply, mul_apply, Fin.sum_univ_three, Fin.sum_univ_three, Fin.sum_univ_three]
|
||||
simp only [Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one, vecCons_const,
|
||||
cons_val_two, tail_val', head_val', cons_val_one, head_cons, tail_cons, head_fin_const,
|
||||
zero_mul, add_zero, mul_zero, zero_add]
|
||||
change (0 * _ + _) * _ = _
|
||||
rw [exp_add]
|
||||
ring_nf
|
||||
|
||||
lemma tb (V : CKMMatrix) (a b c d e f : ℝ) :
|
||||
(phaseShiftApply V a b c d e f).1 2 2 = cexp (c * I + f * I) * V.1 2 2 := by
|
||||
simp only [Fin.isValue, phaseShiftApply_coe]
|
||||
rw [mul_apply, Fin.sum_univ_three]
|
||||
rw [mul_apply, mul_apply, mul_apply, Fin.sum_univ_three, Fin.sum_univ_three, Fin.sum_univ_three]
|
||||
simp only [Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one, vecCons_const,
|
||||
cons_val_two, tail_val', head_val', cons_val_one, head_cons, tail_cons, head_fin_const,
|
||||
zero_mul, add_zero, mul_zero, zero_add]
|
||||
change (0 * _ + _) * _ = _
|
||||
rw [exp_add]
|
||||
ring_nf
|
||||
|
||||
end phaseShiftApply
|
||||
|
||||
|
||||
/-- The aboslute value of the `(i,j)`th element of `V`. -/
|
||||
@[simp]
|
||||
def VAbs' (V : unitaryGroup (Fin 3) ℂ) (i j : Fin 3) : ℝ := Complex.abs (V i j)
|
||||
|
||||
lemma VAbs'_equiv (i j : Fin 3) (V U : CKMMatrix) (h : V ≈ U) :
|
||||
VAbs' V i j = VAbs' U i j := by
|
||||
simp only [VAbs']
|
||||
obtain ⟨a, b, c, e, f, g, h⟩ := h
|
||||
rw [h]
|
||||
simp only [Submonoid.coe_mul, phaseShift_coe_matrix]
|
||||
rw [mul_apply, Fin.sum_univ_three]
|
||||
rw [mul_apply, Fin.sum_univ_three]
|
||||
rw [mul_apply, mul_apply, Fin.sum_univ_three, Fin.sum_univ_three]
|
||||
simp only [phaseShiftMatrix, Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one,
|
||||
vecCons_const, cons_val_one, head_cons, zero_mul, add_zero, cons_val_two, tail_cons,
|
||||
head_fin_const, mul_zero]
|
||||
fin_cases i <;> fin_cases j <;>
|
||||
simp [Complex.abs_exp]
|
||||
all_goals change Complex.abs (0 * _ + _) = _
|
||||
all_goals simp [Complex.abs_exp]
|
||||
|
||||
/-- The absolute value of the `(i,j)`th any representative of `⟦V⟧`. -/
|
||||
def VAbs (i j : Fin 3) : Quotient CKMMatrixSetoid → ℝ :=
|
||||
Quotient.lift (fun V => VAbs' V i j) (VAbs'_equiv i j)
|
||||
|
||||
/-- The absolute value of the `ud`th element of a representative of an equivalence class of
|
||||
CKM matrices. -/
|
||||
@[simp]
|
||||
abbrev VudAbs := VAbs 0 0
|
||||
|
||||
/-- The absolute value of the `us`th element of a representative of an equivalence class of
|
||||
CKM matrices. -/
|
||||
@[simp]
|
||||
abbrev VusAbs := VAbs 0 1
|
||||
|
||||
/-- The absolute value of the `ub`th element of a representative of an equivalence class of
|
||||
CKM matrices. -/
|
||||
@[simp]
|
||||
abbrev VubAbs := VAbs 0 2
|
||||
|
||||
/-- The absolute value of the `cd`th element of a representative of an equivalence class of
|
||||
CKM matrices. -/
|
||||
@[simp]
|
||||
abbrev VcdAbs := VAbs 1 0
|
||||
|
||||
/-- The absolute value of the `cs`th element of a representative of an equivalence class of
|
||||
CKM matrices. -/
|
||||
@[simp]
|
||||
abbrev VcsAbs := VAbs 1 1
|
||||
|
||||
/-- The absolute value of the `cb`th element of a representative of an equivalence class of
|
||||
CKM matrices. -/
|
||||
@[simp]
|
||||
abbrev VcbAbs := VAbs 1 2
|
||||
|
||||
/-- The absolute value of the `td`th element of a representative of an equivalence class of
|
||||
CKM matrices. -/
|
||||
@[simp]
|
||||
abbrev VtdAbs := VAbs 2 0
|
||||
|
||||
/-- The absolute value of the `ts`th element of a representative of an equivalence class of
|
||||
CKM matrices. -/
|
||||
@[simp]
|
||||
abbrev VtsAbs := VAbs 2 1
|
||||
|
||||
/-- The absolute value of the `tb`th element of a representative of an equivalence class of
|
||||
CKM matrices. -/
|
||||
@[simp]
|
||||
abbrev VtbAbs := VAbs 2 2
|
||||
|
||||
|
||||
namespace CKMMatrix
|
||||
open ComplexConjugate
|
||||
|
||||
|
||||
section ratios
|
||||
|
||||
/-- The ratio of the `ub` and `ud` elements of a CKM matrix. -/
|
||||
def Rubud (V : CKMMatrix) : ℂ := [V]ub / [V]ud
|
||||
|
||||
/-- The ratio of the `ub` and `ud` elements of a CKM matrix. -/
|
||||
scoped[CKMMatrix] notation (name := ub_ud_ratio) "[" V "]ub|ud" => Rubud V
|
||||
|
||||
/-- The ratio of the `us` and `ud` elements of a CKM matrix. -/
|
||||
def Rusud (V : CKMMatrix) : ℂ := [V]us / [V]ud
|
||||
|
||||
/-- The ratio of the `us` and `ud` elements of a CKM matrix. -/
|
||||
scoped[CKMMatrix] notation (name := us_ud_ratio) "[" V "]us|ud" => Rusud V
|
||||
|
||||
/-- The ratio of the `ud` and `us` elements of a CKM matrix. -/
|
||||
def Rudus (V : CKMMatrix) : ℂ := [V]ud / [V]us
|
||||
|
||||
/-- The ratio of the `ud` and `us` elements of a CKM matrix. -/
|
||||
scoped[CKMMatrix] notation (name := ud_us_ratio) "[" V "]ud|us" => Rudus V
|
||||
|
||||
/-- The ratio of the `ub` and `us` elements of a CKM matrix. -/
|
||||
def Rubus (V : CKMMatrix) : ℂ := [V]ub / [V]us
|
||||
|
||||
/-- The ratio of the `ub` and `us` elements of a CKM matrix. -/
|
||||
scoped[CKMMatrix] notation (name := ub_us_ratio) "[" V "]ub|us" => Rubus V
|
||||
|
||||
/-- The ratio of the `cd` and `cb` elements of a CKM matrix. -/
|
||||
def Rcdcb (V : CKMMatrix) : ℂ := [V]cd / [V]cb
|
||||
|
||||
/-- The ratio of the `cd` and `cb` elements of a CKM matrix. -/
|
||||
scoped[CKMMatrix] notation (name := cd_cb_ratio) "[" V "]cd|cb" => Rcdcb V
|
||||
|
||||
lemma Rcdcb_mul_cb {V : CKMMatrix} (h : [V]cb ≠ 0): [V]cd = Rcdcb V * [V]cb := by
|
||||
rw [Rcdcb]
|
||||
exact (div_mul_cancel₀ (V.1 1 0) h).symm
|
||||
|
||||
/-- The ratio of the `cs` and `cb` elements of a CKM matrix. -/
|
||||
def Rcscb (V : CKMMatrix) : ℂ := [V]cs / [V]cb
|
||||
|
||||
/-- The ratio of the `cs` and `cb` elements of a CKM matrix. -/
|
||||
scoped[CKMMatrix] notation (name := cs_cb_ratio) "[" V "]cs|cb" => Rcscb V
|
||||
|
||||
lemma Rcscb_mul_cb {V : CKMMatrix} (h : [V]cb ≠ 0): [V]cs = Rcscb V * [V]cb := by
|
||||
rw [Rcscb]
|
||||
exact (div_mul_cancel₀ [V]cs h).symm
|
||||
|
||||
end ratios
|
||||
|
||||
|
||||
end CKMMatrix
|
||||
|
||||
end
|
||||
69
HepLean/FlavorPhysics/CKMMatrix/Invariants.lean
Normal file
69
HepLean/FlavorPhysics/CKMMatrix/Invariants.lean
Normal file
|
|
@ -0,0 +1,69 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.FlavorPhysics.CKMMatrix.Basic
|
||||
import HepLean.FlavorPhysics.CKMMatrix.Rows
|
||||
import HepLean.FlavorPhysics.CKMMatrix.PhaseFreedom
|
||||
import Mathlib.Analysis.SpecialFunctions.Complex.Arg
|
||||
/-!
|
||||
# Invariants of the CKM Matrix
|
||||
|
||||
The CKM matrix is only defined up to an equivalence.
|
||||
|
||||
This file defines some invariants of the CKM matrix, which are well-defined with respect to
|
||||
this equivalence.
|
||||
|
||||
Of note, this file defines the complex jarlskog invariant.
|
||||
|
||||
|
||||
-/
|
||||
open Matrix Complex
|
||||
open ComplexConjugate
|
||||
open CKMMatrix
|
||||
|
||||
|
||||
noncomputable section
|
||||
namespace Invariant
|
||||
|
||||
|
||||
/-- The complex jarlskog invariant for a CKM matrix. -/
|
||||
@[simps!]
|
||||
def jarlskogℂCKM (V : CKMMatrix) : ℂ :=
|
||||
[V]us * [V]cb * conj [V]ub * conj [V]cs
|
||||
|
||||
lemma jarlskogℂCKM_equiv (V U : CKMMatrix) (h : V ≈ U) :
|
||||
jarlskogℂCKM V = jarlskogℂCKM U := by
|
||||
obtain ⟨a, b, c, e, f, g, h⟩ := h
|
||||
change V = phaseShiftApply U a b c e f g at h
|
||||
rw [h]
|
||||
simp only [jarlskogℂCKM, Fin.isValue, phaseShiftApply.ub,
|
||||
phaseShiftApply.us, phaseShiftApply.cb, phaseShiftApply.cs]
|
||||
simp [← exp_conj, conj_ofReal, exp_add, exp_neg]
|
||||
have ha : cexp (↑a * I) ≠ 0 := exp_ne_zero _
|
||||
have hb : cexp (↑b * I) ≠ 0 := exp_ne_zero _
|
||||
have hf : cexp (↑f * I) ≠ 0 := exp_ne_zero _
|
||||
have hg : cexp (↑g * I) ≠ 0 := exp_ne_zero _
|
||||
field_simp
|
||||
ring
|
||||
|
||||
/-- The complex jarlskog invariant for an equivalence class of CKM matrices. -/
|
||||
@[simp]
|
||||
def jarlskogℂ : Quotient CKMMatrixSetoid → ℂ :=
|
||||
Quotient.lift jarlskogℂCKM jarlskogℂCKM_equiv
|
||||
|
||||
/-- An invariant for CKM mtrices corresponding to the square of the absolute values
|
||||
of the `us`, `ub` and `cb` elements multipled together divied by `(VudAbs V ^ 2 + VusAbs V ^2)` .
|
||||
-/
|
||||
def VusVubVcdSq (V : Quotient CKMMatrixSetoid) : ℝ :=
|
||||
VusAbs V ^ 2 * VubAbs V ^ 2 * VcbAbs V ^2 / (VudAbs V ^ 2 + VusAbs V ^2)
|
||||
|
||||
/-- An invariant for CKM matrices. The argument of this invariant is `δ₁₃` in the
|
||||
standard parameterization. -/
|
||||
def mulExpδ₁₃ (V : Quotient CKMMatrixSetoid) : ℂ :=
|
||||
jarlskogℂ V + VusVubVcdSq V
|
||||
|
||||
|
||||
end Invariant
|
||||
end
|
||||
364
HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
Normal file
364
HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
Normal file
|
|
@ -0,0 +1,364 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.FlavorPhysics.CKMMatrix.Basic
|
||||
import HepLean.FlavorPhysics.CKMMatrix.Rows
|
||||
import HepLean.FlavorPhysics.CKMMatrix.Relations
|
||||
import Mathlib.Analysis.SpecialFunctions.Complex.Arg
|
||||
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
|
||||
/-!
|
||||
# Phase freedom of the CKM Matrix
|
||||
|
||||
The CKM matrix is only defined up to an equivalence. This leads to a freedom
|
||||
to shift the phases of the matrices elements of the CKM matrix.
|
||||
|
||||
In this file we define two sets of conditions on the CKM matrices
|
||||
`fstRowThdColRealCond` which we show can be satisfied by any CKM matrix up to equivalence
|
||||
and `ubOnePhaseCond` which we show can be satisfied by any CKM matrix up to equivalence as long as
|
||||
the ub element as absolute value 1.
|
||||
|
||||
|
||||
-/
|
||||
open Matrix Complex
|
||||
|
||||
|
||||
noncomputable section
|
||||
namespace CKMMatrix
|
||||
open ComplexConjugate
|
||||
|
||||
section phaseShiftApply
|
||||
variable (u c t d s b : ℝ)
|
||||
|
||||
lemma shift_ud_phase_zero (V : CKMMatrix) (h1 : u + d = - arg [V]ud) :
|
||||
[phaseShiftApply V u c t d s b]ud = VudAbs ⟦V⟧ := by
|
||||
rw [phaseShiftApply.ud]
|
||||
rw [← abs_mul_exp_arg_mul_I [V]ud]
|
||||
rw [mul_comm, mul_assoc, ← exp_add]
|
||||
have h2 : ↑(arg (V.1 0 0)) * I + (↑u * I + ↑d * I) = ↑(arg (V.1 0 0) + (u + d)) * I := by
|
||||
simp [add_assoc]
|
||||
ring
|
||||
rw [h2, h1]
|
||||
simp
|
||||
rfl
|
||||
|
||||
lemma shift_us_phase_zero {V : CKMMatrix} (h1 : u + s = - arg [V]us) :
|
||||
[phaseShiftApply V u c t d s b]us = VusAbs ⟦V⟧ := by
|
||||
rw [phaseShiftApply.us]
|
||||
rw [← abs_mul_exp_arg_mul_I [V]us]
|
||||
rw [mul_comm, mul_assoc, ← exp_add]
|
||||
have h2 : ↑(arg [V]us) * I + (↑u * I + ↑s * I) = ↑(arg [V]us + (u + s)) * I := by
|
||||
simp [add_assoc]
|
||||
ring
|
||||
rw [h2, h1]
|
||||
simp
|
||||
rfl
|
||||
|
||||
lemma shift_ub_phase_zero {V : CKMMatrix} (h1 : u + b = - arg [V]ub) :
|
||||
[phaseShiftApply V u c t d s b]ub = VubAbs ⟦V⟧ := by
|
||||
rw [phaseShiftApply.ub]
|
||||
rw [← abs_mul_exp_arg_mul_I [V]ub]
|
||||
rw [mul_comm, mul_assoc, ← exp_add]
|
||||
have h2 : ↑(arg [V]ub) * I + (↑u * I + ↑b * I) = ↑(arg [V]ub + (u + b)) * I := by
|
||||
simp [add_assoc]
|
||||
ring
|
||||
rw [h2, h1]
|
||||
simp
|
||||
rfl
|
||||
|
||||
lemma shift_cs_phase_zero {V : CKMMatrix} (h1 : c + s = - arg [V]cs) :
|
||||
[phaseShiftApply V u c t d s b]cs = VcsAbs ⟦V⟧ := by
|
||||
rw [phaseShiftApply.cs]
|
||||
rw [← abs_mul_exp_arg_mul_I [V]cs]
|
||||
rw [mul_comm, mul_assoc, ← exp_add]
|
||||
have h2 : ↑(arg [V]cs) * I + (↑c * I + ↑s * I) = ↑(arg [V]cs + (c + s)) * I := by
|
||||
simp [add_assoc]
|
||||
ring
|
||||
rw [h2, h1]
|
||||
simp
|
||||
rfl
|
||||
|
||||
lemma shift_cb_phase_zero {V : CKMMatrix} (h1 : c + b = - arg [V]cb) :
|
||||
[phaseShiftApply V u c t d s b]cb = VcbAbs ⟦V⟧ := by
|
||||
rw [phaseShiftApply.cb]
|
||||
rw [← abs_mul_exp_arg_mul_I [V]cb]
|
||||
rw [mul_comm, mul_assoc, ← exp_add]
|
||||
have h2 : ↑(arg [V]cb) * I + (↑c * I + ↑b * I) = ↑(arg [V]cb + (c + b)) * I := by
|
||||
simp [add_assoc]
|
||||
ring
|
||||
rw [h2, h1]
|
||||
simp
|
||||
rfl
|
||||
|
||||
lemma shift_tb_phase_zero {V : CKMMatrix} (h1 : t + b = - arg [V]tb) :
|
||||
[phaseShiftApply V u c t d s b]tb = VtbAbs ⟦V⟧ := by
|
||||
rw [phaseShiftApply.tb]
|
||||
rw [← abs_mul_exp_arg_mul_I [V]tb]
|
||||
rw [mul_comm, mul_assoc, ← exp_add]
|
||||
have h2 : ↑(arg [V]tb) * I + (↑t * I + ↑b * I) = ↑(arg [V]tb + (t + b)) * I := by
|
||||
simp [add_assoc]
|
||||
ring
|
||||
rw [h2, h1]
|
||||
simp
|
||||
rfl
|
||||
|
||||
lemma shift_cd_phase_pi {V : CKMMatrix} (h1 : c + d = Real.pi - arg [V]cd) :
|
||||
[phaseShiftApply V u c t d s b]cd = - VcdAbs ⟦V⟧ := by
|
||||
rw [phaseShiftApply.cd]
|
||||
rw [← abs_mul_exp_arg_mul_I [V]cd]
|
||||
rw [mul_comm, mul_assoc, ← exp_add]
|
||||
have h2 : ↑(arg [V]cd) * I + (↑c * I + ↑d * I) = ↑(arg [V]cd + (c + d)) * I := by
|
||||
simp [add_assoc]
|
||||
ring
|
||||
rw [h2, h1]
|
||||
simp
|
||||
rfl
|
||||
|
||||
lemma shift_cross_product_phase_zero {V : CKMMatrix} {τ : ℝ}
|
||||
(hτ : cexp (τ * I) • (conj [V]u ×₃ conj [V]c) = [V]t) (h1 : τ = - u - c - t - d - s - b) :
|
||||
[phaseShiftApply V u c t d s b]t =
|
||||
conj [phaseShiftApply V u c t d s b]u ×₃ conj [phaseShiftApply V u c t d s b]c := by
|
||||
change _ = phaseShiftApply.ucCross _ _ _ _ _ _ _
|
||||
funext i
|
||||
fin_cases i
|
||||
· simp
|
||||
rw [phaseShiftApply.ucCross_fst]
|
||||
simp [tRow, phaseShiftApply.td]
|
||||
have hτ0 := congrFun hτ 0
|
||||
simp [tRow] at hτ0
|
||||
rw [← hτ0]
|
||||
rw [← mul_assoc, ← exp_add, h1]
|
||||
congr 2
|
||||
simp only [ofReal_sub, ofReal_neg]
|
||||
ring
|
||||
· simp
|
||||
rw [phaseShiftApply.ucCross_snd]
|
||||
simp [tRow, phaseShiftApply.ts]
|
||||
have hτ0 := congrFun hτ 1
|
||||
simp [tRow] at hτ0
|
||||
rw [← hτ0]
|
||||
rw [← mul_assoc, ← exp_add, h1]
|
||||
congr 2
|
||||
simp only [ofReal_sub, ofReal_neg]
|
||||
ring
|
||||
· simp
|
||||
rw [phaseShiftApply.ucCross_thd]
|
||||
simp [tRow, phaseShiftApply.tb]
|
||||
have hτ0 := congrFun hτ 2
|
||||
simp [tRow] at hτ0
|
||||
rw [← hτ0]
|
||||
rw [← mul_assoc, ← exp_add, h1]
|
||||
congr 2
|
||||
simp only [ofReal_sub, ofReal_neg]
|
||||
ring
|
||||
|
||||
end phaseShiftApply
|
||||
|
||||
variable (a b c d e f : ℝ)
|
||||
|
||||
/-- A proposition which is satisfied by a CKM matrix if its `ud`, `us`, `cb` and `tb` elements
|
||||
are positive and real, and there is no phase difference between the `t`th-row and
|
||||
the cross product of the conjugates of the `u`th and `c`th rows. -/
|
||||
def fstRowThdColRealCond (U : CKMMatrix) : Prop := [U]ud = VudAbs ⟦U⟧ ∧ [U]us = VusAbs ⟦U⟧
|
||||
∧ [U]cb = VcbAbs ⟦U⟧ ∧ [U]tb = VtbAbs ⟦U⟧ ∧ [U]t = conj [U]u ×₃ conj [U]c
|
||||
|
||||
/-- A proposition which is satisfied by a CKM matrix `ub` is one, `ud`, `us` and `cb` are zero,
|
||||
there is no phase difference between the `t`th-row and
|
||||
the cross product of the conjugates of the `u`th and `c`th rows, and the `cd`th and `cs`th
|
||||
elements are real and related in a set way.
|
||||
-/
|
||||
def ubOnePhaseCond (U : CKMMatrix) : Prop :=
|
||||
[U]ud = 0 ∧ [U]us = 0 ∧ [U]cb = 0 ∧ [U]ub = 1 ∧ [U]t = conj [U]u ×₃ conj [U]c
|
||||
∧ [U]cd = - VcdAbs ⟦U⟧ ∧ [U]cs = √(1 - VcdAbs ⟦U⟧ ^ 2)
|
||||
|
||||
lemma fstRowThdColRealCond_shift_solution {V : CKMMatrix} (h1 : a + d = - arg [V]ud)
|
||||
(h2 : a + e = - arg [V]us) (h3 : b + f = - arg [V]cb)
|
||||
(h4 : c + f = - arg [V]tb) (h5 : τ = - a - b - c - d - e - f) :
|
||||
b = - τ + arg [V]ud + arg [V]us + arg [V]tb + a ∧
|
||||
c = - τ + arg [V]cb + arg [V]ud + arg [V]us + a ∧
|
||||
d = - arg [V]ud - a ∧
|
||||
e = - arg [V]us - a ∧
|
||||
f = τ - arg [V]ud - arg [V]us - arg [V]cb - arg [V]tb - a := by
|
||||
have hd : d = - arg [V]ud - a := by
|
||||
linear_combination h1
|
||||
subst hd
|
||||
have he : e = - arg [V]us - a := by
|
||||
linear_combination h2
|
||||
subst he
|
||||
simp_all
|
||||
have hbf : b = - arg [V]cb - f := by
|
||||
linear_combination h3
|
||||
have hcf : c = - arg [V]tb - f := by
|
||||
linear_combination h4
|
||||
rw [hbf, hcf] at h5
|
||||
simp_all
|
||||
ring_nf at h5
|
||||
have hf : f = τ - a - arg [V]ud - arg [V]us - arg [V]cb - arg [V]tb := by
|
||||
linear_combination -(1 * h5)
|
||||
rw [hf] at hbf hcf
|
||||
ring_nf at hbf hcf
|
||||
subst hf hbf hcf
|
||||
ring_nf
|
||||
simp
|
||||
|
||||
lemma ubOnePhaseCond_shift_solution {V : CKMMatrix} (h1 : a + f = - arg [V]ub)
|
||||
(h2 : 0 = - a - b - c - d - e - f)
|
||||
(h3 : b + d = Real.pi - arg [V]cd) (h5 : b + e = - arg [V]cs) :
|
||||
c = - Real.pi + arg [V]cd + arg [V]cs + arg [V]ub + b ∧
|
||||
d = Real.pi - arg [V]cd - b ∧
|
||||
e = - arg [V]cs - b ∧
|
||||
f = - arg [V]ub - a := by
|
||||
have hf : f = - arg [V]ub - a := by
|
||||
linear_combination h1
|
||||
subst hf
|
||||
have he : e = - arg [V]cs - b := by
|
||||
linear_combination h5
|
||||
have hd : d = Real.pi - arg [V]cd - b := by
|
||||
linear_combination h3
|
||||
subst he hd
|
||||
simp_all
|
||||
ring_nf at h2
|
||||
have hc : c = - Real.pi + arg [V]cd + arg [V]cs + arg [V]ub + b := by
|
||||
linear_combination h2
|
||||
subst hc
|
||||
ring
|
||||
|
||||
-- rename
|
||||
lemma fstRowThdColRealCond_holds_up_to_equiv (V : CKMMatrix) :
|
||||
∃ (U : CKMMatrix), V ≈ U ∧ fstRowThdColRealCond U:= by
|
||||
obtain ⟨τ, hτ⟩ := V.uRow_cross_cRow_eq_tRow
|
||||
let U : CKMMatrix := phaseShiftApply V
|
||||
0
|
||||
(- τ + arg [V]ud + arg [V]us + arg [V]tb )
|
||||
(- τ + arg [V]cb + arg [V]ud + arg [V]us )
|
||||
(- arg [V]ud )
|
||||
(- arg [V]us)
|
||||
(τ - arg [V]ud - arg [V]us - arg [V]cb - arg [V]tb)
|
||||
have hUV : ⟦U⟧ = ⟦V⟧ := by
|
||||
simp only [Quotient.eq]
|
||||
symm
|
||||
exact phaseShiftApply.equiv _ _ _ _ _ _ _
|
||||
use U
|
||||
apply And.intro
|
||||
exact phaseShiftApply.equiv _ _ _ _ _ _ _
|
||||
apply And.intro
|
||||
rw [hUV]
|
||||
apply shift_ud_phase_zero _ _ _ _ _ _ _
|
||||
ring
|
||||
apply And.intro
|
||||
rw [hUV]
|
||||
apply shift_us_phase_zero
|
||||
ring
|
||||
apply And.intro
|
||||
rw [hUV]
|
||||
apply shift_cb_phase_zero
|
||||
ring
|
||||
apply And.intro
|
||||
rw [hUV]
|
||||
apply shift_tb_phase_zero
|
||||
ring
|
||||
apply shift_cross_product_phase_zero _ _ _ _ _ _ hτ.symm
|
||||
ring
|
||||
|
||||
|
||||
lemma ubOnePhaseCond_hold_up_to_equiv_of_ub_one {V : CKMMatrix} (hb : ¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0))
|
||||
(hV : fstRowThdColRealCond V) :
|
||||
∃ (U : CKMMatrix), V ≈ U ∧ ubOnePhaseCond U:= by
|
||||
let U : CKMMatrix := phaseShiftApply V 0 0 (- Real.pi + arg [V]cd + arg [V]cs + arg [V]ub)
|
||||
(Real.pi - arg [V]cd ) (- arg [V]cs) (- arg [V]ub )
|
||||
use U
|
||||
have hUV : ⟦U⟧ = ⟦V⟧ := by
|
||||
simp only [Quotient.eq]
|
||||
symm
|
||||
exact phaseShiftApply.equiv _ _ _ _ _ _ _
|
||||
apply And.intro
|
||||
exact phaseShiftApply.equiv _ _ _ _ _ _ _
|
||||
apply And.intro
|
||||
· simp [not_or] at hb
|
||||
have h1 : VudAbs ⟦U⟧ = 0 := by
|
||||
rw [hUV]
|
||||
simp [VAbs, hb]
|
||||
simp [VAbs] at h1
|
||||
exact h1
|
||||
apply And.intro
|
||||
· simp [not_or] at hb
|
||||
have h1 : VusAbs ⟦U⟧ = 0 := by
|
||||
rw [hUV]
|
||||
simp [VAbs, hb]
|
||||
simp [VAbs] at h1
|
||||
exact h1
|
||||
apply And.intro
|
||||
· simp [not_or] at hb
|
||||
have h3 := cb_eq_zero_of_ud_us_zero hb
|
||||
have h1 : VcbAbs ⟦U⟧ = 0 := by
|
||||
rw [hUV]
|
||||
simp [VAbs, h3]
|
||||
simp [VAbs] at h1
|
||||
exact h1
|
||||
apply And.intro
|
||||
· have hU1 : [U]ub = VubAbs ⟦V⟧ := by
|
||||
apply shift_ub_phase_zero _ _ _ _ _ _ _
|
||||
ring
|
||||
rw [hU1]
|
||||
have h1:= (ud_us_neq_zero_iff_ub_neq_one V).mpr.mt hb
|
||||
simpa using h1
|
||||
apply And.intro
|
||||
· have hτ : [V]t = cexp ((0 : ℝ) * I) • (conj ([V]u) ×₃ conj ([V]c)) := by
|
||||
simp only [ofReal_zero, zero_mul, exp_zero, one_smul]
|
||||
exact hV.2.2.2.2
|
||||
apply shift_cross_product_phase_zero _ _ _ _ _ _ hτ.symm
|
||||
ring
|
||||
apply And.intro
|
||||
· rw [hUV]
|
||||
apply shift_cd_phase_pi _ _ _ _ _ _ _
|
||||
ring
|
||||
have hcs : [U]cs = VcsAbs ⟦U⟧ := by
|
||||
rw [hUV]
|
||||
apply shift_cs_phase_zero _ _ _ _ _ _ _
|
||||
ring
|
||||
rw [hcs, hUV, cs_of_ud_us_zero hb]
|
||||
|
||||
|
||||
lemma cd_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0)
|
||||
(hV : fstRowThdColRealCond V) :
|
||||
[V]cd = (- VtbAbs ⟦V⟧ * VusAbs ⟦V⟧ / (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2)) +
|
||||
(- VubAbs ⟦V⟧ * VudAbs ⟦V⟧ * VcbAbs ⟦V⟧ / (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2 ))
|
||||
* cexp (- arg [V]ub * I) := by
|
||||
have hτ : [V]t = cexp ((0 : ℝ) * I) • (conj ([V]u) ×₃ conj ([V]c)) := by
|
||||
simp only [ofReal_zero, zero_mul, exp_zero, one_smul]
|
||||
exact hV.2.2.2.2
|
||||
rw [cd_of_ud_us_ub_cb_tb hb hτ]
|
||||
rw [hV.1, hV.2.1, hV.2.2.1, hV.2.2.2.1]
|
||||
simp [sq, conj_ofReal]
|
||||
have hx := Vabs_sq_add_neq_zero hb
|
||||
field_simp
|
||||
have h1 : conj [V]ub = VubAbs ⟦V⟧ * cexp (- arg [V]ub * I) := by
|
||||
nth_rewrite 1 [← abs_mul_exp_arg_mul_I [V]ub]
|
||||
rw [@RingHom.map_mul]
|
||||
simp [conj_ofReal, ← exp_conj, VAbs]
|
||||
rw [h1]
|
||||
ring_nf
|
||||
|
||||
lemma cs_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0)
|
||||
(hV : fstRowThdColRealCond V) :
|
||||
[V]cs = (VtbAbs ⟦V⟧ * VudAbs ⟦V⟧ / (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2))
|
||||
+ (- VubAbs ⟦V⟧ * VusAbs ⟦V⟧ * VcbAbs ⟦V⟧/ (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2))
|
||||
* cexp (- arg [V]ub * I) := by
|
||||
have hτ : [V]t = cexp ((0 : ℝ) * I) • (conj ([V]u) ×₃ conj ([V]c)) := by
|
||||
simp only [ofReal_zero, zero_mul, exp_zero, one_smul]
|
||||
exact hV.2.2.2.2
|
||||
rw [cs_of_ud_us_ub_cb_tb hb hτ]
|
||||
rw [hV.1, hV.2.1, hV.2.2.1, hV.2.2.2.1]
|
||||
simp [sq, conj_ofReal]
|
||||
have hx := Vabs_sq_add_neq_zero hb
|
||||
field_simp
|
||||
have h1 : conj [V]ub = VubAbs ⟦V⟧ * cexp (- arg [V]ub * I) := by
|
||||
nth_rewrite 1 [← abs_mul_exp_arg_mul_I [V]ub]
|
||||
rw [@RingHom.map_mul]
|
||||
simp [conj_ofReal, ← exp_conj, VAbs]
|
||||
rw [h1]
|
||||
ring_nf
|
||||
|
||||
end CKMMatrix
|
||||
end
|
||||
380
HepLean/FlavorPhysics/CKMMatrix/Relations.lean
Normal file
380
HepLean/FlavorPhysics/CKMMatrix/Relations.lean
Normal file
|
|
@ -0,0 +1,380 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.FlavorPhysics.CKMMatrix.Basic
|
||||
import HepLean.FlavorPhysics.CKMMatrix.Rows
|
||||
import Mathlib.Analysis.SpecialFunctions.Complex.Arg
|
||||
/-!
|
||||
# Relations for the CKM Matrix
|
||||
|
||||
This file contains a collection of relations and properties between the elements of the CKM
|
||||
matrix.
|
||||
|
||||
-/
|
||||
|
||||
open Matrix Complex
|
||||
|
||||
|
||||
noncomputable section
|
||||
|
||||
namespace CKMMatrix
|
||||
open ComplexConjugate
|
||||
|
||||
section rows
|
||||
|
||||
lemma VAbs_sum_sq_row_eq_one (V : Quotient CKMMatrixSetoid) (i : Fin 3) :
|
||||
(VAbs i 0 V) ^ 2 + (VAbs i 1 V) ^ 2 + (VAbs i 2 V) ^ 2 = 1 := by
|
||||
obtain ⟨V, hV⟩ := Quot.exists_rep V
|
||||
subst hV
|
||||
have hV := V.prop
|
||||
rw [mem_unitaryGroup_iff] at hV
|
||||
have ht := congrFun (congrFun hV i) i
|
||||
simp [Matrix.mul_apply, Fin.sum_univ_three] at ht
|
||||
rw [mul_conj, mul_conj, mul_conj] at ht
|
||||
repeat rw [← Complex.sq_abs] at ht
|
||||
rw [← ofReal_inj]
|
||||
simpa using ht
|
||||
|
||||
lemma fst_row_normalized_abs (V : CKMMatrix) : abs [V]ud ^ 2 + abs [V]us ^ 2 + abs [V]ub ^ 2 = 1 :=
|
||||
VAbs_sum_sq_row_eq_one ⟦V⟧ 0
|
||||
|
||||
lemma snd_row_normalized_abs (V : CKMMatrix) : abs [V]cd ^ 2 + abs [V]cs ^ 2 + abs [V]cb ^ 2 = 1 :=
|
||||
VAbs_sum_sq_row_eq_one ⟦V⟧ 1
|
||||
|
||||
lemma thd_row_normalized_abs (V : CKMMatrix) : abs [V]td ^ 2 + abs [V]ts ^ 2 + abs [V]tb ^ 2 = 1 :=
|
||||
VAbs_sum_sq_row_eq_one ⟦V⟧ 2
|
||||
|
||||
lemma fst_row_normalized_normSq (V : CKMMatrix) :
|
||||
normSq [V]ud + normSq [V]us + normSq [V]ub = 1 := by
|
||||
repeat rw [← Complex.sq_abs]
|
||||
exact V.fst_row_normalized_abs
|
||||
|
||||
lemma snd_row_normalized_normSq (V : CKMMatrix) :
|
||||
normSq [V]cd + normSq [V]cs + normSq [V]cb = 1 := by
|
||||
repeat rw [← Complex.sq_abs]
|
||||
exact V.snd_row_normalized_abs
|
||||
|
||||
lemma thd_row_normalized_normSq (V : CKMMatrix) :
|
||||
normSq [V]td + normSq [V]ts + normSq [V]tb = 1 := by
|
||||
repeat rw [← Complex.sq_abs]
|
||||
exact V.thd_row_normalized_abs
|
||||
|
||||
lemma normSq_Vud_plus_normSq_Vus (V : CKMMatrix) :
|
||||
normSq [V]ud + normSq [V]us = 1 - normSq [V]ub := by
|
||||
linear_combination (fst_row_normalized_normSq V)
|
||||
|
||||
lemma VudAbs_sq_add_VusAbs_sq : VudAbs V ^ 2 + VusAbs V ^2 = 1 - VubAbs V ^2 := by
|
||||
linear_combination (VAbs_sum_sq_row_eq_one V 0)
|
||||
|
||||
lemma ud_us_neq_zero_iff_ub_neq_one (V : CKMMatrix) :
|
||||
[V]ud ≠ 0 ∨ [V]us ≠ 0 ↔ abs [V]ub ≠ 1 := by
|
||||
have h2 := V.fst_row_normalized_abs
|
||||
apply Iff.intro
|
||||
intro h
|
||||
intro h1
|
||||
rw [h1] at h2
|
||||
simp at h2
|
||||
rw [add_eq_zero_iff' (sq_nonneg _) (sq_nonneg _)] at h2
|
||||
simp_all
|
||||
intro h
|
||||
by_contra hn
|
||||
rw [not_or] at hn
|
||||
simp at hn
|
||||
simp_all
|
||||
have h1 := Complex.abs.nonneg [V]ub
|
||||
rw [h2] at h1
|
||||
have h2 : ¬ 0 ≤ ( -1 : ℝ) := by simp
|
||||
exact h2 h1
|
||||
|
||||
lemma normSq_Vud_plus_normSq_Vus_neq_zero_ℝ {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) :
|
||||
normSq [V]ud + normSq [V]us ≠ 0 := by
|
||||
rw [normSq_Vud_plus_normSq_Vus V]
|
||||
rw [ud_us_neq_zero_iff_ub_neq_one] at hb
|
||||
by_contra hn
|
||||
rw [← Complex.sq_abs] at hn
|
||||
have h2 : Complex.abs (V.1 0 2) ^2 = 1 := by
|
||||
linear_combination -(1 * hn)
|
||||
simp at h2
|
||||
cases' h2 with h2 h2
|
||||
exact hb h2
|
||||
have h3 := Complex.abs.nonneg [V]ub
|
||||
rw [h2] at h3
|
||||
have h2 : ¬ 0 ≤ ( -1 : ℝ) := by simp
|
||||
exact h2 h3
|
||||
|
||||
lemma VAbsub_neq_zero_Vud_Vus_neq_zero {V : Quotient CKMMatrixSetoid}
|
||||
(hV : VAbs 0 2 V ≠ 1) :(VudAbs V ^ 2 + VusAbs V ^ 2) ≠ 0 := by
|
||||
obtain ⟨V⟩ := V
|
||||
change VubAbs ⟦V⟧ ≠ 1 at hV
|
||||
simp only [VubAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk] at hV
|
||||
rw [← ud_us_neq_zero_iff_ub_neq_one V] at hV
|
||||
simpa [← Complex.sq_abs] using (normSq_Vud_plus_normSq_Vus_neq_zero_ℝ hV)
|
||||
|
||||
lemma VAbsub_neq_zero_sqrt_Vud_Vus_neq_zero {V : Quotient CKMMatrixSetoid}
|
||||
(hV : VAbs 0 2 V ≠ 1) : √(VudAbs V ^ 2 + VusAbs V ^ 2) ≠ 0 := by
|
||||
obtain ⟨V⟩ := V
|
||||
rw [Real.sqrt_ne_zero (Left.add_nonneg (sq_nonneg _) (sq_nonneg _))]
|
||||
change VubAbs ⟦V⟧ ≠ 1 at hV
|
||||
simp only [VubAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk] at hV
|
||||
rw [← ud_us_neq_zero_iff_ub_neq_one V] at hV
|
||||
simpa [← Complex.sq_abs] using (normSq_Vud_plus_normSq_Vus_neq_zero_ℝ hV)
|
||||
|
||||
|
||||
|
||||
|
||||
lemma normSq_Vud_plus_normSq_Vus_neq_zero_ℂ {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) :
|
||||
(normSq [V]ud : ℂ) + normSq [V]us ≠ 0 := by
|
||||
have h1 := normSq_Vud_plus_normSq_Vus_neq_zero_ℝ hb
|
||||
simp at h1
|
||||
rw [← ofReal_inj] at h1
|
||||
simp_all
|
||||
|
||||
|
||||
lemma Vabs_sq_add_neq_zero {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) :
|
||||
((VudAbs ⟦V⟧ : ℂ) * ↑(VudAbs ⟦V⟧) + ↑(VusAbs ⟦V⟧) * ↑(VusAbs ⟦V⟧)) ≠ 0 := by
|
||||
have h1 := normSq_Vud_plus_normSq_Vus_neq_zero_ℂ hb
|
||||
rw [← Complex.sq_abs, ← Complex.sq_abs] at h1
|
||||
simp [sq] at h1
|
||||
exact h1
|
||||
|
||||
section orthogonal
|
||||
|
||||
lemma fst_row_orthog_snd_row (V : CKMMatrix) :
|
||||
[V]cd * conj [V]ud + [V]cs * conj [V]us + [V]cb * conj [V]ub = 0 := by
|
||||
have hV := V.prop
|
||||
rw [mem_unitaryGroup_iff] at hV
|
||||
have ht := congrFun (congrFun hV 1) 0
|
||||
simp [Matrix.mul_apply, Fin.sum_univ_three] at ht
|
||||
exact ht
|
||||
|
||||
lemma fst_row_orthog_thd_row (V : CKMMatrix) :
|
||||
[V]td * conj [V]ud + [V]ts * conj [V]us + [V]tb * conj [V]ub = 0 := by
|
||||
have hV := V.prop
|
||||
rw [mem_unitaryGroup_iff] at hV
|
||||
have ht := congrFun (congrFun hV 2) 0
|
||||
simp [Matrix.mul_apply, Fin.sum_univ_three] at ht
|
||||
exact ht
|
||||
|
||||
lemma Vcd_mul_conj_Vud (V : CKMMatrix) :
|
||||
[V]cd * conj [V]ud = -[V]cs * conj [V]us - [V]cb * conj [V]ub := by
|
||||
linear_combination (V.fst_row_orthog_snd_row )
|
||||
|
||||
lemma Vcs_mul_conj_Vus (V : CKMMatrix) :
|
||||
[V]cs * conj [V]us = - [V]cd * conj [V]ud - [V]cb * conj [V]ub := by
|
||||
linear_combination (V.fst_row_orthog_snd_row )
|
||||
|
||||
end orthogonal
|
||||
|
||||
lemma VAbs_thd_eq_one_fst_eq_zero {V : Quotient CKMMatrixSetoid} {i : Fin 3} (hV : VAbs i 2 V = 1) :
|
||||
VAbs i 0 V = 0 := by
|
||||
have h := VAbs_sum_sq_row_eq_one V i
|
||||
rw [hV] at h
|
||||
simp at h
|
||||
nlinarith
|
||||
|
||||
lemma VAbs_thd_eq_one_snd_eq_zero {V : Quotient CKMMatrixSetoid} {i : Fin 3} (hV : VAbs i 2 V = 1) :
|
||||
VAbs i 1 V = 0 := by
|
||||
have h := VAbs_sum_sq_row_eq_one V i
|
||||
rw [hV] at h
|
||||
simp at h
|
||||
nlinarith
|
||||
|
||||
section crossProduct
|
||||
|
||||
lemma conj_Vtb_cross_product {V : CKMMatrix} {τ : ℝ}
|
||||
(hτ : [V]t = cexp (τ * I) • (conj [V]u ×₃ conj [V]c)) :
|
||||
conj [V]tb = cexp (- τ * I) * ([V]cs * [V]ud - [V]us * [V]cd) := by
|
||||
have h1 := congrFun hτ 2
|
||||
simp [crossProduct, tRow, uRow, cRow] at h1
|
||||
apply congrArg conj at h1
|
||||
simp at h1
|
||||
rw [h1]
|
||||
simp only [← exp_conj, _root_.map_mul, conj_ofReal, conj_I, mul_neg, Fin.isValue, neg_mul]
|
||||
field_simp
|
||||
ring_nf
|
||||
simp
|
||||
|
||||
end crossProduct
|
||||
|
||||
lemma conj_Vtb_mul_Vud {V : CKMMatrix} {τ : ℝ}
|
||||
(hτ : [V]t = cexp (τ * I) • (conj [V]u ×₃ conj [V]c)) :
|
||||
cexp (τ * I) * conj [V]tb * conj [V]ud =
|
||||
[V]cs * (normSq [V]ud + normSq [V]us) + [V]cb * conj [V]ub * [V]us := by
|
||||
rw [conj_Vtb_cross_product hτ]
|
||||
simp [exp_neg]
|
||||
have h1 := exp_ne_zero (τ * I)
|
||||
field_simp
|
||||
have h2 : cexp (τ * I) * ([V]cs * [V]ud - [V]us * [V]cd) * conj [V]ud = cexp (τ * I) * [V]cs
|
||||
* [V]ud * conj [V]ud - cexp (τ * I) * [V]us * ([V]cd * conj [V]ud) := by
|
||||
ring
|
||||
rw [h2, V.Vcd_mul_conj_Vud]
|
||||
rw [normSq_eq_conj_mul_self, normSq_eq_conj_mul_self]
|
||||
simp only [Fin.isValue, neg_mul]
|
||||
ring
|
||||
|
||||
lemma conj_Vtb_mul_Vus {V : CKMMatrix} {τ : ℝ}
|
||||
(hτ : [V]t = cexp (τ * I) • (conj [V]u ×₃ conj [V]c)) :
|
||||
cexp (τ * I) * conj [V]tb * conj [V]us =
|
||||
- ([V]cd * (normSq [V]ud + normSq [V]us) + [V]cb * conj ([V]ub) * [V]ud) := by
|
||||
rw [conj_Vtb_cross_product hτ]
|
||||
simp [exp_neg]
|
||||
have h1 := exp_ne_zero (τ * I)
|
||||
field_simp
|
||||
have h2 : cexp (τ * I) * ([V]cs * [V]ud - [V]us * [V]cd) * conj [V]us = cexp (τ * I) * ([V]cs
|
||||
* conj [V]us) * [V]ud - cexp (τ * I) * [V]us * [V]cd * conj [V]us := by
|
||||
ring
|
||||
rw [h2, V.Vcs_mul_conj_Vus]
|
||||
rw [normSq_eq_conj_mul_self, normSq_eq_conj_mul_self]
|
||||
simp only [Fin.isValue, neg_mul]
|
||||
ring
|
||||
|
||||
|
||||
lemma cs_of_ud_us_ub_cb_tb {V : CKMMatrix} (h : [V]ud ≠ 0 ∨ [V]us ≠ 0)
|
||||
{τ : ℝ} (hτ : [V]t = cexp (τ * I) • (conj ([V]u) ×₃ conj ([V]c))) :
|
||||
[V]cs = (- conj [V]ub * [V]us * [V]cb +
|
||||
cexp (τ * I) * conj [V]tb * conj [V]ud) / (normSq [V]ud + normSq [V]us) := by
|
||||
have h1 := normSq_Vud_plus_normSq_Vus_neq_zero_ℂ h
|
||||
rw [conj_Vtb_mul_Vud hτ]
|
||||
field_simp
|
||||
ring
|
||||
|
||||
lemma cd_of_ud_us_ub_cb_tb {V : CKMMatrix} (h : [V]ud ≠ 0 ∨ [V]us ≠ 0)
|
||||
{τ : ℝ} (hτ : [V]t = cexp (τ * I) • (conj ([V]u) ×₃ conj ([V]c))) :
|
||||
[V]cd = - (conj [V]ub * [V]ud * [V]cb + cexp (τ * I) * conj [V]tb * conj [V]us) /
|
||||
(normSq [V]ud + normSq [V]us) := by
|
||||
have h1 := normSq_Vud_plus_normSq_Vus_neq_zero_ℂ h
|
||||
rw [conj_Vtb_mul_Vus hτ]
|
||||
field_simp
|
||||
ring
|
||||
|
||||
|
||||
end rows
|
||||
|
||||
|
||||
section individual
|
||||
|
||||
lemma VAbs_ge_zero (i j : Fin 3) (V : Quotient CKMMatrixSetoid) : 0 ≤ VAbs i j V := by
|
||||
obtain ⟨V, hV⟩ := Quot.exists_rep V
|
||||
rw [← hV]
|
||||
exact Complex.abs.nonneg _
|
||||
|
||||
lemma VAbs_leq_one (i j : Fin 3) (V : Quotient CKMMatrixSetoid) : VAbs i j V ≤ 1 := by
|
||||
have h := VAbs_sum_sq_row_eq_one V i
|
||||
fin_cases j
|
||||
change VAbs i 0 V ≤ 1
|
||||
nlinarith
|
||||
change VAbs i 1 V ≤ 1
|
||||
nlinarith
|
||||
change VAbs i 2 V ≤ 1
|
||||
nlinarith
|
||||
|
||||
|
||||
end individual
|
||||
|
||||
section columns
|
||||
|
||||
|
||||
lemma VAbs_sum_sq_col_eq_one (V : Quotient CKMMatrixSetoid) (i : Fin 3) :
|
||||
(VAbs 0 i V) ^ 2 + (VAbs 1 i V) ^ 2 + (VAbs 2 i V) ^ 2 = 1 := by
|
||||
obtain ⟨V, hV⟩ := Quot.exists_rep V
|
||||
subst hV
|
||||
have hV := V.prop
|
||||
rw [mem_unitaryGroup_iff'] at hV
|
||||
have ht := congrFun (congrFun hV i) i
|
||||
simp [Matrix.mul_apply, Fin.sum_univ_three] at ht
|
||||
rw [mul_comm, mul_conj, mul_comm, mul_conj, mul_comm, mul_conj] at ht
|
||||
repeat rw [← Complex.sq_abs] at ht
|
||||
rw [← ofReal_inj]
|
||||
simpa using ht
|
||||
|
||||
lemma thd_col_normalized_abs (V : CKMMatrix) :
|
||||
abs [V]ub ^ 2 + abs [V]cb ^ 2 + abs [V]tb ^ 2 = 1 := by
|
||||
have h1 := VAbs_sum_sq_col_eq_one ⟦V⟧ 2
|
||||
simp [VAbs] at h1
|
||||
exact h1
|
||||
|
||||
lemma thd_col_normalized_normSq (V : CKMMatrix) :
|
||||
normSq [V]ub + normSq [V]cb + normSq [V]tb = 1 := by
|
||||
have h1 := V.thd_col_normalized_abs
|
||||
repeat rw [Complex.sq_abs] at h1
|
||||
exact h1
|
||||
|
||||
lemma cb_eq_zero_of_ud_us_zero {V : CKMMatrix} (h : [V]ud = 0 ∧ [V]us = 0) :
|
||||
[V]cb = 0 := by
|
||||
have h1 := fst_row_normalized_abs V
|
||||
rw [← thd_col_normalized_abs V] at h1
|
||||
simp [h] at h1
|
||||
rw [add_assoc] at h1
|
||||
simp at h1
|
||||
rw [add_eq_zero_iff' (sq_nonneg _) (sq_nonneg _)] at h1
|
||||
simp at h1
|
||||
exact h1.1
|
||||
|
||||
|
||||
lemma cs_of_ud_us_zero {V : CKMMatrix} (ha : ¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0)) :
|
||||
VcsAbs ⟦V⟧ = √(1 - VcdAbs ⟦V⟧ ^ 2) := by
|
||||
have h1 := snd_row_normalized_abs V
|
||||
symm
|
||||
rw [Real.sqrt_eq_iff_sq_eq]
|
||||
simp [not_or] at ha
|
||||
rw [cb_eq_zero_of_ud_us_zero ha] at h1
|
||||
simp at h1
|
||||
simp [VAbs]
|
||||
linear_combination h1
|
||||
simp only [VcdAbs, Fin.isValue, sub_nonneg, sq_le_one_iff_abs_le_one]
|
||||
rw [@abs_le]
|
||||
have h1 := VAbs_leq_one 1 0 ⟦V⟧
|
||||
have h0 := VAbs_ge_zero 1 0 ⟦V⟧
|
||||
simp_all
|
||||
have hn : -1 ≤ (0 : ℝ) := by simp
|
||||
exact hn.trans h0
|
||||
exact VAbs_ge_zero _ _ ⟦V⟧
|
||||
|
||||
lemma VcbAbs_sq_add_VtbAbs_sq (V : Quotient CKMMatrixSetoid) :
|
||||
VcbAbs V ^ 2 + VtbAbs V ^ 2 = 1 - VubAbs V ^2 := by
|
||||
linear_combination (VAbs_sum_sq_col_eq_one V 2)
|
||||
|
||||
|
||||
|
||||
lemma cb_tb_neq_zero_iff_ub_neq_one (V : CKMMatrix) :
|
||||
[V]cb ≠ 0 ∨ [V]tb ≠ 0 ↔ abs [V]ub ≠ 1 := by
|
||||
have h2 := V.thd_col_normalized_abs
|
||||
apply Iff.intro
|
||||
intro h
|
||||
intro h1
|
||||
rw [h1] at h2
|
||||
simp at h2
|
||||
have h2 : Complex.abs (V.1 1 2) ^ 2 + Complex.abs (V.1 2 2) ^ 2 = 0 := by
|
||||
linear_combination h2
|
||||
rw [add_eq_zero_iff' (sq_nonneg _) (sq_nonneg _)] at h2
|
||||
simp_all
|
||||
intro h
|
||||
by_contra hn
|
||||
rw [not_or] at hn
|
||||
simp at hn
|
||||
simp_all
|
||||
have h1 := Complex.abs.nonneg [V]ub
|
||||
rw [h2] at h1
|
||||
have h2 : ¬ 0 ≤ ( -1 : ℝ) := by simp
|
||||
exact h2 h1
|
||||
|
||||
lemma VAbs_fst_col_eq_one_snd_eq_zero {V : Quotient CKMMatrixSetoid} {i : Fin 3}
|
||||
(hV : VAbs 0 i V = 1) : VAbs 1 i V = 0 := by
|
||||
have h := VAbs_sum_sq_col_eq_one V i
|
||||
rw [hV] at h
|
||||
simp at h
|
||||
nlinarith
|
||||
|
||||
lemma VAbs_fst_col_eq_one_thd_eq_zero {V : Quotient CKMMatrixSetoid} {i : Fin 3}
|
||||
(hV : VAbs 0 i V = 1) : VAbs 2 i V = 0 := by
|
||||
have h := VAbs_sum_sq_col_eq_one V i
|
||||
rw [hV] at h
|
||||
simp at h
|
||||
nlinarith
|
||||
|
||||
end columns
|
||||
|
||||
end CKMMatrix
|
||||
end
|
||||
396
HepLean/FlavorPhysics/CKMMatrix/Rows.lean
Normal file
396
HepLean/FlavorPhysics/CKMMatrix/Rows.lean
Normal file
|
|
@ -0,0 +1,396 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.FlavorPhysics.CKMMatrix.Basic
|
||||
import Mathlib.Analysis.SpecialFunctions.Complex.Arg
|
||||
import Mathlib.LinearAlgebra.CrossProduct
|
||||
/-!
|
||||
# Rows for the CKM Matrix
|
||||
|
||||
This file contains the definition extracting the rows of the CKM matrix and
|
||||
proves some properties between them.
|
||||
|
||||
The first row can be extracted as `[V]u` for a CKM matrix `V`.
|
||||
|
||||
|
||||
-/
|
||||
|
||||
open Matrix Complex
|
||||
|
||||
open ComplexConjugate
|
||||
noncomputable section
|
||||
|
||||
namespace CKMMatrix
|
||||
|
||||
|
||||
/-- The `u`th row of the CKM matrix. -/
|
||||
def uRow (V : CKMMatrix) : Fin 3 → ℂ := ![[V]ud, [V]us, [V]ub]
|
||||
|
||||
/-- The `u`th row of the CKM matrix. -/
|
||||
scoped[CKMMatrix] notation (name := u_row) "[" V "]u" => uRow V
|
||||
|
||||
/-- The `c`th row of the CKM matrix. -/
|
||||
def cRow (V : CKMMatrix) : Fin 3 → ℂ := ![[V]cd, [V]cs, [V]cb]
|
||||
|
||||
/-- The `c`th row of the CKM matrix. -/
|
||||
scoped[CKMMatrix] notation (name := c_row) "[" V "]c" => cRow V
|
||||
|
||||
/-- The `t`th row of the CKM matrix. -/
|
||||
def tRow (V : CKMMatrix) : Fin 3 → ℂ := ![[V]td, [V]ts, [V]tb]
|
||||
|
||||
/-- The `t`th row of the CKM matrix. -/
|
||||
scoped[CKMMatrix] notation (name := t_row) "[" V "]t" => tRow V
|
||||
|
||||
lemma uRow_normalized (V : CKMMatrix) : conj [V]u ⬝ᵥ [V]u = 1 := by
|
||||
simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
|
||||
have hV := V.prop
|
||||
rw [mem_unitaryGroup_iff] at hV
|
||||
have ht := congrFun (congrFun hV 0) 0
|
||||
simp [Matrix.mul_apply, Fin.sum_univ_three] at ht
|
||||
rw [mul_comm (V.1 0 0) _, mul_comm (V.1 0 1) _, mul_comm (V.1 0 2) _] at ht
|
||||
exact ht
|
||||
|
||||
lemma cRow_normalized (V : CKMMatrix) : conj [V]c ⬝ᵥ [V]c = 1 := by
|
||||
simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
|
||||
have hV := V.prop
|
||||
rw [mem_unitaryGroup_iff] at hV
|
||||
have ht := congrFun (congrFun hV 1) 1
|
||||
simp [Matrix.mul_apply, Fin.sum_univ_three] at ht
|
||||
rw [mul_comm (V.1 1 0) _, mul_comm (V.1 1 1) _, mul_comm (V.1 1 2) _] at ht
|
||||
exact ht
|
||||
|
||||
lemma uRow_cRow_orthog (V : CKMMatrix) : conj [V]u ⬝ᵥ [V]c = 0 := by
|
||||
simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
|
||||
have hV := V.prop
|
||||
rw [mem_unitaryGroup_iff] at hV
|
||||
have ht := congrFun (congrFun hV 1) 0
|
||||
simp [Matrix.mul_apply, Fin.sum_univ_three] at ht
|
||||
rw [mul_comm (V.1 _ 0) _, mul_comm (V.1 _ 1) _, mul_comm (V.1 _ 2) _] at ht
|
||||
exact ht
|
||||
|
||||
lemma uRow_tRow_orthog (V : CKMMatrix) : conj [V]u ⬝ᵥ [V]t = 0 := by
|
||||
simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
|
||||
have hV := V.prop
|
||||
rw [mem_unitaryGroup_iff] at hV
|
||||
have ht := congrFun (congrFun hV 2) 0
|
||||
simp [Matrix.mul_apply, Fin.sum_univ_three] at ht
|
||||
rw [mul_comm (V.1 _ 0) _, mul_comm (V.1 _ 1) _, mul_comm (V.1 _ 2) _] at ht
|
||||
exact ht
|
||||
|
||||
lemma cRow_uRow_orthog (V : CKMMatrix) : conj [V]c ⬝ᵥ [V]u = 0 := by
|
||||
simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
|
||||
have hV := V.prop
|
||||
rw [mem_unitaryGroup_iff] at hV
|
||||
have ht := congrFun (congrFun hV 0) 1
|
||||
simp [Matrix.mul_apply, Fin.sum_univ_three] at ht
|
||||
rw [mul_comm (V.1 _ 0) _, mul_comm (V.1 _ 1) _, mul_comm (V.1 _ 2) _] at ht
|
||||
exact ht
|
||||
|
||||
lemma cRow_tRow_orthog (V : CKMMatrix) : conj [V]c ⬝ᵥ [V]t = 0 := by
|
||||
simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
|
||||
have hV := V.prop
|
||||
rw [mem_unitaryGroup_iff] at hV
|
||||
have ht := congrFun (congrFun hV 2) 1
|
||||
simp [Matrix.mul_apply, Fin.sum_univ_three] at ht
|
||||
rw [mul_comm (V.1 _ 0) _, mul_comm (V.1 _ 1) _, mul_comm (V.1 _ 2) _] at ht
|
||||
exact ht
|
||||
|
||||
lemma tRow_normalized (V : CKMMatrix) : conj [V]t ⬝ᵥ [V]t = 1 := by
|
||||
simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
|
||||
have hV := V.prop
|
||||
rw [mem_unitaryGroup_iff] at hV
|
||||
have ht := congrFun (congrFun hV 2) 2
|
||||
simp [Matrix.mul_apply, Fin.sum_univ_three] at ht
|
||||
rw [mul_comm (V.1 2 0) _, mul_comm (V.1 2 1) _, mul_comm (V.1 2 2) _] at ht
|
||||
exact ht
|
||||
|
||||
lemma tRow_uRow_orthog (V : CKMMatrix) : conj [V]t ⬝ᵥ [V]u = 0 := by
|
||||
simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
|
||||
have hV := V.prop
|
||||
rw [mem_unitaryGroup_iff] at hV
|
||||
have ht := congrFun (congrFun hV 0) 2
|
||||
simp [Matrix.mul_apply, Fin.sum_univ_three] at ht
|
||||
rw [mul_comm (V.1 _ 0) _, mul_comm (V.1 _ 1) _, mul_comm (V.1 _ 2) _] at ht
|
||||
exact ht
|
||||
|
||||
lemma tRow_cRow_orthog (V : CKMMatrix) : conj [V]t ⬝ᵥ [V]c = 0 := by
|
||||
simp only [vec3_dotProduct, Fin.isValue, Pi.conj_apply]
|
||||
have hV := V.prop
|
||||
rw [mem_unitaryGroup_iff] at hV
|
||||
have ht := congrFun (congrFun hV 1) 2
|
||||
simp [Matrix.mul_apply, Fin.sum_univ_three] at ht
|
||||
rw [mul_comm (V.1 _ 0) _, mul_comm (V.1 _ 1) _, mul_comm (V.1 _ 2) _] at ht
|
||||
exact ht
|
||||
|
||||
lemma uRow_cross_cRow_conj (V : CKMMatrix) : conj (conj [V]u ×₃ conj [V]c) = [V]u ×₃ [V]c := by
|
||||
simp [crossProduct]
|
||||
funext i
|
||||
fin_cases i <;> simp
|
||||
|
||||
lemma cRow_cross_tRow_conj (V : CKMMatrix) : conj (conj [V]c ×₃ conj [V]t) = [V]c ×₃ [V]t := by
|
||||
simp [crossProduct]
|
||||
funext i
|
||||
fin_cases i <;> simp
|
||||
|
||||
lemma uRow_cross_cRow_normalized (V : CKMMatrix) :
|
||||
conj (conj [V]u ×₃ conj [V]c) ⬝ᵥ (conj [V]u ×₃ conj [V]c) = 1 := by
|
||||
rw [uRow_cross_cRow_conj, cross_dot_cross]
|
||||
rw [dotProduct_comm, uRow_normalized, dotProduct_comm, cRow_normalized]
|
||||
rw [dotProduct_comm, cRow_uRow_orthog, dotProduct_comm, uRow_cRow_orthog]
|
||||
simp
|
||||
|
||||
lemma cRow_cross_tRow_normalized (V : CKMMatrix) :
|
||||
conj (conj [V]c ×₃ conj [V]t) ⬝ᵥ (conj [V]c ×₃ conj [V]t) = 1 := by
|
||||
rw [cRow_cross_tRow_conj, cross_dot_cross]
|
||||
rw [dotProduct_comm, cRow_normalized, dotProduct_comm, tRow_normalized]
|
||||
rw [dotProduct_comm, tRow_cRow_orthog, dotProduct_comm, cRow_tRow_orthog]
|
||||
simp
|
||||
|
||||
/-- A map from `Fin 3` to each row of a CKM matrix. -/
|
||||
@[simp]
|
||||
def rows (V : CKMMatrix) : Fin 3 → Fin 3 → ℂ := fun i =>
|
||||
match i with
|
||||
| 0 => uRow V
|
||||
| 1 => cRow V
|
||||
| 2 => tRow V
|
||||
|
||||
lemma rows_linearly_independent (V : CKMMatrix) : LinearIndependent ℂ (rows V) := by
|
||||
apply Fintype.linearIndependent_iff.mpr
|
||||
intro g hg
|
||||
rw [Fin.sum_univ_three] at hg
|
||||
simp at hg
|
||||
have h0 := congrArg (fun X => conj [V]u ⬝ᵥ X) hg
|
||||
have h1 := congrArg (fun X => conj [V]c ⬝ᵥ X) hg
|
||||
have h2 := congrArg (fun X => conj [V]t ⬝ᵥ X) hg
|
||||
simp only [Fin.isValue, dotProduct_add, dotProduct_smul, Pi.conj_apply,
|
||||
smul_eq_mul, dotProduct_zero] at h0 h1 h2
|
||||
rw [uRow_normalized, uRow_cRow_orthog, uRow_tRow_orthog] at h0
|
||||
rw [cRow_normalized, cRow_uRow_orthog, cRow_tRow_orthog] at h1
|
||||
rw [tRow_normalized, tRow_uRow_orthog, tRow_cRow_orthog] at h2
|
||||
simp at h0 h1 h2
|
||||
intro i
|
||||
fin_cases i
|
||||
exact h0
|
||||
exact h1
|
||||
exact h2
|
||||
|
||||
lemma rows_card : Fintype.card (Fin 3) = FiniteDimensional.finrank ℂ (Fin 3 → ℂ) := by
|
||||
simp only [Fintype.card_fin, FiniteDimensional.finrank_fintype_fun_eq_card]
|
||||
|
||||
/-- The rows of a CKM matrix as a basis of `ℂ³`. -/
|
||||
@[simps!]
|
||||
noncomputable def rowBasis (V : CKMMatrix) : Basis (Fin 3) ℂ (Fin 3 → ℂ) :=
|
||||
basisOfLinearIndependentOfCardEqFinrank (rows_linearly_independent V) rows_card
|
||||
|
||||
lemma cRow_cross_tRow_eq_uRow (V : CKMMatrix) :
|
||||
∃ (κ : ℝ), [V]u = cexp (κ * I) • (conj [V]c ×₃ conj [V]t) := by
|
||||
obtain ⟨g, hg⟩ := (mem_span_range_iff_exists_fun ℂ).mp (Basis.mem_span (rowBasis V)
|
||||
(conj [V]c ×₃ conj [V]t))
|
||||
rw [Fin.sum_univ_three, rowBasis] at hg
|
||||
simp at hg
|
||||
have h0 := congrArg (fun X => conj [V]c ⬝ᵥ X) hg
|
||||
have h1 := congrArg (fun X => conj [V]t ⬝ᵥ X) hg
|
||||
simp only [Fin.isValue, dotProduct_add, dotProduct_smul, Pi.conj_apply,
|
||||
smul_eq_mul, dotProduct_zero] at h0 h1
|
||||
rw [cRow_normalized, cRow_uRow_orthog, cRow_tRow_orthog, dot_self_cross] at h0
|
||||
rw [tRow_normalized, tRow_uRow_orthog, tRow_cRow_orthog, dot_cross_self] at h1
|
||||
simp at h0 h1
|
||||
rw [h0, h1] at hg
|
||||
simp at hg
|
||||
have h2 := congrArg (fun X => conj X ⬝ᵥ X) hg
|
||||
simp only [Fin.isValue, dotProduct_smul, Pi.conj_apply, Pi.smul_apply,
|
||||
smul_eq_mul, _root_.map_mul] at h2
|
||||
rw [cRow_cross_tRow_normalized] at h2
|
||||
have h3 : conj (g 0 • [V]u) = conj (g 0) • conj [V]u := by
|
||||
funext i
|
||||
fin_cases i <;> simp
|
||||
rw [h3] at h2
|
||||
simp only [Fin.isValue, smul_dotProduct, Pi.conj_apply, smul_eq_mul] at h2
|
||||
rw [uRow_normalized] at h2
|
||||
simp at h2
|
||||
rw [mul_conj] at h2
|
||||
rw [← Complex.sq_abs] at h2
|
||||
simp at h2
|
||||
cases' h2 with h2 h2
|
||||
swap
|
||||
have hx : Complex.abs (g 0) = -1 := by
|
||||
rw [← ofReal_inj]
|
||||
simp only [Fin.isValue, ofReal_neg, ofReal_one]
|
||||
exact h2
|
||||
have h3 := Complex.abs.nonneg (g 0)
|
||||
simp_all
|
||||
have h4 : (0 : ℝ) < 1 := by norm_num
|
||||
exact False.elim (lt_iff_not_le.mp h4 h3)
|
||||
have hx : [V]u = (g 0)⁻¹ • (conj ([V]c) ×₃ conj ([V]t)) := by
|
||||
rw [← hg]
|
||||
rw [@smul_smul]
|
||||
rw [inv_mul_cancel]
|
||||
simp only [one_smul]
|
||||
by_contra hn
|
||||
rw [hn] at h2
|
||||
simp at h2
|
||||
have hg2 : Complex.abs (g 0)⁻¹ = 1 := by
|
||||
rw [@map_inv₀, h2]
|
||||
simp
|
||||
have hg22 : ∃ (τ : ℝ), (g 0)⁻¹ = Complex.exp (τ * I) := by
|
||||
rw [← abs_mul_exp_arg_mul_I (g 0)⁻¹]
|
||||
rw [hg2]
|
||||
use arg (g 0)⁻¹
|
||||
simp
|
||||
obtain ⟨τ, hτ⟩ := hg22
|
||||
use τ
|
||||
rw [hx, hτ]
|
||||
|
||||
lemma uRow_cross_cRow_eq_tRow (V : CKMMatrix) :
|
||||
∃ (τ : ℝ), [V]t = cexp (τ * I) • (conj ([V]u) ×₃ conj ([V]c)) := by
|
||||
obtain ⟨g, hg⟩ := (mem_span_range_iff_exists_fun ℂ).mp (Basis.mem_span (rowBasis V)
|
||||
(conj ([V]u) ×₃ conj ([V]c)) )
|
||||
rw [Fin.sum_univ_three, rowBasis] at hg
|
||||
simp at hg
|
||||
have h0 := congrArg (fun X => conj [V]u ⬝ᵥ X) hg
|
||||
have h1 := congrArg (fun X => conj [V]c ⬝ᵥ X) hg
|
||||
simp only [Fin.isValue, dotProduct_add, dotProduct_smul, Pi.conj_apply,
|
||||
smul_eq_mul, dotProduct_zero] at h0 h1
|
||||
rw [uRow_normalized, uRow_cRow_orthog, uRow_tRow_orthog, dot_self_cross] at h0
|
||||
rw [cRow_normalized, cRow_uRow_orthog, cRow_tRow_orthog, dot_cross_self] at h1
|
||||
simp at h0 h1
|
||||
rw [h0, h1] at hg
|
||||
simp at hg
|
||||
have h2 := congrArg (fun X => conj X ⬝ᵥ X) hg
|
||||
simp only [Fin.isValue, dotProduct_smul, Pi.conj_apply, Pi.smul_apply,
|
||||
smul_eq_mul, _root_.map_mul] at h2
|
||||
rw [uRow_cross_cRow_normalized] at h2
|
||||
have h3 : conj (g 2 • [V]t) = conj (g 2) • conj [V]t := by
|
||||
funext i
|
||||
fin_cases i <;> simp
|
||||
rw [h3] at h2
|
||||
simp only [Fin.isValue, smul_dotProduct, Pi.conj_apply, smul_eq_mul] at h2
|
||||
rw [tRow_normalized] at h2
|
||||
simp at h2
|
||||
rw [mul_conj] at h2
|
||||
rw [← Complex.sq_abs] at h2
|
||||
simp at h2
|
||||
cases' h2 with h2 h2
|
||||
swap
|
||||
have hx : Complex.abs (g 2) = -1 := by
|
||||
rw [← ofReal_inj]
|
||||
simp only [Fin.isValue, ofReal_neg, ofReal_one]
|
||||
exact h2
|
||||
have h3 := Complex.abs.nonneg (g 2)
|
||||
simp_all
|
||||
have h4 : (0 : ℝ) < 1 := by norm_num
|
||||
exact False.elim (lt_iff_not_le.mp h4 h3)
|
||||
have hx : [V]t = (g 2)⁻¹ • (conj ([V]u) ×₃ conj ([V]c)) := by
|
||||
rw [← hg]
|
||||
rw [@smul_smul]
|
||||
rw [inv_mul_cancel]
|
||||
simp only [one_smul]
|
||||
by_contra hn
|
||||
rw [hn] at h2
|
||||
simp at h2
|
||||
have hg2 : Complex.abs (g 2)⁻¹ = 1 := by
|
||||
rw [@map_inv₀, h2]
|
||||
simp
|
||||
have hg22 : ∃ (τ : ℝ), (g 2)⁻¹ = Complex.exp (τ * I) := by
|
||||
rw [← abs_mul_exp_arg_mul_I (g 2)⁻¹]
|
||||
rw [hg2]
|
||||
use arg (g 2)⁻¹
|
||||
simp
|
||||
obtain ⟨τ, hτ⟩ := hg22
|
||||
use τ
|
||||
rw [hx, hτ]
|
||||
|
||||
|
||||
lemma ext_Rows {U V : CKMMatrix} (hu : [U]u = [V]u) (hc : [U]c = [V]c) (ht : [U]t = [V]t) :
|
||||
U = V := by
|
||||
apply CKMMatrix_ext
|
||||
funext i j
|
||||
fin_cases i
|
||||
have h1 := congrFun hu j
|
||||
fin_cases j <;> simpa using h1
|
||||
have h1 := congrFun hc j
|
||||
fin_cases j <;> simpa using h1
|
||||
have h1 := congrFun ht j
|
||||
fin_cases j <;> simpa using h1
|
||||
|
||||
end CKMMatrix
|
||||
|
||||
namespace phaseShiftApply
|
||||
open CKMMatrix
|
||||
|
||||
variable (V : CKMMatrix) (a b c d e f : ℝ)
|
||||
|
||||
/-- The cross product of the conjugate of the `u` and `c` rows of a CKM matrix. -/
|
||||
def ucCross : Fin 3 → ℂ :=
|
||||
conj [phaseShiftApply V a b c d e f]u ×₃ conj [phaseShiftApply V a b c d e f]c
|
||||
|
||||
lemma ucCross_fst (V : CKMMatrix) : (ucCross V a b c d e f) 0 =
|
||||
cexp ((- a * I) + (- b * I) + ( - e * I) + (- f * I)) * (conj [V]u ×₃ conj [V]c) 0 := by
|
||||
simp [ucCross, crossProduct]
|
||||
simp [uRow, us, ub, cRow, cs, cb]
|
||||
rw [exp_add, exp_add]
|
||||
simp [exp_add, exp_sub, ← exp_conj, conj_ofReal]
|
||||
ring
|
||||
|
||||
lemma ucCross_snd (V : CKMMatrix) : (ucCross V a b c d e f) 1 =
|
||||
cexp ((- a * I) + (- b * I) + ( - d * I) + (- f * I)) * (conj [V]u ×₃ conj [V]c) 1 := by
|
||||
simp [ucCross, crossProduct]
|
||||
simp [uRow, us, ub, cRow, cs, cb, ud, cd]
|
||||
rw [exp_add, exp_add]
|
||||
simp [exp_add, exp_sub, ← exp_conj, conj_ofReal]
|
||||
ring
|
||||
|
||||
lemma ucCross_thd (V : CKMMatrix) : (ucCross V a b c d e f) 2 =
|
||||
cexp ((- a * I) + (- b * I) + ( - d * I) + (- e * I)) * (conj [V]u ×₃ conj [V]c) 2 := by
|
||||
simp [ucCross, crossProduct]
|
||||
simp [uRow, us, ub, cRow, cs, cb, ud, cd]
|
||||
rw [exp_add, exp_add]
|
||||
simp [exp_add, exp_sub, ← exp_conj, conj_ofReal]
|
||||
ring
|
||||
|
||||
lemma uRow_mul (V : CKMMatrix) (a b c : ℝ) :
|
||||
[phaseShiftApply V a b c 0 0 0]u = cexp (a * I) • [V]u := by
|
||||
funext i
|
||||
simp only [Pi.smul_apply, smul_eq_mul]
|
||||
fin_cases i <;>
|
||||
change (phaseShiftApply V a b c 0 0 0).1 0 _ = _
|
||||
rw [ud, uRow]
|
||||
simp only [ofReal_zero, zero_mul, add_zero, Fin.isValue, Fin.zero_eta, cons_val_zero]
|
||||
rw [us, uRow]
|
||||
simp only [ofReal_zero, zero_mul, add_zero, Fin.isValue, Fin.mk_one, cons_val_one, head_cons]
|
||||
rw [ub, uRow]
|
||||
simp
|
||||
|
||||
lemma cRow_mul (V : CKMMatrix) (a b c : ℝ) :
|
||||
[phaseShiftApply V a b c 0 0 0]c = cexp (b * I) • [V]c := by
|
||||
funext i
|
||||
simp only [Pi.smul_apply, smul_eq_mul]
|
||||
fin_cases i <;>
|
||||
change (phaseShiftApply V a b c 0 0 0).1 1 _ = _
|
||||
rw [cd, cRow]
|
||||
simp only [ofReal_zero, zero_mul, add_zero, Fin.isValue, Fin.zero_eta, cons_val_zero]
|
||||
rw [cs, cRow]
|
||||
simp only [ofReal_zero, zero_mul, add_zero, Fin.isValue, Fin.mk_one, cons_val_one, head_cons]
|
||||
rw [cb, cRow]
|
||||
simp
|
||||
|
||||
lemma tRow_mul (V : CKMMatrix) (a b c : ℝ) :
|
||||
[phaseShiftApply V a b c 0 0 0]t = cexp (c * I) • [V]t := by
|
||||
funext i
|
||||
simp only [Pi.smul_apply, smul_eq_mul]
|
||||
fin_cases i <;>
|
||||
change (phaseShiftApply V a b c 0 0 0).1 2 _ = _
|
||||
rw [td, tRow]
|
||||
simp only [ofReal_zero, zero_mul, add_zero, Fin.isValue, Fin.zero_eta, cons_val_zero]
|
||||
rw [ts, tRow]
|
||||
simp only [ofReal_zero, zero_mul, add_zero, Fin.isValue, Fin.mk_one, cons_val_one, head_cons]
|
||||
rw [tb, tRow]
|
||||
simp
|
||||
|
||||
|
||||
|
||||
end phaseShiftApply
|
||||
|
||||
end
|
||||
|
|
@ -0,0 +1,201 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.FlavorPhysics.CKMMatrix.Basic
|
||||
import HepLean.FlavorPhysics.CKMMatrix.Rows
|
||||
import HepLean.FlavorPhysics.CKMMatrix.PhaseFreedom
|
||||
import HepLean.FlavorPhysics.CKMMatrix.Invariants
|
||||
import Mathlib.Analysis.SpecialFunctions.Complex.Arg
|
||||
/-!
|
||||
# Standard parameterization for the CKM Matrix
|
||||
|
||||
This file defines the standard parameterization of CKM matrices in terms of
|
||||
four real numbers `θ₁₂`, `θ₁₃`, `θ₂₃` and `δ₁₃`.
|
||||
|
||||
We will show that every CKM matrix can be written within this standard parameterization
|
||||
in the file `FlavorPhysics.CKMMatrix.StandardParameters`.
|
||||
|
||||
|
||||
-/
|
||||
open Matrix Complex
|
||||
open ComplexConjugate
|
||||
open CKMMatrix
|
||||
|
||||
noncomputable section
|
||||
|
||||
/-- Given four reals `θ₁₂ θ₁₃ θ₂₃ δ₁₃` the standard paramaterization of the CKM matrix
|
||||
as a `3×3` complex matrix. -/
|
||||
def standParamAsMatrix (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : Matrix (Fin 3) (Fin 3) ℂ :=
|
||||
![![Real.cos θ₁₂ * Real.cos θ₁₃, Real.sin θ₁₂ * Real.cos θ₁₃, Real.sin θ₁₃ * exp (-I * δ₁₃)],
|
||||
![(-Real.sin θ₁₂ * Real.cos θ₂₃) - (Real.cos θ₁₂ * Real.sin θ₁₃ * Real.sin θ₂₃ * exp (I * δ₁₃)),
|
||||
Real.cos θ₁₂ * Real.cos θ₂₃ - Real.sin θ₁₂ * Real.sin θ₁₃ * Real.sin θ₂₃ * exp (I * δ₁₃),
|
||||
Real.sin θ₂₃ * Real.cos θ₁₃],
|
||||
![Real.sin θ₁₂ * Real.sin θ₂₃ - Real.cos θ₁₂ * Real.sin θ₁₃ * Real.cos θ₂₃ * exp (I * δ₁₃),
|
||||
(-Real.cos θ₁₂ * Real.sin θ₂₃) - (Real.sin θ₁₂ * Real.sin θ₁₃ * Real.cos θ₂₃ * exp (I * δ₁₃)),
|
||||
Real.cos θ₂₃ * Real.cos θ₁₃]]
|
||||
|
||||
open CKMMatrix
|
||||
|
||||
lemma standParamAsMatrix_unitary (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) :
|
||||
((standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃)ᴴ * standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃) = 1 := by
|
||||
funext j i
|
||||
simp only [standParamAsMatrix, neg_mul, Fin.isValue]
|
||||
rw [mul_apply]
|
||||
have h1 := exp_ne_zero (I * ↑δ₁₃)
|
||||
fin_cases j <;> rw [Fin.sum_univ_three]
|
||||
simp only [Fin.zero_eta, Fin.isValue, conjTranspose_apply, cons_val', cons_val_zero, empty_val',
|
||||
cons_val_fin_one, star_mul', RCLike.star_def, conj_ofReal, cons_val_one, head_cons, star_sub,
|
||||
star_neg, ← exp_conj, _root_.map_mul, conj_I, neg_mul, cons_val_two, tail_cons, head_fin_const]
|
||||
simp [conj_ofReal]
|
||||
rw [exp_neg ]
|
||||
fin_cases i <;> simp
|
||||
· ring_nf
|
||||
field_simp
|
||||
rw [sin_sq, sin_sq, sin_sq]
|
||||
ring
|
||||
· ring_nf
|
||||
field_simp
|
||||
rw [sin_sq, sin_sq]
|
||||
ring
|
||||
· ring_nf
|
||||
field_simp
|
||||
rw [sin_sq]
|
||||
ring
|
||||
simp only [Fin.mk_one, Fin.isValue, conjTranspose_apply, cons_val', cons_val_one, head_cons,
|
||||
empty_val', cons_val_fin_one, cons_val_zero, star_mul', RCLike.star_def, conj_ofReal, star_sub,
|
||||
← exp_conj, _root_.map_mul, conj_I, neg_mul, cons_val_two, tail_cons, head_fin_const, star_neg]
|
||||
simp [conj_ofReal]
|
||||
rw [exp_neg]
|
||||
fin_cases i <;> simp
|
||||
· ring_nf
|
||||
field_simp
|
||||
rw [sin_sq, sin_sq]
|
||||
ring
|
||||
· ring_nf
|
||||
field_simp
|
||||
rw [sin_sq, sin_sq, sin_sq]
|
||||
ring
|
||||
· ring_nf
|
||||
field_simp
|
||||
rw [sin_sq]
|
||||
ring
|
||||
simp only [Fin.reduceFinMk, Fin.isValue, conjTranspose_apply, cons_val', cons_val_two, tail_cons,
|
||||
head_cons, empty_val', cons_val_fin_one, cons_val_zero, star_mul', RCLike.star_def, conj_ofReal,
|
||||
← exp_conj, map_neg, _root_.map_mul, conj_I, neg_mul, neg_neg, cons_val_one, head_fin_const]
|
||||
simp [conj_ofReal]
|
||||
rw [exp_neg]
|
||||
fin_cases i <;> simp
|
||||
· ring_nf
|
||||
rw [sin_sq]
|
||||
ring
|
||||
· ring_nf
|
||||
rw [sin_sq]
|
||||
ring
|
||||
· ring_nf
|
||||
field_simp
|
||||
rw [sin_sq, sin_sq]
|
||||
ring
|
||||
|
||||
/-- Given four reals `θ₁₂ θ₁₃ θ₂₃ δ₁₃` the standard paramaterization of the CKM matrix
|
||||
as a CKM matrix. -/
|
||||
def standParam (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) : CKMMatrix :=
|
||||
⟨standParamAsMatrix θ₁₂ θ₁₃ θ₂₃ δ₁₃, by
|
||||
rw [mem_unitaryGroup_iff']
|
||||
exact standParamAsMatrix_unitary θ₁₂ θ₁₃ θ₂₃ δ₁₃⟩
|
||||
|
||||
namespace standParam
|
||||
lemma cross_product_t (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) :
|
||||
[standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]t =
|
||||
(conj [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]u ×₃ conj [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) := by
|
||||
have h1 := exp_ne_zero (I * ↑δ₁₃)
|
||||
funext i
|
||||
fin_cases i
|
||||
· simp only [tRow, standParam, standParamAsMatrix, neg_mul, exp_neg,
|
||||
Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one, cons_val_two, tail_cons,
|
||||
head_fin_const, cons_val_one, head_cons, Fin.zero_eta, crossProduct, uRow, cRow,
|
||||
LinearMap.mk₂_apply, Pi.conj_apply, _root_.map_mul, map_inv₀, ← exp_conj, conj_I, conj_ofReal,
|
||||
inv_inv, map_sub, map_neg]
|
||||
field_simp
|
||||
ring_nf
|
||||
rw [sin_sq]
|
||||
ring
|
||||
· simp only [tRow, standParam, standParamAsMatrix, neg_mul, exp_neg, Fin.isValue, cons_val',
|
||||
cons_val_zero, empty_val', cons_val_fin_one, cons_val_two, tail_cons, head_fin_const,
|
||||
cons_val_one, head_cons, Fin.mk_one, crossProduct, uRow, cRow, LinearMap.mk₂_apply,
|
||||
Pi.conj_apply, _root_.map_mul, conj_ofReal, map_inv₀, ← exp_conj, conj_I, inv_inv, map_sub,
|
||||
map_neg]
|
||||
field_simp
|
||||
ring_nf
|
||||
rw [sin_sq]
|
||||
ring
|
||||
· simp only [tRow, standParam, standParamAsMatrix, neg_mul, exp_neg, Fin.isValue,
|
||||
cons_val', cons_val_zero, empty_val', cons_val_fin_one, cons_val_two, tail_cons, head_fin_const,
|
||||
cons_val_one, head_cons, Fin.reduceFinMk, crossProduct, uRow, cRow, LinearMap.mk₂_apply,
|
||||
Pi.conj_apply, _root_.map_mul, conj_ofReal, map_inv₀, ← exp_conj, conj_I, inv_inv, map_sub,
|
||||
map_neg]
|
||||
field_simp
|
||||
ring_nf
|
||||
rw [sin_sq]
|
||||
ring
|
||||
|
||||
lemma eq_rows (U : CKMMatrix) {θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ} (hu : [U]u = [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]u)
|
||||
(hc : [U]c = [standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃]c) (hU : [U]t = conj [U]u ×₃ conj [U]c) :
|
||||
U = standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ := by
|
||||
apply ext_Rows hu hc
|
||||
rw [hU, cross_product_t, hu, hc]
|
||||
|
||||
lemma eq_exp_of_phases (θ₁₂ θ₁₃ θ₂₃ δ₁₃ δ₁₃' : ℝ) (h : cexp (δ₁₃ * I) = cexp (δ₁₃' * I)) :
|
||||
standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ = standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃' := by
|
||||
simp [standParam, standParamAsMatrix]
|
||||
apply CKMMatrix_ext
|
||||
simp only
|
||||
rw [show exp (I * δ₁₃) = exp (I * δ₁₃') by rw [mul_comm, h, mul_comm]]
|
||||
rw [show cexp (-(I * ↑δ₁₃)) = cexp (-(I * ↑δ₁₃')) by rw [exp_neg, exp_neg, mul_comm, h, mul_comm]]
|
||||
|
||||
open Invariant in
|
||||
lemma VusVubVcdSq_eq (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤ Real.sin θ₁₂)
|
||||
(h2 : 0 ≤ Real.cos θ₁₃) (h3 : 0 ≤ Real.sin θ₂₃) (h4 : 0 ≤ Real.cos θ₁₂) :
|
||||
VusVubVcdSq ⟦standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃⟧ =
|
||||
Real.sin θ₁₂ ^ 2 * Real.cos θ₁₃ ^ 2 * Real.sin θ₁₃ ^ 2 * Real.sin θ₂₃ ^ 2 := by
|
||||
simp only [VusVubVcdSq, VusAbs, VAbs, VAbs', Fin.isValue, standParam, standParamAsMatrix,
|
||||
neg_mul, Quotient.lift_mk, cons_val', cons_val_one, head_cons,
|
||||
empty_val', cons_val_fin_one, cons_val_zero, _root_.map_mul, VubAbs, cons_val_two, tail_cons,
|
||||
VcbAbs, VudAbs, Complex.abs_ofReal]
|
||||
by_cases hx : Real.cos θ₁₃ ≠ 0
|
||||
· rw [Complex.abs_exp]
|
||||
simp only [neg_re, mul_re, I_re, ofReal_re, zero_mul, I_im, ofReal_im, mul_zero, sub_self,
|
||||
neg_zero, Real.exp_zero, mul_one, _root_.sq_abs]
|
||||
rw [_root_.abs_of_nonneg h1, _root_.abs_of_nonneg h3, _root_.abs_of_nonneg h2,
|
||||
_root_.abs_of_nonneg h4]
|
||||
simp [sq]
|
||||
ring_nf
|
||||
nth_rewrite 2 [Real.sin_sq θ₁₂]
|
||||
ring_nf
|
||||
field_simp
|
||||
ring
|
||||
· simp at hx
|
||||
rw [hx]
|
||||
simp
|
||||
|
||||
open Invariant in
|
||||
lemma mulExpδ₁₃_eq (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤ Real.sin θ₁₂)
|
||||
(h2 : 0 ≤ Real.cos θ₁₃) (h3 : 0 ≤ Real.sin θ₂₃) (h4 : 0 ≤ Real.cos θ₁₂) :
|
||||
mulExpδ₁₃ ⟦standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃⟧ =
|
||||
sin θ₁₂ * cos θ₁₃ ^ 2 * sin θ₂₃ * sin θ₁₃ * cos θ₁₂ * cos θ₂₃ * cexp (I * δ₁₃) := by
|
||||
rw [mulExpδ₁₃, VusVubVcdSq_eq _ _ _ _ h1 h2 h3 h4 ]
|
||||
simp only [jarlskogℂ, standParam, standParamAsMatrix, neg_mul,
|
||||
Quotient.lift_mk, jarlskogℂCKM, Fin.isValue, cons_val', cons_val_one, head_cons,
|
||||
empty_val', cons_val_fin_one, cons_val_zero, cons_val_two, tail_cons, _root_.map_mul, ←
|
||||
exp_conj, map_neg, conj_I, conj_ofReal, neg_neg, map_sub]
|
||||
simp only [ofReal_sin, ofReal_cos, ofReal_mul, ofReal_pow]
|
||||
ring_nf
|
||||
rw [exp_neg]
|
||||
have h1 : cexp (I * δ₁₃) ≠ 0 := exp_ne_zero _
|
||||
field_simp
|
||||
|
||||
|
||||
|
||||
end standParam
|
||||
end
|
||||
|
|
@ -0,0 +1,686 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.FlavorPhysics.CKMMatrix.Basic
|
||||
import HepLean.FlavorPhysics.CKMMatrix.Rows
|
||||
import HepLean.FlavorPhysics.CKMMatrix.PhaseFreedom
|
||||
import HepLean.FlavorPhysics.CKMMatrix.Invariants
|
||||
import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
|
||||
import Mathlib.Analysis.SpecialFunctions.Complex.Arg
|
||||
/-!
|
||||
# Standard parameters for the CKM Matrix
|
||||
|
||||
Given a CKM matrix `V` we can extract four real numbers `θ₁₂`, `θ₁₃`, `θ₂₃` and `δ₁₃`.
|
||||
These, when used in the standard parameterization return `V` up to equivalence.
|
||||
|
||||
This leads to the theorem `standParam.exists_for_CKMatrix` which says that up to equivalence every
|
||||
CKM matrix can be written using the standard parameterization.
|
||||
|
||||
|
||||
-/
|
||||
open Matrix Complex
|
||||
open ComplexConjugate
|
||||
open CKMMatrix
|
||||
|
||||
noncomputable section
|
||||
|
||||
/-- Given a CKM matrix `V` the real number corresponding to `sin θ₁₂` in the
|
||||
standard parameterization. --/
|
||||
def S₁₂ (V : Quotient CKMMatrixSetoid) : ℝ := VusAbs V / (√ (VudAbs V ^ 2 + VusAbs V ^ 2))
|
||||
|
||||
/-- Given a CKM matrix `V` the real number corresponding to `sin θ₁₃` in the
|
||||
standard parameterization. --/
|
||||
def S₁₃ (V : Quotient CKMMatrixSetoid) : ℝ := VubAbs V
|
||||
|
||||
/-- Given a CKM matrix `V` the real number corresponding to `sin θ₂₃` in the
|
||||
standard parameterization. --/
|
||||
def S₂₃ (V : Quotient CKMMatrixSetoid) : ℝ :=
|
||||
if VubAbs V = 1 then VcdAbs V
|
||||
else VcbAbs V / √ (VudAbs V ^ 2 + VusAbs V ^ 2)
|
||||
|
||||
/-- Given a CKM matrix `V` the real number corresponding to `θ₁₂` in the
|
||||
standard parameterization. --/
|
||||
def θ₁₂ (V : Quotient CKMMatrixSetoid) : ℝ := Real.arcsin (S₁₂ V)
|
||||
|
||||
/-- Given a CKM matrix `V` the real number corresponding to `θ₁₃` in the
|
||||
standard parameterization. --/
|
||||
def θ₁₃ (V : Quotient CKMMatrixSetoid) : ℝ := Real.arcsin (S₁₃ V)
|
||||
|
||||
/-- Given a CKM matrix `V` the real number corresponding to `θ₂₃` in the
|
||||
standard parameterization. --/
|
||||
def θ₂₃ (V : Quotient CKMMatrixSetoid) : ℝ := Real.arcsin (S₂₃ V)
|
||||
|
||||
/-- Given a CKM matrix `V` the real number corresponding to `cos θ₁₂` in the
|
||||
standard parameterization. --/
|
||||
def C₁₂ (V : Quotient CKMMatrixSetoid) : ℝ := Real.cos (θ₁₂ V)
|
||||
|
||||
/-- Given a CKM matrix `V` the real number corresponding to `cos θ₁₃` in the
|
||||
standard parameterization. --/
|
||||
def C₁₃ (V : Quotient CKMMatrixSetoid) : ℝ := Real.cos (θ₁₃ V)
|
||||
|
||||
/-- Given a CKM matrix `V` the real number corresponding to `sin θ₂₃` in the
|
||||
standard parameterization. --/
|
||||
def C₂₃ (V : Quotient CKMMatrixSetoid) : ℝ := Real.cos (θ₂₃ V)
|
||||
|
||||
/-- Given a CKM matrix `V` the real number corresponding to the phase `δ₁₃` in the
|
||||
standard parameterization. --/
|
||||
def δ₁₃ (V : Quotient CKMMatrixSetoid) : ℝ :=
|
||||
arg (Invariant.mulExpδ₁₃ V)
|
||||
|
||||
section sines
|
||||
|
||||
lemma S₁₂_nonneg (V : Quotient CKMMatrixSetoid) : 0 ≤ S₁₂ V := by
|
||||
rw [S₁₂, div_nonneg_iff]
|
||||
apply Or.inl
|
||||
apply (And.intro (VAbs_ge_zero 0 1 V) (Real.sqrt_nonneg (VudAbs V ^ 2 + VusAbs V ^ 2)))
|
||||
|
||||
lemma S₁₃_nonneg (V : Quotient CKMMatrixSetoid) : 0 ≤ S₁₃ V :=
|
||||
VAbs_ge_zero 0 2 V
|
||||
|
||||
lemma S₂₃_nonneg (V : Quotient CKMMatrixSetoid) : 0 ≤ S₂₃ V := by
|
||||
by_cases ha : VubAbs V = 1
|
||||
rw [S₂₃, if_pos ha]
|
||||
exact VAbs_ge_zero 1 0 V
|
||||
rw [S₂₃, if_neg ha, @div_nonneg_iff]
|
||||
apply Or.inl
|
||||
apply And.intro (VAbs_ge_zero 1 2 V) (Real.sqrt_nonneg (VudAbs V ^ 2 + VusAbs V ^ 2))
|
||||
|
||||
lemma S₁₂_leq_one (V : Quotient CKMMatrixSetoid) : S₁₂ V ≤ 1 := by
|
||||
rw [S₁₂, @div_le_one_iff]
|
||||
by_cases h1 : √(VudAbs V ^ 2 + VusAbs V ^ 2) = 0
|
||||
simp [h1]
|
||||
have h2 := le_iff_eq_or_lt.mp (Real.sqrt_nonneg (VudAbs V ^ 2 + VusAbs V ^ 2))
|
||||
have h3 : 0 < √(VudAbs V ^ 2 + VusAbs V ^ 2) := by
|
||||
cases' h2 with h2 h2
|
||||
simp_all
|
||||
exact h2
|
||||
apply Or.inl
|
||||
simp_all
|
||||
rw [Real.le_sqrt (VAbs_ge_zero 0 1 V) (le_of_lt h3)]
|
||||
simp only [Fin.isValue, le_add_iff_nonneg_left]
|
||||
exact sq_nonneg (VAbs 0 0 V)
|
||||
|
||||
lemma S₁₃_leq_one (V : Quotient CKMMatrixSetoid) : S₁₃ V ≤ 1 :=
|
||||
VAbs_leq_one 0 2 V
|
||||
|
||||
lemma S₂₃_leq_one (V : Quotient CKMMatrixSetoid) : S₂₃ V ≤ 1 := by
|
||||
by_cases ha : VubAbs V = 1
|
||||
rw [S₂₃, if_pos ha]
|
||||
exact VAbs_leq_one 1 0 V
|
||||
rw [S₂₃, if_neg ha, @div_le_one_iff]
|
||||
by_cases h1 : √(VudAbs V ^ 2 + VusAbs V ^ 2) = 0
|
||||
simp [h1]
|
||||
have h2 := le_iff_eq_or_lt.mp (Real.sqrt_nonneg (VudAbs V ^ 2 + VusAbs V ^ 2))
|
||||
have h3 : 0 < √(VudAbs V ^ 2 + VusAbs V ^ 2) := by
|
||||
cases' h2 with h2 h2
|
||||
simp_all
|
||||
exact h2
|
||||
apply Or.inl
|
||||
simp_all
|
||||
rw [Real.le_sqrt (VAbs_ge_zero 1 2 V) (le_of_lt h3)]
|
||||
rw [VudAbs_sq_add_VusAbs_sq, ← VcbAbs_sq_add_VtbAbs_sq]
|
||||
simp only [Fin.isValue, VcbAbs, VtbAbs, le_add_iff_nonneg_right]
|
||||
exact sq_nonneg (VAbs 2 2 V)
|
||||
|
||||
lemma S₁₂_eq_sin_θ₁₂ (V : Quotient CKMMatrixSetoid) : Real.sin (θ₁₂ V) = S₁₂ V :=
|
||||
Real.sin_arcsin (le_trans (by simp) (S₁₂_nonneg V)) (S₁₂_leq_one V)
|
||||
|
||||
lemma S₁₃_eq_sin_θ₁₃ (V : Quotient CKMMatrixSetoid) : Real.sin (θ₁₃ V) = S₁₃ V :=
|
||||
Real.sin_arcsin (le_trans (by simp) (S₁₃_nonneg V)) (S₁₃_leq_one V)
|
||||
|
||||
lemma S₂₃_eq_sin_θ₂₃ (V : Quotient CKMMatrixSetoid) : Real.sin (θ₂₃ V) = S₂₃ V :=
|
||||
Real.sin_arcsin (le_trans (by simp) (S₂₃_nonneg V)) (S₂₃_leq_one V)
|
||||
|
||||
lemma S₁₂_eq_ℂsin_θ₁₂ (V : Quotient CKMMatrixSetoid) : Complex.sin (θ₁₂ V) = S₁₂ V :=
|
||||
(ofReal_sin _).symm.trans (congrArg ofReal (S₁₂_eq_sin_θ₁₂ V))
|
||||
|
||||
lemma S₁₃_eq_ℂsin_θ₁₃ (V : Quotient CKMMatrixSetoid) : Complex.sin (θ₁₃ V) = S₁₃ V :=
|
||||
(ofReal_sin _).symm.trans (congrArg ofReal (S₁₃_eq_sin_θ₁₃ V))
|
||||
|
||||
lemma S₂₃_eq_ℂsin_θ₂₃ (V : Quotient CKMMatrixSetoid) : Complex.sin (θ₂₃ V) = S₂₃ V :=
|
||||
(ofReal_sin _).symm.trans (congrArg ofReal (S₂₃_eq_sin_θ₂₃ V))
|
||||
|
||||
lemma complexAbs_sin_θ₁₂ (V : Quotient CKMMatrixSetoid) :
|
||||
Complex.abs (Complex.sin (θ₁₂ V)) = sin (θ₁₂ V):= by
|
||||
rw [S₁₂_eq_ℂsin_θ₁₂, Complex.abs_ofReal, ofReal_inj, abs_eq_self]
|
||||
exact S₁₂_nonneg _
|
||||
|
||||
lemma complexAbs_sin_θ₁₃ (V : Quotient CKMMatrixSetoid) :
|
||||
Complex.abs (Complex.sin (θ₁₃ V)) = sin (θ₁₃ V):= by
|
||||
rw [S₁₃_eq_ℂsin_θ₁₃, Complex.abs_ofReal, ofReal_inj, abs_eq_self]
|
||||
exact S₁₃_nonneg _
|
||||
|
||||
lemma complexAbs_sin_θ₂₃ (V : Quotient CKMMatrixSetoid) :
|
||||
Complex.abs (Complex.sin (θ₂₃ V)) = sin (θ₂₃ V):= by
|
||||
rw [S₂₃_eq_ℂsin_θ₂₃, Complex.abs_ofReal, ofReal_inj, abs_eq_self]
|
||||
exact S₂₃_nonneg _
|
||||
|
||||
lemma S₁₂_of_Vub_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) : S₁₂ V = 0 := by
|
||||
have h1 : 1 - VubAbs V ^ 2 = VudAbs V ^ 2 + VusAbs V ^ 2 := by
|
||||
linear_combination - (VAbs_sum_sq_row_eq_one V 0)
|
||||
simp [S₁₂, ← h1, ha]
|
||||
|
||||
lemma S₁₃_of_Vub_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) : S₁₃ V = 1 := by
|
||||
rw [S₁₃, ha]
|
||||
|
||||
lemma S₂₃_of_Vub_eq_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) : S₂₃ V = VcdAbs V := by
|
||||
rw [S₂₃, if_pos ha]
|
||||
|
||||
lemma S₂₃_of_Vub_neq_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V ≠ 1) :
|
||||
S₂₃ V = VcbAbs V / √ (VudAbs V ^ 2 + VusAbs V ^ 2) := by
|
||||
rw [S₂₃, if_neg ha]
|
||||
|
||||
end sines
|
||||
|
||||
section cosines
|
||||
|
||||
lemma C₁₂_eq_ℂcos_θ₁₂ (V : Quotient CKMMatrixSetoid) : Complex.cos (θ₁₂ V) = C₁₂ V := by
|
||||
simp [C₁₂]
|
||||
|
||||
lemma C₁₃_eq_ℂcos_θ₁₃ (V : Quotient CKMMatrixSetoid) : Complex.cos (θ₁₃ V) = C₁₃ V := by
|
||||
simp [C₁₃]
|
||||
|
||||
lemma C₂₃_eq_ℂcos_θ₂₃ (V : Quotient CKMMatrixSetoid) : Complex.cos (θ₂₃ V) = C₂₃ V := by
|
||||
simp [C₂₃]
|
||||
|
||||
lemma complexAbs_cos_θ₁₂ (V : Quotient CKMMatrixSetoid) : Complex.abs (Complex.cos (θ₁₂ V)) =
|
||||
cos (θ₁₂ V):= by
|
||||
rw [C₁₂_eq_ℂcos_θ₁₂, Complex.abs_ofReal]
|
||||
simp only [ofReal_inj, abs_eq_self]
|
||||
exact Real.cos_arcsin_nonneg _
|
||||
|
||||
lemma complexAbs_cos_θ₁₃ (V : Quotient CKMMatrixSetoid) : Complex.abs (Complex.cos (θ₁₃ V)) =
|
||||
cos (θ₁₃ V):= by
|
||||
rw [C₁₃_eq_ℂcos_θ₁₃, Complex.abs_ofReal]
|
||||
simp only [ofReal_inj, abs_eq_self]
|
||||
exact Real.cos_arcsin_nonneg _
|
||||
|
||||
lemma complexAbs_cos_θ₂₃ (V : Quotient CKMMatrixSetoid) : Complex.abs (Complex.cos (θ₂₃ V)) =
|
||||
cos (θ₂₃ V):= by
|
||||
rw [C₂₃_eq_ℂcos_θ₂₃, Complex.abs_ofReal]
|
||||
simp only [ofReal_inj, abs_eq_self]
|
||||
exact Real.cos_arcsin_nonneg _
|
||||
|
||||
lemma S₁₂_sq_add_C₁₂_sq (V : Quotient CKMMatrixSetoid) : S₁₂ V ^ 2 + C₁₂ V ^ 2 = 1 := by
|
||||
rw [← S₁₂_eq_sin_θ₁₂ V, C₁₂]
|
||||
exact Real.sin_sq_add_cos_sq (θ₁₂ V)
|
||||
|
||||
lemma S₁₃_sq_add_C₁₃_sq (V : Quotient CKMMatrixSetoid) : S₁₃ V ^ 2 + C₁₃ V ^ 2 = 1 := by
|
||||
rw [← S₁₃_eq_sin_θ₁₃ V, C₁₃]
|
||||
exact Real.sin_sq_add_cos_sq (θ₁₃ V)
|
||||
|
||||
lemma S₂₃_sq_add_C₂₃_sq (V : Quotient CKMMatrixSetoid) : S₂₃ V ^ 2 + C₂₃ V ^ 2 = 1 := by
|
||||
rw [← S₂₃_eq_sin_θ₂₃ V, C₂₃]
|
||||
exact Real.sin_sq_add_cos_sq (θ₂₃ V)
|
||||
|
||||
lemma C₁₂_of_Vub_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) : C₁₂ V = 1 := by
|
||||
rw [C₁₂, θ₁₂, Real.cos_arcsin, S₁₂_of_Vub_one ha]
|
||||
simp
|
||||
|
||||
lemma C₁₃_of_Vub_eq_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) : C₁₃ V = 0 := by
|
||||
rw [C₁₃, θ₁₃, Real.cos_arcsin, S₁₃, ha]
|
||||
simp
|
||||
|
||||
--rename
|
||||
lemma C₁₂_eq_Vud_div_sqrt {V : Quotient CKMMatrixSetoid} (ha : VubAbs V ≠ 1) :
|
||||
C₁₂ V = VudAbs V / √ (VudAbs V ^ 2 + VusAbs V ^ 2) := by
|
||||
rw [C₁₂, θ₁₂, Real.cos_arcsin, S₁₂, div_pow, Real.sq_sqrt]
|
||||
rw [one_sub_div]
|
||||
simp only [VudAbs, Fin.isValue, VusAbs, add_sub_cancel_right]
|
||||
rw [Real.sqrt_div]
|
||||
rw [Real.sqrt_sq]
|
||||
exact VAbs_ge_zero 0 0 V
|
||||
exact sq_nonneg (VAbs 0 0 V)
|
||||
exact VAbsub_neq_zero_Vud_Vus_neq_zero ha
|
||||
exact (Left.add_nonneg (sq_nonneg (VAbs 0 0 V)) (sq_nonneg (VAbs 0 1 V)))
|
||||
|
||||
--rename
|
||||
lemma C₁₃_eq_add_sq (V : Quotient CKMMatrixSetoid) : C₁₃ V = √ (VudAbs V ^ 2 + VusAbs V ^ 2) := by
|
||||
rw [C₁₃, θ₁₃, Real.cos_arcsin, S₁₃]
|
||||
have h1 : 1 - VubAbs V ^ 2 = VudAbs V ^ 2 + VusAbs V ^ 2 := by
|
||||
linear_combination - (VAbs_sum_sq_row_eq_one V 0)
|
||||
rw [h1]
|
||||
|
||||
lemma C₂₃_of_Vub_neq_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V ≠ 1) :
|
||||
C₂₃ V = VtbAbs V / √ (VudAbs V ^ 2 + VusAbs V ^ 2) := by
|
||||
rw [C₂₃, θ₂₃, Real.cos_arcsin, S₂₃_of_Vub_neq_one ha, div_pow, Real.sq_sqrt]
|
||||
rw [VudAbs_sq_add_VusAbs_sq, ← VcbAbs_sq_add_VtbAbs_sq]
|
||||
rw [one_sub_div]
|
||||
simp only [VcbAbs, Fin.isValue, VtbAbs, add_sub_cancel_left]
|
||||
rw [Real.sqrt_div (sq_nonneg (VAbs 2 2 V))]
|
||||
rw [Real.sqrt_sq (VAbs_ge_zero 2 2 V)]
|
||||
rw [VcbAbs_sq_add_VtbAbs_sq, ← VudAbs_sq_add_VusAbs_sq ]
|
||||
exact VAbsub_neq_zero_Vud_Vus_neq_zero ha
|
||||
exact (Left.add_nonneg (sq_nonneg (VAbs 0 0 V)) (sq_nonneg (VAbs 0 1 V)))
|
||||
|
||||
end cosines
|
||||
|
||||
section VAbs
|
||||
|
||||
-- rename to VudAbs_standard_param
|
||||
lemma VudAbs_eq_C₁₂_mul_C₁₃ (V : Quotient CKMMatrixSetoid) : VudAbs V = C₁₂ V * C₁₃ V := by
|
||||
by_cases ha : VubAbs V = 1
|
||||
change VAbs 0 0 V = C₁₂ V * C₁₃ V
|
||||
rw [VAbs_thd_eq_one_fst_eq_zero ha]
|
||||
rw [C₁₃, θ₁₃, Real.cos_arcsin, S₁₃, ha]
|
||||
simp only [one_pow, sub_self, Real.sqrt_zero, mul_zero]
|
||||
rw [C₁₂_eq_Vud_div_sqrt ha, C₁₃, θ₁₃, Real.cos_arcsin, S₁₃]
|
||||
have h1 : 1 - VubAbs V ^ 2 = VudAbs V ^ 2 + VusAbs V ^ 2 := by
|
||||
linear_combination - (VAbs_sum_sq_row_eq_one V 0)
|
||||
rw [h1, mul_comm]
|
||||
exact (mul_div_cancel₀ (VudAbs V) (VAbsub_neq_zero_sqrt_Vud_Vus_neq_zero ha)).symm
|
||||
|
||||
lemma VusAbs_eq_S₁₂_mul_C₁₃ (V : Quotient CKMMatrixSetoid) : VusAbs V = S₁₂ V * C₁₃ V := by
|
||||
rw [C₁₃, θ₁₃, Real.cos_arcsin, S₁₂, S₁₃]
|
||||
have h1 : 1 - VubAbs V ^ 2 = VudAbs V ^ 2 + VusAbs V ^ 2 := by
|
||||
linear_combination - (VAbs_sum_sq_row_eq_one V 0)
|
||||
rw [h1]
|
||||
rw [mul_comm]
|
||||
by_cases ha : VubAbs V = 1
|
||||
rw [ha] at h1
|
||||
simp only [one_pow, sub_self, Fin.isValue] at h1
|
||||
rw [← h1]
|
||||
simp only [Real.sqrt_zero, div_zero, mul_zero]
|
||||
exact VAbs_thd_eq_one_snd_eq_zero ha
|
||||
have h2 := VAbsub_neq_zero_sqrt_Vud_Vus_neq_zero ha
|
||||
exact (mul_div_cancel₀ (VusAbs V) h2).symm
|
||||
|
||||
lemma VubAbs_eq_S₁₃ (V : Quotient CKMMatrixSetoid) : VubAbs V = S₁₃ V := rfl
|
||||
|
||||
lemma VcbAbs_eq_S₂₃_mul_C₁₃ (V : Quotient CKMMatrixSetoid) : VcbAbs V = S₂₃ V * C₁₃ V := by
|
||||
by_cases ha : VubAbs V = 1
|
||||
rw [C₁₃_of_Vub_eq_one ha]
|
||||
simp only [VcbAbs, Fin.isValue, mul_zero]
|
||||
exact VAbs_fst_col_eq_one_snd_eq_zero ha
|
||||
rw [S₂₃_of_Vub_neq_one ha, C₁₃_eq_add_sq]
|
||||
rw [mul_comm]
|
||||
exact (mul_div_cancel₀ (VcbAbs V) (VAbsub_neq_zero_sqrt_Vud_Vus_neq_zero ha)).symm
|
||||
|
||||
lemma VtbAbs_eq_C₂₃_mul_C₁₃ (V : Quotient CKMMatrixSetoid) : VtbAbs V = C₂₃ V * C₁₃ V := by
|
||||
by_cases ha : VubAbs V = 1
|
||||
rw [C₁₃_of_Vub_eq_one ha]
|
||||
simp only [VtbAbs, Fin.isValue, mul_zero]
|
||||
exact VAbs_fst_col_eq_one_thd_eq_zero ha
|
||||
rw [C₂₃_of_Vub_neq_one ha, C₁₃_eq_add_sq]
|
||||
rw [mul_comm]
|
||||
exact (mul_div_cancel₀ (VtbAbs V) (VAbsub_neq_zero_sqrt_Vud_Vus_neq_zero ha)).symm
|
||||
|
||||
lemma VubAbs_of_cos_θ₁₃_zero {V : Quotient CKMMatrixSetoid} (h1 : Real.cos (θ₁₃ V) = 0) :
|
||||
VubAbs V = 1 := by
|
||||
rw [θ₁₃, Real.cos_arcsin, ← VubAbs_eq_S₁₃, Real.sqrt_eq_zero] at h1
|
||||
have h2 : VubAbs V ^ 2 = 1 := by linear_combination -(1 * h1)
|
||||
simp at h2
|
||||
cases' h2 with h2 h2
|
||||
exact h2
|
||||
have h3 := VAbs_ge_zero 0 2 V
|
||||
rw [h2] at h3
|
||||
simp at h3
|
||||
linarith
|
||||
simp only [VubAbs, Fin.isValue, sub_nonneg, sq_le_one_iff_abs_le_one]
|
||||
rw [_root_.abs_of_nonneg (VAbs_ge_zero 0 2 V)]
|
||||
exact VAbs_leq_one 0 2 V
|
||||
|
||||
lemma Vs_zero_iff_cos_sin_zero (V : CKMMatrix) :
|
||||
VudAbs ⟦V⟧ = 0 ∨ VubAbs ⟦V⟧ = 0 ∨ VusAbs ⟦V⟧ = 0 ∨ VcbAbs ⟦V⟧ = 0 ∨ VtbAbs ⟦V⟧ = 0
|
||||
↔ Real.cos (θ₁₂ ⟦V⟧) = 0 ∨ Real.cos (θ₁₃ ⟦V⟧) = 0 ∨ Real.cos (θ₂₃ ⟦V⟧) = 0 ∨
|
||||
Real.sin (θ₁₂ ⟦V⟧) = 0 ∨ Real.sin (θ₁₃ ⟦V⟧) = 0 ∨ Real.sin (θ₂₃ ⟦V⟧) = 0 := by
|
||||
rw [VudAbs_eq_C₁₂_mul_C₁₃, VubAbs_eq_S₁₃, VusAbs_eq_S₁₂_mul_C₁₃, VcbAbs_eq_S₂₃_mul_C₁₃,
|
||||
VtbAbs_eq_C₂₃_mul_C₁₃]
|
||||
rw [C₁₂, C₁₃, C₂₃, S₁₂_eq_sin_θ₁₂, S₂₃_eq_sin_θ₂₃, S₁₃_eq_sin_θ₁₃]
|
||||
aesop
|
||||
|
||||
end VAbs
|
||||
|
||||
|
||||
namespace standParam
|
||||
open Invariant
|
||||
|
||||
lemma mulExpδ₁₃_on_param_δ₁₃ (V : CKMMatrix) (δ₁₃ : ℝ) :
|
||||
mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ =
|
||||
sin (θ₁₂ ⟦V⟧) * cos (θ₁₃ ⟦V⟧) ^ 2 * sin (θ₂₃ ⟦V⟧) * sin (θ₁₃ ⟦V⟧)
|
||||
* cos (θ₁₂ ⟦V⟧) * cos (θ₂₃ ⟦V⟧) * cexp (I * δ₁₃) := by
|
||||
refine mulExpδ₁₃_eq _ _ _ _ ?_ ?_ ?_ ?_
|
||||
rw [S₁₂_eq_sin_θ₁₂]
|
||||
exact S₁₂_nonneg _
|
||||
exact Real.cos_arcsin_nonneg _
|
||||
rw [S₂₃_eq_sin_θ₂₃]
|
||||
exact S₂₃_nonneg _
|
||||
exact Real.cos_arcsin_nonneg _
|
||||
|
||||
lemma mulExpδ₁₃_on_param_eq_zero_iff (V : CKMMatrix) (δ₁₃ : ℝ) :
|
||||
mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ = 0 ↔
|
||||
VudAbs ⟦V⟧ = 0 ∨ VubAbs ⟦V⟧ = 0 ∨ VusAbs ⟦V⟧ = 0 ∨ VcbAbs ⟦V⟧ = 0 ∨ VtbAbs ⟦V⟧ = 0 := by
|
||||
rw [VudAbs_eq_C₁₂_mul_C₁₃, VubAbs_eq_S₁₃, VusAbs_eq_S₁₂_mul_C₁₃, VcbAbs_eq_S₂₃_mul_C₁₃,
|
||||
VtbAbs_eq_C₂₃_mul_C₁₃, ← ofReal_inj,
|
||||
← ofReal_inj, ← ofReal_inj, ← ofReal_inj, ← ofReal_inj]
|
||||
simp only [ofReal_mul]
|
||||
rw [← S₁₃_eq_ℂsin_θ₁₃, ← S₁₂_eq_ℂsin_θ₁₂, ← S₂₃_eq_ℂsin_θ₂₃,
|
||||
← C₁₃_eq_ℂcos_θ₁₃, ← C₂₃_eq_ℂcos_θ₂₃,← C₁₂_eq_ℂcos_θ₁₂]
|
||||
rw [mulExpδ₁₃_on_param_δ₁₃]
|
||||
simp only [mul_eq_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff,
|
||||
ofReal_zero]
|
||||
have h1 := exp_ne_zero (I * δ₁₃)
|
||||
simp_all
|
||||
aesop
|
||||
|
||||
lemma mulExpδ₁₃_on_param_abs (V : CKMMatrix) (δ₁₃ : ℝ) :
|
||||
Complex.abs (mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧) =
|
||||
sin (θ₁₂ ⟦V⟧) * cos (θ₁₃ ⟦V⟧) ^ 2 * sin (θ₂₃ ⟦V⟧) * sin (θ₁₃ ⟦V⟧)
|
||||
* cos (θ₁₂ ⟦V⟧) * cos (θ₂₃ ⟦V⟧) := by
|
||||
rw [mulExpδ₁₃_on_param_δ₁₃]
|
||||
simp [abs_exp]
|
||||
rw [complexAbs_sin_θ₁₃, complexAbs_cos_θ₁₃, complexAbs_sin_θ₁₂, complexAbs_cos_θ₁₂,
|
||||
complexAbs_sin_θ₂₃, complexAbs_cos_θ₂₃]
|
||||
|
||||
lemma mulExpδ₁₃_on_param_neq_zero_arg (V : CKMMatrix) (δ₁₃ : ℝ)
|
||||
(h1 : mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ ≠ 0 ) :
|
||||
cexp (arg ( mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ ) * I) =
|
||||
cexp (δ₁₃ * I) := by
|
||||
have h1a := mulExpδ₁₃_on_param_δ₁₃ V δ₁₃
|
||||
have habs := mulExpδ₁₃_on_param_abs V δ₁₃
|
||||
have h2 : mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ = Complex.abs
|
||||
(mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧) * exp (δ₁₃ * I) := by
|
||||
rw [habs, h1a]
|
||||
ring_nf
|
||||
nth_rewrite 1 [← abs_mul_exp_arg_mul_I (mulExpδ₁₃
|
||||
⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ )] at h2
|
||||
have habs_neq_zero :
|
||||
(Complex.abs (mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧) : ℂ) ≠ 0 := by
|
||||
simp only [ne_eq, ofReal_eq_zero, map_eq_zero]
|
||||
exact h1
|
||||
rw [← mul_right_inj' habs_neq_zero]
|
||||
rw [← h2]
|
||||
|
||||
lemma on_param_cos_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₁₃ ⟦V⟧) = 0) :
|
||||
standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
|
||||
have hS13 := congrArg ofReal (S₁₃_of_Vub_one (VubAbs_of_cos_θ₁₃_zero h))
|
||||
simp [← S₁₃_eq_ℂsin_θ₁₃] at hS13
|
||||
have hC12 := congrArg ofReal (C₁₂_of_Vub_one (VubAbs_of_cos_θ₁₃_zero h))
|
||||
simp [← C₁₂_eq_ℂcos_θ₁₂] at hC12
|
||||
have hS12 := congrArg ofReal (S₁₂_of_Vub_one (VubAbs_of_cos_θ₁₃_zero h))
|
||||
simp [← S₁₂_eq_ℂsin_θ₁₂] at hS12
|
||||
use 0, 0, 0, δ₁₃, 0, -δ₁₃
|
||||
simp [standParam, standParamAsMatrix, h, phaseShift, hS13, hC12, hS12]
|
||||
funext i j
|
||||
fin_cases i <;> fin_cases j <;>
|
||||
simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three]
|
||||
rfl
|
||||
rfl
|
||||
|
||||
|
||||
lemma on_param_cos_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₁₂ ⟦V⟧) = 0) :
|
||||
standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
|
||||
use 0, δ₁₃, δ₁₃, -δ₁₃, 0, - δ₁₃
|
||||
have hb := exp_ne_zero (I * δ₁₃)
|
||||
simp [standParam, standParamAsMatrix, h, phaseShift, exp_neg]
|
||||
funext i j
|
||||
fin_cases i <;> fin_cases j <;>
|
||||
simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three]
|
||||
apply Or.inr
|
||||
rfl
|
||||
change _ = _ + _ * 0
|
||||
simp only [mul_zero, add_zero, neg_inj]
|
||||
field_simp
|
||||
ring
|
||||
ring
|
||||
field_simp
|
||||
ring
|
||||
change _ = _ + _ * 0
|
||||
simp only [mul_zero, add_zero]
|
||||
field_simp
|
||||
ring
|
||||
ring
|
||||
field_simp
|
||||
ring
|
||||
|
||||
lemma on_param_cos_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₂₃ ⟦V⟧) = 0) :
|
||||
standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
|
||||
use 0, δ₁₃, 0, 0, 0, - δ₁₃
|
||||
have hb := exp_ne_zero (I * δ₁₃)
|
||||
simp [standParam, standParamAsMatrix, h, phaseShift, exp_neg]
|
||||
funext i j
|
||||
fin_cases i <;> fin_cases j <;>
|
||||
simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three]
|
||||
apply Or.inr
|
||||
rfl
|
||||
ring_nf
|
||||
change _ = _ + _ * 0
|
||||
simp only [mul_zero, add_zero]
|
||||
ring
|
||||
field_simp
|
||||
ring
|
||||
|
||||
lemma on_param_sin_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₁₃ ⟦V⟧) = 0) :
|
||||
standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
|
||||
use 0, 0, 0, 0, 0, 0
|
||||
simp [standParam, standParamAsMatrix, h, phaseShift, exp_neg]
|
||||
funext i j
|
||||
fin_cases i <;> fin_cases j <;>
|
||||
simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three]
|
||||
apply Or.inr
|
||||
rfl
|
||||
apply Or.inr
|
||||
rfl
|
||||
|
||||
lemma on_param_sin_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₁₂ ⟦V⟧) = 0) :
|
||||
standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
|
||||
use 0, δ₁₃, δ₁₃, 0, -δ₁₃, - δ₁₃
|
||||
have hb := exp_ne_zero (I * δ₁₃)
|
||||
simp [standParam, standParamAsMatrix, h, phaseShift, exp_neg]
|
||||
funext i j
|
||||
fin_cases i <;> fin_cases j <;>
|
||||
simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three]
|
||||
apply Or.inr
|
||||
rfl
|
||||
change _ = _ + _ * 0
|
||||
simp only [mul_zero, add_zero, neg_inj]
|
||||
ring
|
||||
field_simp
|
||||
ring
|
||||
field_simp
|
||||
ring
|
||||
change _ = _ + _ * 0
|
||||
simp only [mul_zero, add_zero, neg_inj]
|
||||
ring
|
||||
field_simp
|
||||
ring
|
||||
field_simp
|
||||
ring
|
||||
|
||||
|
||||
lemma on_param_sin_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₂₃ ⟦V⟧) = 0) :
|
||||
standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
|
||||
use 0, 0, δ₁₃, 0, 0, - δ₁₃
|
||||
have hb := exp_ne_zero (I * δ₁₃)
|
||||
simp [standParam, standParamAsMatrix, h, phaseShift, exp_neg]
|
||||
funext i j
|
||||
fin_cases i <;> fin_cases j <;>
|
||||
simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three]
|
||||
apply Or.inr
|
||||
rfl
|
||||
change _ = _ + _ * 0
|
||||
simp only [mul_zero, add_zero, neg_inj]
|
||||
ring
|
||||
ring
|
||||
field_simp
|
||||
ring
|
||||
|
||||
|
||||
|
||||
lemma eq_standParam_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0)
|
||||
(hV : fstRowThdColRealCond V) : V = standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) (- arg [V]ub) := by
|
||||
have hb' : VubAbs ⟦V⟧ ≠ 1 := by
|
||||
rw [ud_us_neq_zero_iff_ub_neq_one] at hb
|
||||
simp [VAbs, hb]
|
||||
have h1 : ofReal (√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) *
|
||||
↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2)) = ofReal ((VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) ) := by
|
||||
rw [Real.mul_self_sqrt ]
|
||||
apply add_nonneg (sq_nonneg _) (sq_nonneg _)
|
||||
simp at h1
|
||||
have hx := Vabs_sq_add_neq_zero hb
|
||||
refine eq_rows V ?_ ?_ hV.2.2.2.2
|
||||
funext i
|
||||
fin_cases i
|
||||
simp only [uRow, Fin.isValue, Fin.zero_eta, cons_val_zero, standParam, standParamAsMatrix,
|
||||
ofReal_cos, ofReal_sin, ofReal_neg, mul_neg, neg_mul, neg_neg, cons_val', empty_val',
|
||||
cons_val_fin_one, cons_val_one, head_cons, cons_val_two, tail_cons]
|
||||
rw [hV.1, VudAbs_eq_C₁₂_mul_C₁₃ ⟦V⟧]
|
||||
simp [C₁₂, C₁₃]
|
||||
simp [uRow, standParam, standParamAsMatrix]
|
||||
rw [hV.2.1, VusAbs_eq_S₁₂_mul_C₁₃ ⟦V⟧, ← S₁₂_eq_sin_θ₁₂ ⟦V⟧, C₁₃]
|
||||
simp only [ofReal_mul, ofReal_sin, ofReal_cos]
|
||||
simp [uRow, standParam, standParamAsMatrix]
|
||||
nth_rewrite 1 [← abs_mul_exp_arg_mul_I (V.1 0 2)]
|
||||
rw [show Complex.abs (V.1 0 2) = VubAbs ⟦V⟧ from rfl]
|
||||
rw [VubAbs_eq_S₁₃, ← S₁₃_eq_sin_θ₁₃ ⟦V⟧]
|
||||
simp only [ofReal_sin, Fin.isValue, mul_eq_mul_left_iff]
|
||||
ring_nf
|
||||
simp only [true_or]
|
||||
funext i
|
||||
fin_cases i
|
||||
simp [cRow, standParam, standParamAsMatrix]
|
||||
rw [cd_of_fstRowThdColRealCond hb hV]
|
||||
rw [S₁₂_eq_ℂsin_θ₁₂ ⟦V⟧, S₁₂, C₁₂_eq_ℂcos_θ₁₂ ⟦V⟧, C₁₂_eq_Vud_div_sqrt hb']
|
||||
rw [S₂₃_eq_ℂsin_θ₂₃ ⟦V⟧, S₂₃_of_Vub_neq_one hb', C₂₃_eq_ℂcos_θ₂₃ ⟦V⟧,
|
||||
C₂₃_of_Vub_neq_one hb', S₁₃_eq_ℂsin_θ₁₃ ⟦V⟧, S₁₃]
|
||||
field_simp
|
||||
rw [h1]
|
||||
simp [sq]
|
||||
field_simp
|
||||
ring_nf
|
||||
simp [cRow, standParam, standParamAsMatrix]
|
||||
rw [C₁₂_eq_ℂcos_θ₁₂ ⟦V⟧, C₂₃_eq_ℂcos_θ₂₃ ⟦V⟧, S₁₂_eq_ℂsin_θ₁₂ ⟦V⟧,
|
||||
S₁₃_eq_ℂsin_θ₁₃ ⟦V⟧, S₂₃_eq_ℂsin_θ₂₃ ⟦V⟧]
|
||||
rw [C₁₂_eq_Vud_div_sqrt hb', C₂₃_of_Vub_neq_one hb', S₁₂, S₁₃, S₂₃_of_Vub_neq_one hb']
|
||||
rw [cs_of_fstRowThdColRealCond hb hV]
|
||||
field_simp
|
||||
rw [h1]
|
||||
simp [sq]
|
||||
field_simp
|
||||
ring_nf
|
||||
simp [cRow, standParam, standParamAsMatrix]
|
||||
rw [hV.2.2.1]
|
||||
rw [VcbAbs_eq_S₂₃_mul_C₁₃ ⟦V⟧, S₂₃_eq_ℂsin_θ₂₃ ⟦V⟧, C₁₃]
|
||||
simp
|
||||
|
||||
|
||||
lemma eq_standParam_of_ubOnePhaseCond {V : CKMMatrix} (hV : ubOnePhaseCond V) :
|
||||
V = standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
|
||||
have h1 : VubAbs ⟦V⟧ = 1 := by
|
||||
simp [VAbs]
|
||||
rw [hV.2.2.2.1]
|
||||
simp
|
||||
refine eq_rows V ?_ ?_ hV.2.2.2.2.1
|
||||
funext i
|
||||
fin_cases i
|
||||
simp [uRow, standParam, standParamAsMatrix]
|
||||
rw [C₁₃_eq_ℂcos_θ₁₃ ⟦V⟧, C₁₃_of_Vub_eq_one h1, hV.1]
|
||||
simp only [ofReal_zero, mul_zero]
|
||||
simp [uRow, standParam, standParamAsMatrix]
|
||||
rw [C₁₃_eq_ℂcos_θ₁₃ ⟦V⟧, C₁₃_of_Vub_eq_one h1, hV.2.1]
|
||||
simp only [ofReal_zero, mul_zero]
|
||||
simp [uRow, standParam, standParamAsMatrix]
|
||||
rw [S₁₃_eq_ℂsin_θ₁₃ ⟦V⟧, S₁₃]
|
||||
simp [VAbs]
|
||||
rw [hV.2.2.2.1]
|
||||
simp only [_root_.map_one, ofReal_one]
|
||||
funext i
|
||||
fin_cases i
|
||||
simp [cRow, standParam, standParamAsMatrix]
|
||||
rw [S₂₃_eq_ℂsin_θ₂₃ ⟦V⟧, S₂₃_of_Vub_eq_one h1]
|
||||
rw [S₁₂_eq_ℂsin_θ₁₂ ⟦V⟧, S₁₂_of_Vub_one h1]
|
||||
rw [C₁₂_eq_ℂcos_θ₁₂ ⟦V⟧, C₁₂_of_Vub_one h1]
|
||||
rw [S₁₃_eq_ℂsin_θ₁₃ ⟦V⟧, S₁₃_of_Vub_one h1]
|
||||
rw [hV.2.2.2.2.2.1]
|
||||
simp only [VcdAbs, Fin.isValue, ofReal_zero, zero_mul, neg_zero, ofReal_one, mul_one, one_mul,
|
||||
zero_sub]
|
||||
simp [cRow, standParam, standParamAsMatrix]
|
||||
rw [S₂₃_eq_ℂsin_θ₂₃ ⟦V⟧, S₂₃_of_Vub_eq_one h1]
|
||||
rw [S₁₂_eq_ℂsin_θ₁₂ ⟦V⟧, S₁₂_of_Vub_one h1]
|
||||
rw [C₁₂_eq_ℂcos_θ₁₂ ⟦V⟧, C₁₂_of_Vub_one h1]
|
||||
rw [S₁₃_eq_ℂsin_θ₁₃ ⟦V⟧, S₁₃_of_Vub_one h1]
|
||||
simp only [Fin.isValue, ofReal_one, one_mul, ofReal_zero, mul_one, VcdAbs, zero_mul, sub_zero]
|
||||
have h3 : (Real.cos (θ₂₃ ⟦V⟧) : ℂ) = √(1 - S₂₃ ⟦V⟧ ^ 2) := by
|
||||
rw [θ₂₃, Real.cos_arcsin]
|
||||
simp at h3
|
||||
rw [h3, S₂₃_of_Vub_eq_one h1, hV.2.2.2.2.2.2]
|
||||
simp [cRow, standParam, standParamAsMatrix]
|
||||
rw [C₁₃_eq_ℂcos_θ₁₃ ⟦V⟧, C₁₃_of_Vub_eq_one h1, hV.2.2.1]
|
||||
simp
|
||||
|
||||
|
||||
theorem exists_δ₁₃ (V : CKMMatrix) :
|
||||
∃ (δ₃ : ℝ), V ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₃ := by
|
||||
obtain ⟨U, hU⟩ := fstRowThdColRealCond_holds_up_to_equiv V
|
||||
have hUV : ⟦U⟧ = ⟦V⟧ := (Quotient.eq.mpr (phaseShiftEquivRelation.symm hU.1))
|
||||
by_cases ha : [V]ud ≠ 0 ∨ [V]us ≠ 0
|
||||
· have haU : [U]ud ≠ 0 ∨ [U]us ≠ 0 := by -- should be much simplier
|
||||
by_contra hn
|
||||
simp [not_or] at hn
|
||||
have hna : VudAbs ⟦U⟧ = 0 ∧ VusAbs ⟦U⟧ =0 := by
|
||||
simp [VAbs]
|
||||
exact hn
|
||||
rw [hUV] at hna
|
||||
simp [VAbs] at hna
|
||||
simp_all
|
||||
have hU' := eq_standParam_of_fstRowThdColRealCond haU hU.2
|
||||
rw [hU'] at hU
|
||||
use (- arg ([U]ub))
|
||||
rw [← hUV]
|
||||
exact hU.1
|
||||
· have haU : ¬ ([U]ud ≠ 0 ∨ [U]us ≠ 0) := by -- should be much simplier
|
||||
simp [not_or] at ha
|
||||
have h1 : VudAbs ⟦U⟧ = 0 ∧ VusAbs ⟦U⟧ = 0 := by
|
||||
rw [hUV]
|
||||
simp [VAbs]
|
||||
exact ha
|
||||
simpa [not_or, VAbs] using h1
|
||||
have ⟨U2, hU2⟩ := ubOnePhaseCond_hold_up_to_equiv_of_ub_one haU hU.2
|
||||
have hUVa2 : V ≈ U2 := phaseShiftEquivRelation.trans hU.1 hU2.1
|
||||
have hUV2 : ⟦U2⟧ = ⟦V⟧ := (Quotient.eq.mpr (phaseShiftEquivRelation.symm hUVa2))
|
||||
have hx := eq_standParam_of_ubOnePhaseCond hU2.2
|
||||
use 0
|
||||
rw [← hUV2, ← hx]
|
||||
exact hUVa2
|
||||
|
||||
open Invariant in
|
||||
theorem eq_standardParameterization_δ₃ (V : CKMMatrix) :
|
||||
V ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) (δ₁₃ ⟦V⟧) := by
|
||||
obtain ⟨δ₁₃', hδ₃⟩ := exists_δ₁₃ V
|
||||
have hSV := (Quotient.eq.mpr (hδ₃))
|
||||
by_cases h : Invariant.mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃'⟧ ≠ 0
|
||||
have h2 := eq_exp_of_phases (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃'
|
||||
(δ₁₃ ⟦V⟧) (by rw [← mulExpδ₁₃_on_param_neq_zero_arg V δ₁₃' h, ← hSV, δ₁₃, Invariant.mulExpδ₁₃])
|
||||
rw [h2] at hδ₃
|
||||
exact hδ₃
|
||||
simp at h
|
||||
have h1 : δ₁₃ ⟦V⟧ = 0 := by
|
||||
rw [hSV, δ₁₃, h]
|
||||
simp
|
||||
rw [h1]
|
||||
rw [mulExpδ₁₃_on_param_eq_zero_iff, Vs_zero_iff_cos_sin_zero] at h
|
||||
refine phaseShiftEquivRelation.trans hδ₃ ?_
|
||||
rcases h with h | h | h | h | h | h
|
||||
exact on_param_cos_θ₁₂_eq_zero δ₁₃' h
|
||||
exact on_param_cos_θ₁₃_eq_zero δ₁₃' h
|
||||
exact on_param_cos_θ₂₃_eq_zero δ₁₃' h
|
||||
exact on_param_sin_θ₁₂_eq_zero δ₁₃' h
|
||||
exact on_param_sin_θ₁₃_eq_zero δ₁₃' h
|
||||
exact on_param_sin_θ₂₃_eq_zero δ₁₃' h
|
||||
|
||||
|
||||
theorem exists_for_CKMatrix (V : CKMMatrix) :
|
||||
∃ (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ), V ≈ standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ := by
|
||||
use θ₁₂ ⟦V⟧, θ₁₃ ⟦V⟧, θ₂₃ ⟦V⟧, δ₁₃ ⟦V⟧
|
||||
exact eq_standardParameterization_δ₃ V
|
||||
|
||||
end standParam
|
||||
|
||||
|
||||
open CKMMatrix
|
||||
|
||||
|
||||
|
||||
end
|
||||
Loading…
Add table
Add a link
Reference in a new issue