DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor: More simps

Browse source
This commit is contained in:
jstoobysmith 2024-10-12 08:42:20 +00:00
parent 4a396783ab
commit 269f4d53a7
16 changed files with 139 additions and 62 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
View file

@ -121,7 +121,7 @@ theorem linesInPlane_constAbs {S : (PureU1 (n.succ.succ.succ.succ.succ)).LinSols
lemma linesInPlane_four (S : (PureU1 4).Sols) (hS : LineInPlaneCond S.1.1) :
ConstAbsProp (S.val (0 : Fin 4), S.val (1 : Fin 4)) := by
simp [ConstAbsProp]
simp only [ConstAbsProp, Fin.isValue]
by_contra hn
have hLin := pureU1_linear S.1.1
have hcube := pureU1_cube S

25
HepLean/AnomalyCancellation/SMNu/Basic.lean
View file

@ -93,13 +93,15 @@ def accGrav : (SMνCharges n).Charges →ₗ[ℚ] ℚ where
map_add' S T := by
simp only
repeat rw [map_add]
simp [Pi.add_apply, mul_add]
simp only [SMνSpecies_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply,
Fin.isValue, mul_add]
repeat erw [Finset.sum_add_distrib]
ring
map_smul' a S := by
simp only
repeat erw [map_smul]
simp [HSMul.hSMul, SMul.smul]
simp only [SMνSpecies_numberCharges, HSMul.hSMul, SMul.smul, toSpecies_apply, Fin.isValue,
eq_ratCast, Rat.cast_eq_id, id_eq]
repeat erw [Finset.sum_add_distrib]
repeat erw [← Finset.mul_sum]
-- rw [show Rat.cast a = a from rfl]
@ -127,13 +129,15 @@ def accSU2 : (SMνCharges n).Charges →ₗ[ℚ] ℚ where
map_add' S T := by
simp only
repeat rw [map_add]
simp [Pi.add_apply, mul_add]
simp only [SMνSpecies_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply,
Fin.isValue, mul_add]
repeat erw [Finset.sum_add_distrib]
ring
map_smul' a S := by
simp only
repeat erw [map_smul]
simp [HSMul.hSMul, SMul.smul]
simp only [SMνSpecies_numberCharges, HSMul.hSMul, SMul.smul, toSpecies_apply, Fin.isValue,
eq_ratCast, Rat.cast_eq_id, id_eq]
repeat erw [Finset.sum_add_distrib]
repeat erw [← Finset.mul_sum]
-- rw [show Rat.cast a = a from rfl]
@ -160,13 +164,15 @@ def accSU3 : (SMνCharges n).Charges →ₗ[ℚ] ℚ where
map_add' S T := by
simp only
repeat rw [map_add]
simp [Pi.add_apply, mul_add]
simp only [SMνSpecies_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply,
Fin.isValue, mul_add]
repeat erw [Finset.sum_add_distrib]
ring
map_smul' a S := by
simp only
repeat erw [map_smul]
simp [HSMul.hSMul, SMul.smul]
simp only [SMνSpecies_numberCharges, HSMul.hSMul, SMul.smul, toSpecies_apply, Fin.isValue,
eq_ratCast, Rat.cast_eq_id, id_eq]
repeat erw [Finset.sum_add_distrib]
repeat erw [← Finset.mul_sum]
-- rw [show Rat.cast a = a from rfl]
@ -201,7 +207,8 @@ def accYY : (SMνCharges n).Charges →ₗ[ℚ] ℚ where
map_smul' a S := by
simp only
repeat erw [map_smul]
simp [HSMul.hSMul, SMul.smul]
simp only [SMνSpecies_numberCharges, HSMul.hSMul, SMul.smul, toSpecies_apply, Fin.isValue,
eq_ratCast, Rat.cast_eq_id, id_eq]
repeat erw [Finset.sum_add_distrib]
repeat erw [← Finset.mul_sum]
-- rw [show Rat.cast a = a from rfl]
@ -235,7 +242,7 @@ def quadBiLin : BiLinearSymm (SMνCharges n).Charges := BiLinearSymm.mk₂
rw [Finset.mul_sum]
refine Fintype.sum_congr _ _ fun i ↦ ?_
repeat erw [map_smul]
simp [HSMul.hSMul, SMul.smul]
simp only [HSMul.hSMul, SMul.smul, toSpecies_apply, Fin.isValue, neg_mul, one_mul]
ring)
(by
intro S T R
@ -298,7 +305,7 @@ def cubeTriLin : TriLinearSymm (SMνCharges n).Charges := TriLinearSymm.mk₃
rw [Finset.mul_sum]
refine Fintype.sum_congr _ _ fun i ↦ ?_
repeat erw [map_smul]
simp [HSMul.hSMul, SMul.smul]
simp only [HSMul.hSMul, SMul.smul, toSpecies_apply, Fin.isValue]
ring)
(by
intro S T R L

3
HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
View file

@ -69,7 +69,8 @@ def speciesEmbed (m n : ℕ) :
rfl
map_smul' a S := by
funext i
simp [HSMul.hSMul]
simp only [SMνSpecies_numberCharges, HSMul.hSMul, ACCSystemCharges.chargesModule_smul,
eq_ratCast, Rat.cast_eq_id, id_eq]
by_cases hi : i.val < m
· erw [dif_pos hi, dif_pos hi]
· erw [dif_neg hi, dif_neg hi]

6
HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean
View file

@ -38,12 +38,12 @@ variable {n : ℕ}
lemma SU2Sol (S : (SMNoGrav n).LinSols) : accSU2 S.val = 0 := by
have hS := S.linearSol
simp at hS
simp only [SMNoGrav_numberLinear, SMNoGrav_linearACCs, Fin.isValue] at hS
exact hS 0
lemma SU3Sol (S : (SMNoGrav n).LinSols) : accSU3 S.val = 0 := by
have hS := S.linearSol
simp at hS
simp only [SMNoGrav_numberLinear, SMNoGrav_linearACCs, Fin.isValue] at hS
exact hS 1
lemma cubeSol (S : (SMNoGrav n).Sols) : accCube S.val = 0 := S.cubicSol
@ -54,7 +54,7 @@ def chargeToLinear (S : (SMNoGrav n).Charges) (hSU2 : accSU2 S = 0) (hSU3 : accS
(SMNoGrav n).LinSols :=
⟨S, by
intro i
simp at i
simp only [SMNoGrav_numberLinear] at i
match i with
| 0 => exact hSU2
| 1 => exact hSU3⟩

27
HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean
View file

@ -130,7 +130,11 @@ def B₆ : (SM 3).Charges := toSpeciesEquiv.invFun (fun s => fun i =>
lemma B₆_cubic (S T : (SM 3).Charges) : cubeTriLin B₆ S T =
3 * (S (5 : Fin 18) * T (5 : Fin 18) - S (8 : Fin 18) * T (8 : Fin 18)) := by
simp [Fin.sum_univ_three, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
simp only [B₆, Equiv.invFun_as_coe, cubeTriLin_toFun_apply_apply, Nat.reduceMul, finProdFinEquiv,
Fin.divNat, Fin.modNat, Fin.isValue, Equiv.coe_fn_mk, Fin.val_zero, mul_zero, add_zero,
toSpeciesEquiv_symm_apply, Fin.val_one, mul_one, Nat.ofNat_pos, Nat.add_div_right,
Nat.add_mod_right, Fin.val_two, Nat.add_mul_mod_self_left, Fin.sum_univ_three, Fin.zero_eta,
zero_mul, zero_add, Fin.reduceFinMk, Fin.mk_one, Nat.reduceAdd, one_mul, neg_mul, mul_neg]
ring_nf
/-- The charge assignments forming a basis of the plane. -/
@ -150,7 +154,8 @@ lemma B₀_Bi_cubic {i : Fin 7} (hi : 0 ≠ i) (S : (SM 3).Charges) :
change cubeTriLin B₀ (B i) S = 0
rw [B₀_cubic]
fin_cases i <;>
simp at hi <;>
simp only [Fin.isValue, Fin.zero_eta, ne_eq, Fin.reduceEq, not_false_eq_true, Fin.mk_one,
Fin.reduceFinMk, not_true_eq_false] at hi <;>
simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
lemma B₁_Bi_cubic {i : Fin 7} (hi : 1 ≠ i) (S : (SM 3).Charges) :
@ -158,7 +163,8 @@ lemma B₁_Bi_cubic {i : Fin 7} (hi : 1 ≠ i) (S : (SM 3).Charges) :
change cubeTriLin B₁ (B i) S = 0
rw [B₁_cubic]
fin_cases i <;>
simp at hi <;>
simp only [Fin.isValue, Fin.zero_eta, ne_eq, Fin.reduceEq, not_false_eq_true, Fin.mk_one,
Fin.reduceFinMk, not_true_eq_false] at hi <;>
simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
lemma B₂_Bi_cubic {i : Fin 7} (hi : 2 ≠ i) (S : (SM 3).Charges) :
@ -166,7 +172,8 @@ lemma B₂_Bi_cubic {i : Fin 7} (hi : 2 ≠ i) (S : (SM 3).Charges) :
change cubeTriLin B₂ (B i) S = 0
rw [B₂_cubic]
fin_cases i <;>
simp at hi <;>
simp only [Fin.isValue, Fin.zero_eta, ne_eq, Fin.reduceEq, not_false_eq_true, Fin.mk_one,
Fin.reduceFinMk, not_true_eq_false] at hi <;>
simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
lemma B₃_Bi_cubic {i : Fin 7} (hi : 3 ≠ i) (S : (SM 3).Charges) :
@ -174,7 +181,8 @@ lemma B₃_Bi_cubic {i : Fin 7} (hi : 3 ≠ i) (S : (SM 3).Charges) :
change cubeTriLin (B₃) (B i) S = 0
rw [B₃_cubic]
fin_cases i <;>
simp at hi <;>
simp only [Fin.isValue, Fin.zero_eta, ne_eq, Fin.reduceEq, not_false_eq_true, Fin.mk_one,
Fin.reduceFinMk, not_true_eq_false] at hi <;>
simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
lemma B₄_Bi_cubic {i : Fin 7} (hi : 4 ≠ i) (S : (SM 3).Charges) :
@ -182,7 +190,8 @@ lemma B₄_Bi_cubic {i : Fin 7} (hi : 4 ≠ i) (S : (SM 3).Charges) :
change cubeTriLin (B₄) (B i) S = 0
rw [B₄_cubic]
fin_cases i <;>
simp at hi <;>
simp only [Fin.isValue, Fin.zero_eta, ne_eq, Fin.reduceEq, not_false_eq_true, Fin.mk_one,
Fin.reduceFinMk, not_true_eq_false] at hi <;>
simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
lemma B₅_Bi_cubic {i : Fin 7} (hi : 5 ≠ i) (S : (SM 3).Charges) :
@ -190,7 +199,8 @@ lemma B₅_Bi_cubic {i : Fin 7} (hi : 5 ≠ i) (S : (SM 3).Charges) :
change cubeTriLin (B₅) (B i) S = 0
rw [B₅_cubic]
fin_cases i <;>
simp at hi <;>
simp only [Fin.isValue, Fin.zero_eta, ne_eq, Fin.reduceEq, not_false_eq_true, Fin.mk_one,
Fin.reduceFinMk, not_true_eq_false] at hi <;>
simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
lemma B₆_Bi_cubic {i : Fin 7} (hi : 6 ≠ i) (S : (SM 3).Charges) :
@ -198,7 +208,8 @@ lemma B₆_Bi_cubic {i : Fin 7} (hi : 6 ≠ i) (S : (SM 3).Charges) :
change cubeTriLin (B₆) (B i) S = 0
rw [B₆_cubic]
fin_cases i <;>
simp at hi <;>
simp only [Fin.isValue, Fin.zero_eta, ne_eq, Fin.reduceEq, not_false_eq_true, Fin.mk_one,
Fin.reduceFinMk, not_true_eq_false] at hi <;>
simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
lemma Bi_Bj_ne_cubic {i j : Fin 7} (h : i ≠ j) (S : (SM 3).Charges) :

4
HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
View file

@ -35,7 +35,7 @@ def BL₁ : (PlusU1 1).Sols where
| (5 : Fin 6) => 3
linearSol := by
intro i
simp at i
simp only [PlusU1_numberLinear] at i
match i with
| 0 => rfl
| 1 => rfl
@ -43,7 +43,7 @@ def BL₁ : (PlusU1 1).Sols where
| 3 => rfl
quadSol := by
intro i
simp at i
simp only [PlusU1_numberQuadratic] at i
match i with
| 0 => rfl
cubicSol := by rfl

18
HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean
View file

@ -40,27 +40,27 @@ variable {n : ℕ}
lemma gravSol (S : (PlusU1 n).LinSols) : accGrav S.val = 0 := by
have hS := S.linearSol
simp at hS
simp only [PlusU1_numberLinear, PlusU1_linearACCs, Fin.isValue] at hS
exact hS 0
lemma SU2Sol (S : (PlusU1 n).LinSols) : accSU2 S.val = 0 := by
have hS := S.linearSol
simp at hS
simp only [PlusU1_numberLinear, PlusU1_linearACCs, Fin.isValue] at hS
exact hS 1
lemma SU3Sol (S : (PlusU1 n).LinSols) : accSU3 S.val = 0 := by
have hS := S.linearSol
simp at hS
simp only [PlusU1_numberLinear, PlusU1_linearACCs, Fin.isValue] at hS
exact hS 2
lemma YYsol (S : (PlusU1 n).LinSols) : accYY S.val = 0 := by
have hS := S.linearSol
simp at hS
simp only [PlusU1_numberLinear, PlusU1_linearACCs, Fin.isValue] at hS
exact hS 3
lemma quadSol (S : (PlusU1 n).QuadSols) : accQuad S.val = 0 := by
have hS := S.quadSol
simp at hS
simp only [PlusU1_numberQuadratic, HomogeneousQuadratic.eq_1, PlusU1_quadraticACCs] at hS
exact hS 0
lemma cubeSol (S : (PlusU1 n).Sols) : accCube S.val = 0 := by
@ -73,7 +73,7 @@ def chargeToLinear (S : (PlusU1 n).Charges) (hGrav : accGrav S = 0)
(PlusU1 n).LinSols :=
⟨S, by
intro i
simp at i
simp only [PlusU1_numberLinear] at i
match i with
| 0 => exact hGrav
| 1 => exact hSU2
@ -86,7 +86,7 @@ def linearToQuad (S : (PlusU1 n).LinSols) (hQ : accQuad S.val = 0) :
(PlusU1 n).QuadSols :=
⟨S, by
intro i
simp at i
simp only [PlusU1_numberQuadratic] at i
match i with
| 0 => exact hQ⟩
@ -122,7 +122,7 @@ def perm (n : ℕ) : ACCSystemGroupAction (PlusU1 n) where
rep := repCharges
linearInvariant := by
intro i
simp at i
simp only [PlusU1_numberLinear] at i
match i with
| 0 => exact accGrav_invariant
| 1 => exact accSU2_invariant
@ -130,7 +130,7 @@ def perm (n : ℕ) : ACCSystemGroupAction (PlusU1 n) where
| 3 => exact accYY_invariant
quadInvariant := by
intro i
simp at i
simp only [PlusU1_numberQuadratic] at i
match i with
| 0 => exact accQuad_invariant
cubicInvariant := accCube_invariant

6
HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
View file

@ -162,7 +162,7 @@ lemma isSolution_sum_part (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑
rw [isSolution_f0 f hS, isSolution_f1 f hS, isSolution_f2 f hS, isSolution_f3 f hS,
isSolution_f4 f hS, isSolution_f5 f hS,
isSolution_f6 f hS, isSolution_f7 f hS, isSolution_f8 f hS]
simp
simp only [Fin.isValue, zero_smul, add_zero, zero_add]
rfl
lemma isSolution_grav (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) :
@ -172,7 +172,7 @@ lemma isSolution_grav (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f
have hg := gravSol S.toLinSols
rw [hS', hx, accGrav.map_add, accGrav.map_smul, accGrav.map_smul, show accGrav B₉ = 3 by rfl,
show accGrav B₁₀ = 1 by rfl] at hg
simp at hg
simp only [Fin.isValue, smul_eq_mul, mul_one] at hg
linear_combination hg
lemma isSolution_sum_part' (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) :
@ -193,7 +193,7 @@ lemma isSolution_f9 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i
cubeTriLin.map_smul₃, cubeTriLin.map_smul₃] at hc
rw [show accCube B₉ = 9 by rfl, show accCube B₁₀ = 1 by rfl, show cubeTriLin B₉ B₉ B₁₀ = 0 by rfl,
show cubeTriLin B₁₀ B₁₀ B₉ = 0 by rfl] at hc
simp at hc
simp only [Fin.isValue, neg_mul, mul_one, mul_zero, add_zero] at hc
have h1 : f 9 ^ 3 * 9 + (-(3 * f 9)) ^ 3 = - 18 * f 9 ^ 3 := by ring
rw [h1] at hc
simpa using hc

4
HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean
View file

@ -55,7 +55,9 @@ lemma accQuad_α₁_α₂ (S : (PlusU1 n).LinSols) :
lemma accQuad_α₁_α₂_zero (S : (PlusU1 n).LinSols) (h1 : α₁ C S = 0)
(h2 : α₂ S = 0) (a b : ℚ) : accQuad (a • S + b • C.1).val = 0 := by
erw [add_AFL_quad]
simp [α₁, α₂] at h1 h2
simp only [α₁, quadBiLin_toFun_apply, Fin.isValue, neg_mul, neg_eq_zero, mul_eq_zero,
OfNat.ofNat_ne_zero, false_or, α₂, HomogeneousQuadratic.eq_1, accQuad,
BiLinearSymm.toHomogeneousQuad_apply] at h1 h2
field_simp [h1, h2]
/-- The construction of a `QuadSol` from a `LinSols` in the generic case. -/

4
HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean
View file

@ -118,14 +118,14 @@ lemma quadSolToSolInv_α₁_α₂_neq_zero (S : (PlusU1 n).Sols) (h : α₁ S.1
lemma quadSolToSolInv_special (S : (PlusU1 n).Sols) (h : α₁ S.1 = 0) :
special (quadSolToSolInv S).1 (quadSolToSolInv S).2.1 (quadSolToSolInv S).2.2
(quadSolToSolInv_α₁_α₂_zero S h).1 (quadSolToSolInv_α₁_α₂_zero S h).2 = S := by
simp [quadSolToSolInv_1]
simp only [quadSolToSolInv_1]
rw [show (quadSolToSolInv S).2.1 = 1 by rw [quadSolToSolInv, if_pos h]]
rw [show (quadSolToSolInv S).2.2 = 0 by rw [quadSolToSolInv, if_pos h]]
rw [special_on_AF]
lemma quadSolToSolInv_generic (S : (PlusU1 n).Sols) (h : α₁ S.1 ≠ 0) :
(quadSolToSolInv S).2.1 • generic (quadSolToSolInv S).1 = S := by
simp [quadSolToSolInv_1]
simp only [quadSolToSolInv_1]
rw [show (quadSolToSolInv S).2.1 = (α₁ S.1)⁻¹ by rw [quadSolToSolInv, if_neg h]]
rw [generic_on_AF_α₁_ne_zero S h]

17
HepLean/FlavorPhysics/CKMMatrix/Basic.lean
View file

@ -45,7 +45,11 @@ 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]
simp only [phaseShiftMatrix, Fin.zero_eta, Fin.isValue, conjTranspose_apply, cons_val',
cons_val_zero, empty_val', cons_val_fin_one, vecCons_const, star_def, ← exp_conj,
_root_.map_mul, conj_I, conj_ofReal, neg_mul, ofReal_neg, mul_neg, Fin.mk_one, cons_val_one,
head_fin_const, star_zero, head_cons, cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd,
tail_val', head_val', tail_cons, Fin.reduceFinMk, map_eq_zero]
· rfl
· rfl
@ -53,7 +57,10 @@ 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]
simp only [phaseShiftMatrix, Fin.zero_eta, Fin.isValue, mul_apply, cons_val', empty_val',
cons_val_fin_one, cons_val_zero, vecCons_const, Fin.sum_univ_three, cons_val_one, head_cons,
head_fin_const, mul_zero, add_zero, cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons,
tail_val', head_val', zero_mul, ofReal_add, Fin.mk_one, Fin.reduceFinMk, zero_add]
any_goals rw [mul_add, exp_add]
change cexp (I * ↑c) * 0 = 0
simp
@ -286,7 +293,11 @@ lemma VAbs'_equiv (i j : Fin 3) (V U : CKMMatrix) (h : V ≈ U) :
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]
simp only [Fin.zero_eta, Fin.isValue, cons_val_zero, zero_mul, add_zero, mul_zero,
_root_.map_mul, abs_exp, mul_re, I_re, ofReal_re, I_im, ofReal_im, sub_self, Real.exp_zero,
one_mul, mul_one, Fin.mk_one, cons_val_one, head_cons, zero_add, head_fin_const,
Fin.reduceFinMk, cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons,
tail_val', head_val']
all_goals change Complex.abs (0 * _ + _) = _
all_goals simp [Complex.abs_exp]

8
HepLean/FlavorPhysics/CKMMatrix/Relations.lean
View file

@ -273,7 +273,8 @@ lemma VAbs_sum_sq_col_eq_one (V : Quotient CKMMatrixSetoid) (i : Fin 3) :
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
simp only [mul_apply, star_apply, RCLike.star_def, Fin.sum_univ_three, Fin.isValue,
one_apply_eq] 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]
@ -309,9 +310,10 @@ lemma cs_of_ud_us_zero {V : CKMMatrix} (ha : ¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0)) :
have h1 := snd_row_normalized_abs V
symm
rw [Real.sqrt_eq_iff_eq_sq]
· simp [not_or] at ha
· simp only [Fin.isValue, ne_eq, not_or, Decidable.not_not] at ha
rw [cb_eq_zero_of_ud_us_zero ha] at h1
simp at h1
simp only [Fin.isValue, map_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow,
add_zero] at h1
simp only [VcdAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk, VcsAbs]
rw [← h1]
ring

7
HepLean/FlavorPhysics/CKMMatrix/Rows.lean
View file

@ -47,7 +47,8 @@ lemma uRow_normalized (V : CKMMatrix) : conj [V]u ⬝ᵥ [V]u = 1 := by
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
simp only [Fin.isValue, mul_apply, star_apply, RCLike.star_def, Fin.sum_univ_three,
one_apply_eq] 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
@ -215,7 +216,7 @@ lemma cRow_cross_tRow_eq_uRow (V : CKMMatrix) :
fin_cases i <;> simp
simp only [h3, Fin.isValue, smul_dotProduct, Pi.conj_apply, smul_eq_mul,
uRow_normalized, Fin.isValue, mul_one, mul_conj, ← Complex.sq_abs] at h2
simp at h2
simp only [Fin.isValue, ofReal_pow, sq_eq_one_iff, ofReal_eq_one] at h2
cases' h2 with h2 h2
· have hx : [V]u = (g 0)⁻¹ • (conj ([V]c) ×₃ conj ([V]t)) := by
rw [← hg, smul_smul, inv_mul_cancel₀, one_smul]
@ -242,7 +243,7 @@ lemma uRow_cross_cRow_eq_tRow (V : CKMMatrix) :
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
simp only [Fin.isValue, coe_basisOfLinearIndependentOfCardEqFinrank, rows] 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,

17
HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
View file

@ -49,7 +49,10 @@ lemma standParamAsMatrix_unitary (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) :
head_fin_const]
simp only [ofReal_cos, ofReal_sin]
rw [exp_neg]
fin_cases i <;> simp
fin_cases i <;>
simp only [Fin.zero_eta, Fin.isValue, cons_val_zero, one_apply_eq, Fin.mk_one, cons_val_one,
head_cons, ne_eq, zero_ne_one, not_false_eq_true, one_apply_ne, Fin.reduceFinMk,
cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons, Fin.reduceEq]
· ring_nf
field_simp
rw [sin_sq, sin_sq, sin_sq]
@ -67,7 +70,10 @@ lemma standParamAsMatrix_unitary (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) :
← exp_conj, _root_.map_mul, conj_I, neg_mul, cons_val_two, tail_cons, head_fin_const, star_neg]
simp only [ofReal_sin, ofReal_cos]
rw [exp_neg]
fin_cases i <;> simp
fin_cases i <;>
simp only [Fin.zero_eta, Fin.isValue, cons_val_zero, Fin.mk_one, ne_eq, one_ne_zero,
not_false_eq_true, one_apply_ne, cons_val_one, head_cons, one_apply_eq, Fin.reduceFinMk,
cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons, Fin.reduceEq]
· ring_nf
field_simp
rw [sin_sq, sin_sq]
@ -86,7 +92,10 @@ lemma standParamAsMatrix_unitary (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) :
head_fin_const]
simp only [ofReal_sin, ofReal_cos]
rw [exp_neg]
fin_cases i <;> simp
fin_cases i <;>
simp only [Fin.zero_eta, Fin.isValue, cons_val_zero, Fin.reduceFinMk, ne_eq, Fin.reduceEq,
not_false_eq_true, one_apply_ne, Fin.mk_one, cons_val_one, head_cons, cons_val_two,
Nat.succ_eq_add_one, Nat.reduceAdd, tail_cons, one_apply_eq]
· ring_nf
rw [sin_sq]
ring
@ -148,7 +157,7 @@ lemma eq_rows (U : CKMMatrix) {θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ} (hu :
lemma eq_exp_of_phases (θ₁₂ θ₁₃ θ₂₃ δ₁₃ δ₁₃' : ℝ) (h : cexp (δ₁₃ * I) = cexp (δ₁₃' * I)) :
standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ = standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃' := by
simp [standParam, standParamAsMatrix]
simp only [standParam, standParamAsMatrix, ofReal_cos, ofReal_sin, neg_mul]
apply CKMMatrix_ext
simp only
rw [show exp (I * δ₁₃) = exp (I * δ₁₃') by rw [mul_comm, h, mul_comm]]

48
HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
View file

@ -397,10 +397,16 @@ lemma on_param_cos_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.c
have hS12 := congrArg ofReal (S₁₂_of_Vub_one (VubAbs_of_cos_θ₁₃_zero h))
simp only [ofReal_eq_coe, ← S₁₂_eq_ℂsin_θ₁₂, map_zero] at hS12
use 0, 0, 0, δ₁₃, 0, -δ₁₃
simp [standParam, standParamAsMatrix, h, phaseShift, hS13, hC12, hS12]
simp only [standParam, standParamAsMatrix, ofReal_cos, hC12, h, ofReal_zero, mul_zero, ofReal_sin,
hS12, hS13, neg_mul, one_mul, neg_zero, zero_mul, mul_one, zero_sub, sub_zero, phaseShift,
phaseShiftMatrix, exp_zero, Submonoid.mk_mul_mk, ofReal_neg, mul_neg, Subtype.mk.injEq]
funext i j
fin_cases i <;> fin_cases j <;>
simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three]
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue, cons_val',
cons_val_zero, empty_val', cons_val_fin_one, mul_apply, Fin.sum_univ_three, one_mul,
cons_val_one, head_cons, zero_mul, add_zero, cons_val_two, tail_cons, head_fin_const,
vecCons_const, mul_zero, tail_val', head_val', zero_add, Fin.mk_one, Fin.reduceFinMk,
neg_mul, mul_one]
· rfl
· rfl
@ -413,7 +419,11 @@ lemma on_param_cos_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.c
exp_zero, mul_one, Submonoid.mk_mul_mk, ofReal_neg, mul_neg, Subtype.mk.injEq]
funext i j
fin_cases i <;> fin_cases j <;>
simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three]
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue, cons_val',
cons_val_zero, empty_val', cons_val_fin_one, mul_apply, Fin.sum_univ_three, one_mul,
cons_val_one, head_cons, zero_mul, add_zero, cons_val_two, tail_cons, head_fin_const,
vecCons_const, mul_zero, tail_val', head_val', zero_add, zero_eq_mul, mul_neg, neg_mul,
mul_one, neg_inj, Fin.mk_one, Fin.reduceFinMk]
· exact Or.inr rfl
· change _ = _ + _ * 0
field_simp
@ -429,10 +439,16 @@ lemma on_param_cos_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.c
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]
simp only [standParam, standParamAsMatrix, ofReal_cos, ofReal_sin, neg_mul, exp_neg, h,
ofReal_zero, mul_zero, zero_sub, zero_mul, sub_zero, phaseShift, phaseShiftMatrix, exp_zero,
mul_one, Submonoid.mk_mul_mk, ofReal_neg, mul_neg, Subtype.mk.injEq]
funext i j
fin_cases i <;> fin_cases j <;>
simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three]
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue, cons_val',
cons_val_zero, empty_val', cons_val_fin_one, mul_apply, Fin.sum_univ_three, one_mul,
cons_val_one, head_cons, zero_mul, add_zero, cons_val_two, tail_cons, head_fin_const,
vecCons_const, mul_one, mul_zero, tail_val', head_val', self_eq_add_right, mul_eq_zero,
zero_add, mul_neg, neg_inj, Fin.mk_one, Fin.reduceFinMk]
· exact Or.inr rfl
· ring_nf
change _ = _ + _ * 0
@ -448,7 +464,11 @@ lemma on_param_sin_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.s
Submonoid.mk_mul_mk, Subtype.mk.injEq]
funext i j
fin_cases i <;> fin_cases j <;>
simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three]
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue, cons_val',
cons_val_zero, empty_val', cons_val_fin_one, mul_apply, Fin.sum_univ_three, one_mul,
cons_val_one, head_cons, zero_mul, add_zero, cons_val_two, tail_cons, head_fin_const,
vecCons_const, mul_one, mul_zero, tail_val', head_val', zero_add, self_eq_add_right,
mul_eq_zero, Fin.mk_one, Fin.reduceFinMk]
· exact Or.inr rfl
· exact Or.inr rfl
@ -456,10 +476,16 @@ lemma on_param_sin_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.s
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]
simp only [standParam, standParamAsMatrix, ofReal_cos, h, ofReal_zero, zero_mul, ofReal_sin,
neg_mul, exp_neg, neg_zero, zero_sub, sub_zero, phaseShift, phaseShiftMatrix, mul_zero,
exp_zero, mul_one, Submonoid.mk_mul_mk, ofReal_neg, mul_neg, Subtype.mk.injEq]
funext i j
fin_cases i <;> fin_cases j <;>
simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three]
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue, cons_val',
cons_val_zero, empty_val', cons_val_fin_one, mul_apply, Fin.sum_univ_three, one_mul,
cons_val_one, head_cons, zero_mul, add_zero, cons_val_two, tail_cons, head_fin_const,
vecCons_const, mul_one, mul_zero, tail_val', head_val', self_eq_add_right, mul_eq_zero,
Fin.mk_one, zero_add, Fin.reduceFinMk, mul_neg, neg_mul, neg_inj]
· apply Or.inr rfl
· change _ = _ + _ * 0
simp only [mul_zero, add_zero, neg_inj]
@ -484,7 +510,11 @@ lemma on_param_sin_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.s
mul_one, Submonoid.mk_mul_mk, ofReal_neg, mul_neg, Subtype.mk.injEq]
funext i j
fin_cases i <;> fin_cases j <;>
simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three]
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue, cons_val',
cons_val_zero, empty_val', cons_val_fin_one, mul_apply, Fin.sum_univ_three, one_mul,
cons_val_one, head_cons, zero_mul, add_zero, cons_val_two, tail_cons, head_fin_const,
vecCons_const, mul_one, mul_zero, tail_val', head_val', self_eq_add_right, mul_eq_zero,
Fin.mk_one, zero_add, Fin.reduceFinMk, mul_neg, neg_inj]
· exact Or.inr rfl
· change _ = _ + _ * 0
simp only [mul_zero, add_zero, neg_inj]

5
HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean
View file

@ -31,7 +31,10 @@ lemma toMatrix_isSelfAdjoint (x : LorentzVector 3) : IsSelfAdjoint (toMatrix x)
rw [isSelfAdjoint_iff, star_eq_conjTranspose, ← Matrix.ext_iff]
intro i j
fin_cases i <;> fin_cases j <;>
simp [toMatrix, conj_ofReal]
simp only [toMatrix, LorentzVector.time, Fin.isValue, LorentzVector.space, Function.comp_apply,
Fin.zero_eta, conjTranspose_apply, of_apply, cons_val', cons_val_zero, empty_val',
cons_val_fin_one, star_add, RCLike.star_def, conj_ofReal, Fin.mk_one, cons_val_one,
head_fin_const, star_mul', conj_I, mul_neg, head_cons, star_sub, sub_neg_eq_add]
rfl
/-- A self-adjoint matrix formed from a Lorentz vector point. -/