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

doc: More doc strings.

Browse source
This commit is contained in:
jstoobysmith 2024-11-12 06:33:58 +00:00
parent c24029c9ca
commit c6fdcbbe7d
3 changed files with 14 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -70,14 +70,17 @@ def δ₁₃ (V : Quotient CKMMatrixSetoid) : ℝ :=
section sines
/-- For a CKM matrix `sin θ₁₂` is non-negative. -/
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)))
/-- For a CKM matrix `sin θ₁₃` is non-negative. -/
lemma S₁₃_nonneg (V : Quotient CKMMatrixSetoid) : 0 ≤ S₁₃ V :=
VAbs_ge_zero 0 2 V
/-- For a CKM matrix `sin θ₂₃` is non-negative. -/
lemma S₂₃_nonneg (V : Quotient CKMMatrixSetoid) : 0 ≤ S₂₃ V := by
by_cases ha : VubAbs V = 1
· rw [S₂₃, if_pos ha]
@ -86,6 +89,7 @@ lemma S₂₃_nonneg (V : Quotient CKMMatrixSetoid) : 0 ≤ S₂₃ V := by
apply Or.inl
apply And.intro (VAbs_ge_zero 1 2 V) (Real.sqrt_nonneg (VudAbs V ^ 2 + VusAbs V ^ 2))
/-- For a CKM matrix `sin θ₁₂` is less then or equal to 1. -/
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
@ -101,9 +105,11 @@ lemma S₁₂_leq_one (V : Quotient CKMMatrixSetoid) : S₁₂ V ≤ 1 := by
simp only [Fin.isValue, le_add_iff_nonneg_left]
exact sq_nonneg (VAbs 0 0 V)
/-- For a CKM matrix `sin θ₁₃` is less then or equal to 1. -/
lemma S₁₃_leq_one (V : Quotient CKMMatrixSetoid) : S₁₃ V ≤ 1 :=
VAbs_leq_one 0 2 V
/-- For a CKM matrix `sin θ₂₃` is less then or equal to 1. -/
lemma S₂₃_leq_one (V : Quotient CKMMatrixSetoid) : S₂₃ V ≤ 1 := by
by_cases ha : VubAbs V = 1
· rw [S₂₃, if_pos ha]

1
HepLean/Lorentz/Weyl/Unit.lean
View file

@ -108,6 +108,7 @@ def altLeftLeftUnit : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ altLeftHanded ⊗ leftHanded
simp only [mul_one, ← transpose_mul, SpecialLinearGroup.det_coe, isUnit_iff_ne_zero, ne_eq,
one_ne_zero, not_false_eq_true, mul_nonsing_inv, transpose_one]
/-- Applying the morphism `altLeftLeftUnit` to `1` returns `altLeftLeftUnitVal`. -/
lemma altLeftLeftUnit_apply_one : altLeftLeftUnit.hom (1 : ℂ) = altLeftLeftUnitVal := by
change altLeftLeftUnit.hom.toFun (1 : ℂ) = altLeftLeftUnitVal
simp only [Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,

7
HepLean/SpaceTime/Basic.lean
View file

@ -15,6 +15,8 @@ This file introduce 4d Minkowski spacetime.
noncomputable section
/-! TODO: SpaceTime should be refactored into a structure, to prevent casting. -/
/-- The space-time -/
def SpaceTime : Type := Fin 4 → ℝ
@ -59,18 +61,22 @@ lemma stdBasis_not_eq {μ ν : Fin 4} (h : μ ≠ ν) : stdBasis μ ν = 0 := by
rw [stdBasis_apply]
exact if_neg h
/-- For space-time,`stdBasis 0` is equal to `![1, 0, 0, 0] `. -/
lemma stdBasis_0 : stdBasis 0 = ![1, 0, 0, 0] := by
funext i
fin_cases i <;> simp [stdBasis_apply]
/-- For space-time,`stdBasis 1` is equal to `![0, 1, 0, 0] `. -/
lemma stdBasis_1 : stdBasis 1 = ![0, 1, 0, 0] := by
funext i
fin_cases i <;> simp [stdBasis_apply]
/-- For space-time,`stdBasis 2` is equal to `![0, 0, 1, 0] `. -/
lemma stdBasis_2 : stdBasis 2 = ![0, 0, 1, 0] := by
funext i
fin_cases i <;> simp [stdBasis_apply]
/-- For space-time,`stdBasis 3` is equal to `![0, 0, 0, 1] `. -/
lemma stdBasis_3 : stdBasis 3 = ![0, 0, 0, 1] := by
funext i
fin_cases i <;> simp [stdBasis_apply]
@ -83,6 +89,7 @@ lemma stdBasis_mulVec (μ ν : Fin 4) (Λ : Matrix (Fin 4) (Fin 4) ℝ) :
rw [stdBasis_apply, if_neg (Ne.symm h)]
exact CommMonoidWithZero.mul_zero (Λ ν x)
/-- The explicit expansion of a point in spacetime as `![x 0, x 1, x 2, x 3]`. -/
lemma explicit (x : SpaceTime) : x = ![x 0, x 1, x 2, x 3] := by
funext i
fin_cases i <;> rfl