refactor: pass at removing double spaces
This commit is contained in:
jstoobysmith
parent
1fe51b2e04
commit
1133b883f3
19 changed files with 121 additions and 121 deletions
|
|
@ -40,19 +40,19 @@ def S₂₃ (V : Quotient CKMMatrixSetoid) : ℝ :=
|
|||
else VcbAbs V / √ (VudAbs V ^ 2 + VusAbs V ^ 2)
|
||||
|
||||
/-- Given a CKM matrix `V` the real number corresponding to `θ₁₂` in the
|
||||
standard parameterization. --/
|
||||
standard parameterization. --/
|
||||
def θ₁₂ (V : Quotient CKMMatrixSetoid) : ℝ := Real.arcsin (S₁₂ V)
|
||||
|
||||
/-- Given a CKM matrix `V` the real number corresponding to `θ₁₃` in the
|
||||
standard parameterization. --/
|
||||
standard parameterization. --/
|
||||
def θ₁₃ (V : Quotient CKMMatrixSetoid) : ℝ := Real.arcsin (S₁₃ V)
|
||||
|
||||
/-- Given a CKM matrix `V` the real number corresponding to `θ₂₃` in the
|
||||
standard parameterization. --/
|
||||
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. --/
|
||||
standard parameterization. --/
|
||||
def C₁₂ (V : Quotient CKMMatrixSetoid) : ℝ := Real.cos (θ₁₂ V)
|
||||
|
||||
/-- Given a CKM matrix `V` the real number corresponding to `cos θ₁₃` in the
|
||||
|
|
@ -60,7 +60,7 @@ 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. --/
|
||||
standard parameterization. --/
|
||||
def C₂₃ (V : Quotient CKMMatrixSetoid) : ℝ := Real.cos (θ₂₃ V)
|
||||
|
||||
/-- Given a CKM matrix `V` the real number corresponding to the phase `δ₁₃` in the
|
||||
|
|
@ -126,7 +126,7 @@ lemma S₂₃_leq_one (V : Quotient CKMMatrixSetoid) : S₂₃ V ≤ 1 := by
|
|||
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 :=
|
||||
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 :=
|
||||
|
|
@ -168,7 +168,7 @@ lemma S₂₃_of_Vub_eq_one {V : Quotient CKMMatrixSetoid} (ha : VubAbs V = 1) :
|
|||
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
|
||||
S₂₃ V = VcbAbs V / √ (VudAbs V ^ 2 + VusAbs V ^ 2) := by
|
||||
rw [S₂₃, if_neg ha]
|
||||
|
||||
end sines
|
||||
|
|
@ -336,9 +336,9 @@ namespace standParam
|
|||
open Invariant
|
||||
|
||||
lemma mulExpδ₁₃_on_param_δ₁₃ (V : CKMMatrix) (δ₁₃ : ℝ) :
|
||||
mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ =
|
||||
mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ =
|
||||
sin (θ₁₂ ⟦V⟧) * cos (θ₁₃ ⟦V⟧) ^ 2 * sin (θ₂₃ ⟦V⟧) * sin (θ₁₃ ⟦V⟧)
|
||||
* cos (θ₁₂ ⟦V⟧) * cos (θ₂₃ ⟦V⟧) * cexp (I * δ₁₃) := by
|
||||
* cos (θ₁₂ ⟦V⟧) * cos (θ₂₃ ⟦V⟧) * cexp (I * δ₁₃) := by
|
||||
refine mulExpδ₁₃_eq _ _ _ _ ?_ ?_ ?_ ?_
|
||||
rw [S₁₂_eq_sin_θ₁₂]
|
||||
exact S₁₂_nonneg _
|
||||
|
|
@ -364,7 +364,7 @@ lemma mulExpδ₁₃_on_param_eq_zero_iff (V : CKMMatrix) (δ₁₃ : ℝ) :
|
|||
aesop
|
||||
|
||||
lemma mulExpδ₁₃_on_param_abs (V : CKMMatrix) (δ₁₃ : ℝ) :
|
||||
Complex.abs (mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧) =
|
||||
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_δ₁₃]
|
||||
|
|
@ -373,19 +373,19 @@ lemma mulExpδ₁₃_on_param_abs (V : CKMMatrix) (δ₁₃ : ℝ) :
|
|||
complexAbs_sin_θ₂₃, complexAbs_cos_θ₂₃]
|
||||
|
||||
lemma mulExpδ₁₃_on_param_neq_zero_arg (V : CKMMatrix) (δ₁₃ : ℝ)
|
||||
(h1 : mulExpδ₁₃ ⟦standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃⟧ ≠ 0 ) :
|
||||
(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
|
||||
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
|
||||
(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]
|
||||
|
|
@ -514,7 +514,7 @@ lemma eq_standParam_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0
|
|||
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',
|
||||
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₁₃]
|
||||
|
|
@ -613,7 +613,7 @@ theorem exists_δ₁₃ (V : CKMMatrix) :
|
|||
rw [hUV] at hna
|
||||
simp [VAbs] at hna
|
||||
simp_all
|
||||
have hU' := eq_standParam_of_fstRowThdColRealCond haU hU.2
|
||||
have hU' := eq_standParam_of_fstRowThdColRealCond haU hU.2
|
||||
rw [hU'] at hU
|
||||
use (- arg ([U]ub))
|
||||
rw [← hUV]
|
||||
|
|
@ -639,7 +639,7 @@ theorem eq_standardParameterization_δ₃ (V : CKMMatrix) :
|
|||
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⟧) δ₁₃'
|
||||
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δ₃
|
||||
|
|
|
|||
|
|
@ -77,7 +77,7 @@ def mk₂ (f : V × V → ℚ) (map_smul : ∀ a S T, f (a • S, T) = a * f (S,
|
|||
exact congrArg (HMul.hMul a) (swap T S)
|
||||
}
|
||||
map_smul' := fun a S => LinearMap.ext fun T => map_smul a S T
|
||||
map_add' := fun S1 S2 => LinearMap.ext fun T => map_add S1 S2 T
|
||||
map_add' := fun S1 S2 => LinearMap.ext fun T => map_add S1 S2 T
|
||||
swap' := swap
|
||||
|
||||
lemma map_smul₁ (f : BiLinearSymm V) (a : ℚ) (S T : V) : f (a • S) T = a * f S T := by
|
||||
|
|
@ -99,7 +99,7 @@ lemma map_add₂ (f : BiLinearSymm V) (S : V) (T1 T2 : V) :
|
|||
rw [f.swap, f.map_add₁, f.swap T1 S, f.swap T2 S]
|
||||
|
||||
/-- Fixing the second input vectors, the resulting linear map. -/
|
||||
def toLinear₁ (f : BiLinearSymm V) (T : V) : V →ₗ[ℚ] ℚ where
|
||||
def toLinear₁ (f : BiLinearSymm V) (T : V) : V →ₗ[ℚ] ℚ where
|
||||
toFun S := f S T
|
||||
map_add' S1 S2 := map_add₁ f S1 S2 T
|
||||
map_smul' a S := by
|
||||
|
|
@ -166,7 +166,7 @@ end HomogeneousCubic
|
|||
/-- The structure of a symmetric trilinear function. -/
|
||||
structure TriLinearSymm (V : Type) [AddCommMonoid V] [Module ℚ V] extends
|
||||
V →ₗ[ℚ] V →ₗ[ℚ] V →ₗ[ℚ] ℚ where
|
||||
swap₁' : ∀ S T L, toFun S T L = toFun T S L
|
||||
swap₁' : ∀ S T L, toFun S T L = toFun T S L
|
||||
swap₂' : ∀ S T L, toFun S T L = toFun S L T
|
||||
|
||||
namespace TriLinearSymm
|
||||
|
|
|
|||
|
|
@ -59,7 +59,7 @@ def toGL : SO(3) →* GL (Fin 3) ℝ where
|
|||
map_one' := by
|
||||
simp
|
||||
rfl
|
||||
map_mul' x y := by
|
||||
map_mul' x y := by
|
||||
simp only [_root_.mul_inv_rev, coe_inv]
|
||||
ext
|
||||
rfl
|
||||
|
|
@ -143,16 +143,16 @@ instance : TopologicalGroup SO(3) :=
|
|||
Inducing.topologicalGroup toGL toGL_embedding.toInducing
|
||||
|
||||
lemma det_minus_id (A : SO(3)) : det (A.1 - 1) = 0 := by
|
||||
have h1 : det (A.1 - 1) = - det (A.1 - 1) :=
|
||||
have h1 : det (A.1 - 1) = - det (A.1 - 1) :=
|
||||
calc
|
||||
det (A.1 - 1) = det (A.1 - A.1 * A.1ᵀ) := by simp [A.2.2]
|
||||
_ = det A.1 * det (1 - A.1ᵀ) := by rw [← det_mul, mul_sub, mul_one]
|
||||
_ = det A.1 * det (1 - A.1ᵀ) := by rw [← det_mul, mul_sub, mul_one]
|
||||
_ = det (1 - A.1ᵀ):= by simp [A.2.1]
|
||||
_ = det (1 - A.1ᵀ)ᵀ := by rw [det_transpose]
|
||||
_ = det (1 - A.1) := by simp
|
||||
_ = det (- (A.1 - 1)) := by simp
|
||||
_ = (- 1) ^ 3 * det (A.1 - 1) := by simp only [det_neg, Fintype.card_fin, neg_mul, one_mul]
|
||||
_ = - det (A.1 - 1) := by simp [pow_three]
|
||||
_ = (- 1) ^ 3 * det (A.1 - 1) := by simp only [det_neg, Fintype.card_fin, neg_mul, one_mul]
|
||||
_ = - det (A.1 - 1) := by simp [pow_three]
|
||||
simpa using h1
|
||||
|
||||
@[simp]
|
||||
|
|
@ -161,7 +161,7 @@ lemma det_id_minus (A : SO(3)) : det (1 - A.1) = 0 := by
|
|||
calc
|
||||
det (1 - A.1) = det (- (A.1 - 1)) := by simp
|
||||
_ = (- 1) ^ 3 * det (A.1 - 1) := by simp only [det_neg, Fintype.card_fin, neg_mul, one_mul]
|
||||
_ = - det (A.1 - 1) := by simp [pow_three]
|
||||
_ = - det (A.1 - 1) := by simp [pow_three]
|
||||
rw [h1, det_minus_id]
|
||||
simp only [neg_zero]
|
||||
|
||||
|
|
@ -216,7 +216,7 @@ lemma exists_basis_preserved (A : SO(3)) :
|
|||
obtain ⟨v, hv⟩ := exists_stationary_vec A
|
||||
have h3 : FiniteDimensional.finrank ℝ (EuclideanSpace ℝ (Fin 3)) = Fintype.card (Fin 3) := by
|
||||
simp_all only [toEnd_apply, finrank_euclideanSpace, Fintype.card_fin]
|
||||
obtain ⟨b, hb⟩ := Orthonormal.exists_orthonormalBasis_extension_of_card_eq h3 hv.1
|
||||
obtain ⟨b, hb⟩ := Orthonormal.exists_orthonormalBasis_extension_of_card_eq h3 hv.1
|
||||
simp at hb
|
||||
use b
|
||||
rw [hb, hv.2]
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@ We define
|
|||
- Define `lorentzAlgebra` via `LieAlgebra.Orthogonal.so'` as a subalgebra of
|
||||
`Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ`.
|
||||
- In `mem_iff` prove that a matrix is in the Lorentz algebra if and only if it satisfies the
|
||||
condition `Aᵀ * η = - η * A`.
|
||||
condition `Aᵀ * η = - η * A`.
|
||||
|
||||
-/
|
||||
|
||||
|
|
@ -21,7 +21,7 @@ namespace SpaceTime
|
|||
open Matrix
|
||||
open TensorProduct
|
||||
|
||||
/-- The Lorentz algebra as a subalgebra of `Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ`. -/
|
||||
/-- The Lorentz algebra as a subalgebra of `Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ`. -/
|
||||
def lorentzAlgebra : LieSubalgebra ℝ (Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ) :=
|
||||
(LieAlgebra.Orthogonal.so' (Fin 1) (Fin 3) ℝ)
|
||||
|
||||
|
|
@ -34,7 +34,7 @@ lemma transpose_eta (A : lorentzAlgebra) : A.1ᵀ * η = - η * A.1 := by
|
|||
simpa [LieAlgebra.Orthogonal.so', IsSkewAdjoint, IsAdjointPair] using h1
|
||||
|
||||
lemma mem_of_transpose_eta_eq_eta_mul_self {A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ}
|
||||
(h : Aᵀ * η = - η * A) : A ∈ lorentzAlgebra := by
|
||||
(h : Aᵀ * η = - η * A) : A ∈ lorentzAlgebra := by
|
||||
erw [mem_skewAdjointMatricesLieSubalgebra]
|
||||
simpa [LieAlgebra.Orthogonal.so', IsSkewAdjoint, IsAdjointPair] using h
|
||||
|
||||
|
|
@ -42,8 +42,8 @@ lemma mem_iff {A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ} :
|
|||
A ∈ lorentzAlgebra ↔ Aᵀ * η = - η * A :=
|
||||
Iff.intro (fun h => transpose_eta ⟨A, h⟩) (fun h => mem_of_transpose_eta_eq_eta_mul_self h)
|
||||
|
||||
lemma mem_iff' (A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ) :
|
||||
A ∈ lorentzAlgebra ↔ A = - η * Aᵀ * η := by
|
||||
lemma mem_iff' (A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ) :
|
||||
A ∈ lorentzAlgebra ↔ A = - η * Aᵀ * η := by
|
||||
rw [mem_iff]
|
||||
refine Iff.intro (fun h => ?_) (fun h => ?_)
|
||||
· trans -η * (Aᵀ * η)
|
||||
|
|
@ -91,7 +91,7 @@ instance lorentzVectorAsLieRingModule : LieRingModule lorentzAlgebra (LorentzVec
|
|||
|
||||
@[simps!]
|
||||
instance spaceTimeAsLieModule : LieModule ℝ lorentzAlgebra (LorentzVector 3) where
|
||||
smul_lie r Λ x := by
|
||||
smul_lie r Λ x := by
|
||||
simp [Bracket.bracket, smul_mulVec_assoc]
|
||||
lie_smul r Λ x := by
|
||||
simp [Bracket.bracket]
|
||||
|
|
|
|||
|
|
@ -44,7 +44,7 @@ scoped[LorentzGroup] notation (name := lorentzGroup_notation) "𝓛" => LorentzG
|
|||
|
||||
open minkowskiMetric
|
||||
|
||||
variable {Λ Λ' : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ}
|
||||
variable {Λ Λ' : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ}
|
||||
|
||||
/-!
|
||||
|
||||
|
|
@ -52,7 +52,7 @@ variable {Λ Λ' : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ}
|
|||
|
||||
-/
|
||||
|
||||
lemma mem_iff_norm : Λ ∈ LorentzGroup d ↔
|
||||
lemma mem_iff_norm : Λ ∈ LorentzGroup d ↔
|
||||
∀ (x : LorentzVector d), ⟪Λ *ᵥ x, Λ *ᵥ x⟫ₘ = ⟪x, x⟫ₘ := by
|
||||
refine Iff.intro (fun h x => h x x) (fun h x y => ?_)
|
||||
have hp := h (x + y)
|
||||
|
|
@ -78,7 +78,7 @@ lemma mem_iff_dual_mul_self : Λ ∈ LorentzGroup d ↔ dual Λ * Λ = 1 := by
|
|||
rw [mem_iff_on_right, matrix_eq_id_iff]
|
||||
exact forall_comm
|
||||
|
||||
lemma mem_iff_self_mul_dual : Λ ∈ LorentzGroup d ↔ Λ * dual Λ = 1 := by
|
||||
lemma mem_iff_self_mul_dual : Λ ∈ LorentzGroup d ↔ Λ * dual Λ = 1 := by
|
||||
rw [mem_iff_dual_mul_self]
|
||||
exact mul_eq_one_comm
|
||||
|
||||
|
|
@ -147,7 +147,7 @@ open minkowskiMetric
|
|||
|
||||
variable {Λ Λ' : LorentzGroup d}
|
||||
|
||||
lemma coe_inv : (Λ⁻¹).1 = Λ.1⁻¹:= by
|
||||
lemma coe_inv : (Λ⁻¹).1 = Λ.1⁻¹:= by
|
||||
refine (inv_eq_left_inv ?h).symm
|
||||
exact mem_iff_dual_mul_self.mp Λ.2
|
||||
|
||||
|
|
@ -190,7 +190,7 @@ def toProd : LorentzGroup d →* (Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ
|
|||
(Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)ᵐᵒᵖ :=
|
||||
MonoidHom.comp (Units.embedProduct _) toGL
|
||||
|
||||
lemma toProd_eq_transpose_η : toProd Λ = (Λ.1, MulOpposite.op $ minkowskiMetric.dual Λ.1) := rfl
|
||||
lemma toProd_eq_transpose_η : toProd Λ = (Λ.1, MulOpposite.op $ minkowskiMetric.dual Λ.1) := rfl
|
||||
|
||||
lemma toProd_injective : Function.Injective (@toProd d) := by
|
||||
intro A B h
|
||||
|
|
|
|||
|
|
@ -100,7 +100,7 @@ lemma toMatrix_mulVec (u v : FuturePointing d) (x : LorentzVector d) :
|
|||
open minkowskiMatrix LorentzVector in
|
||||
@[simp]
|
||||
lemma toMatrix_apply (u v : FuturePointing d) (μ ν : Fin 1 ⊕ Fin d) :
|
||||
(toMatrix u v) μ ν = η μ μ * (⟪e μ, e ν⟫ₘ + 2 * ⟪e ν, u⟫ₘ * ⟪e μ, v⟫ₘ
|
||||
(toMatrix u v) μ ν = η μ μ * (⟪e μ, e ν⟫ₘ + 2 * ⟪e ν, u⟫ₘ * ⟪e μ, v⟫ₘ
|
||||
- ⟪e μ, u + v⟫ₘ * ⟪e ν, u + v⟫ₘ / (1 + ⟪u, v.1.1⟫ₘ)) := by
|
||||
rw [matrix_apply_stdBasis (toMatrix u v) μ ν, toMatrix_mulVec]
|
||||
simp only [genBoost, genBoostAux₁, genBoostAux₂, map_add, smul_add, neg_smul, LinearMap.add_apply,
|
||||
|
|
|
|||
|
|
@ -39,7 +39,7 @@ lemma IsOrthochronous_iff_transpose :
|
|||
IsOrthochronous Λ ↔ IsOrthochronous (transpose Λ) := by rfl
|
||||
|
||||
lemma IsOrthochronous_iff_ge_one :
|
||||
IsOrthochronous Λ ↔ 1 ≤ timeComp Λ := by
|
||||
IsOrthochronous Λ ↔ 1 ≤ timeComp Λ := by
|
||||
rw [IsOrthochronous_iff_futurePointing, NormOneLorentzVector.FuturePointing.mem_iff,
|
||||
NormOneLorentzVector.time_pos_iff]
|
||||
simp only [time, toNormOneLorentzVector, timeVec, Fin.isValue]
|
||||
|
|
@ -68,7 +68,7 @@ def timeCompCont : C(LorentzGroup d, ℝ) := ⟨fun Λ => timeComp Λ ,
|
|||
/-- An auxillary function used in the definition of `orthchroMapReal`. -/
|
||||
def stepFunction : ℝ → ℝ := fun t =>
|
||||
if t ≤ -1 then -1 else
|
||||
if 1 ≤ t then 1 else t
|
||||
if 1 ≤ t then 1 else t
|
||||
|
||||
lemma stepFunction_continuous : Continuous stepFunction := by
|
||||
apply Continuous.if ?_ continuous_const (Continuous.if ?_ continuous_const continuous_id)
|
||||
|
|
@ -105,20 +105,20 @@ lemma orthchroMapReal_minus_one_or_one (Λ : LorentzGroup d) :
|
|||
apply Or.inr $ orthchroMapReal_on_IsOrthochronous h
|
||||
apply Or.inl $ orthchroMapReal_on_not_IsOrthochronous h
|
||||
|
||||
local notation "ℤ₂" => Multiplicative (ZMod 2)
|
||||
local notation "ℤ₂" => Multiplicative (ZMod 2)
|
||||
|
||||
/-- A continuous map from `lorentzGroup` to `ℤ₂` whose kernal are the Orthochronous elements. -/
|
||||
def orthchroMap : C(LorentzGroup d, ℤ₂) :=
|
||||
ContinuousMap.comp coeForℤ₂ {
|
||||
toFun := fun Λ => ⟨orthchroMapReal Λ, orthchroMapReal_minus_one_or_one Λ⟩,
|
||||
continuous_toFun := Continuous.subtype_mk (ContinuousMap.continuous orthchroMapReal) _}
|
||||
continuous_toFun := Continuous.subtype_mk (ContinuousMap.continuous orthchroMapReal) _}
|
||||
|
||||
lemma orthchroMap_IsOrthochronous {Λ : LorentzGroup d} (h : IsOrthochronous Λ) :
|
||||
orthchroMap Λ = 1 := by
|
||||
simp [orthchroMap, orthchroMapReal_on_IsOrthochronous h]
|
||||
|
||||
lemma orthchroMap_not_IsOrthochronous {Λ : LorentzGroup d} (h : ¬ IsOrthochronous Λ) :
|
||||
orthchroMap Λ = Additive.toMul (1 : ZMod 2) := by
|
||||
orthchroMap Λ = Additive.toMul (1 : ZMod 2) := by
|
||||
simp [orthchroMap, orthchroMapReal_on_not_IsOrthochronous h]
|
||||
rfl
|
||||
|
||||
|
|
@ -136,7 +136,7 @@ lemma mul_othchron_of_not_othchron_not_othchron {Λ Λ' : LorentzGroup d} (h :
|
|||
rw [IsOrthochronous, timeComp_mul]
|
||||
exact NormOneLorentzVector.FuturePointing.metric_reflect_not_mem_not_mem h h'
|
||||
|
||||
lemma mul_not_othchron_of_othchron_not_othchron {Λ Λ' : LorentzGroup d} (h : IsOrthochronous Λ)
|
||||
lemma mul_not_othchron_of_othchron_not_othchron {Λ Λ' : LorentzGroup d} (h : IsOrthochronous Λ)
|
||||
(h' : ¬ IsOrthochronous Λ') : ¬ IsOrthochronous (Λ * Λ') := by
|
||||
rw [not_orthochronous_iff_le_zero, timeComp_mul]
|
||||
rw [IsOrthochronous_iff_transpose] at h
|
||||
|
|
|
|||
|
|
@ -42,7 +42,7 @@ instance : TopologicalGroup ℤ₂ := TopologicalGroup.mk
|
|||
|
||||
/-- A continuous function from `({-1, 1} : Set ℝ)` to `ℤ₂`. -/
|
||||
@[simps!]
|
||||
def coeForℤ₂ : C(({-1, 1} : Set ℝ), ℤ₂) where
|
||||
def coeForℤ₂ : C(({-1, 1} : Set ℝ), ℤ₂) where
|
||||
toFun x := if x = ⟨1, Set.mem_insert_of_mem (-1) rfl⟩
|
||||
then (Additive.toMul 0) else (Additive.toMul (1 : ZMod 2))
|
||||
continuous_toFun := by
|
||||
|
|
@ -50,7 +50,7 @@ def coeForℤ₂ : C(({-1, 1} : Set ℝ), ℤ₂) where
|
|||
exact continuous_of_discreteTopology
|
||||
|
||||
/-- The continuous map taking a Lorentz matrix to its determinant. -/
|
||||
def detContinuous : C(𝓛 d, ℤ₂) :=
|
||||
def detContinuous : C(𝓛 d, ℤ₂) :=
|
||||
ContinuousMap.comp coeForℤ₂ {
|
||||
toFun := fun Λ => ⟨Λ.1.det, Or.symm (LorentzGroup.det_eq_one_or_neg_one _)⟩,
|
||||
continuous_toFun := by
|
||||
|
|
@ -64,7 +64,7 @@ lemma detContinuous_eq_iff_det_eq (Λ Λ' : LorentzGroup d) :
|
|||
apply Iff.intro
|
||||
intro h
|
||||
simp [detContinuous] at h
|
||||
cases' det_eq_one_or_neg_one Λ with h1 h1
|
||||
cases' det_eq_one_or_neg_one Λ with h1 h1
|
||||
<;> cases' det_eq_one_or_neg_one Λ' with h2 h2
|
||||
<;> simp_all [h1, h2, h]
|
||||
rw [← toMul_zero, @Equiv.apply_eq_iff_eq] at h
|
||||
|
|
@ -92,16 +92,16 @@ def detRep : 𝓛 d →* ℤ₂ where
|
|||
|
||||
lemma detRep_continuous : Continuous (@detRep d) := detContinuous.2
|
||||
|
||||
lemma det_on_connected_component {Λ Λ' : LorentzGroup d} (h : Λ' ∈ connectedComponent Λ) :
|
||||
lemma det_on_connected_component {Λ Λ' : LorentzGroup d} (h : Λ' ∈ connectedComponent Λ) :
|
||||
Λ.1.det = Λ'.1.det := by
|
||||
obtain ⟨s, hs, hΛ'⟩ := h
|
||||
let f : ContinuousMap s ℤ₂ := ContinuousMap.restrict s detContinuous
|
||||
haveI : PreconnectedSpace s := isPreconnected_iff_preconnectedSpace.mp hs.1
|
||||
simpa [f, detContinuous_eq_iff_det_eq] using
|
||||
(@IsPreconnected.subsingleton ℤ₂ _ _ _ (isPreconnected_range f.2))
|
||||
(Set.mem_range_self ⟨Λ, hs.2⟩) (Set.mem_range_self ⟨Λ', hΛ'⟩)
|
||||
(Set.mem_range_self ⟨Λ, hs.2⟩) (Set.mem_range_self ⟨Λ', hΛ'⟩)
|
||||
|
||||
lemma detRep_on_connected_component {Λ Λ' : LorentzGroup d} (h : Λ' ∈ connectedComponent Λ) :
|
||||
lemma detRep_on_connected_component {Λ Λ' : LorentzGroup d} (h : Λ' ∈ connectedComponent Λ) :
|
||||
detRep Λ = detRep Λ' := by
|
||||
simp [detRep_apply, detRep_apply, detContinuous]
|
||||
rw [det_on_connected_component h]
|
||||
|
|
@ -125,7 +125,7 @@ lemma IsProper_iff (Λ : LorentzGroup d) : IsProper Λ ↔ detRep Λ = 1 := by
|
|||
lemma id_IsProper : (@IsProper d) 1 := by
|
||||
simp [IsProper]
|
||||
|
||||
lemma isProper_on_connected_component {Λ Λ' : LorentzGroup d} (h : Λ' ∈ connectedComponent Λ) :
|
||||
lemma isProper_on_connected_component {Λ Λ' : LorentzGroup d} (h : Λ' ∈ connectedComponent Λ) :
|
||||
IsProper Λ ↔ IsProper Λ' := by
|
||||
simp [detRep_apply, detRep_apply, detContinuous]
|
||||
rw [det_on_connected_component h]
|
||||
|
|
|
|||
|
|
@ -64,7 +64,7 @@ lemma indexType_eq {T₁ T₂ : RealLorentzTensor d X} (h : T₁.color = T₂.co
|
|||
rw [h]
|
||||
|
||||
lemma ext {T₁ T₂ : RealLorentzTensor d X} (h : T₁.color = T₂.color)
|
||||
(h' : T₁.coord = T₂.coord ∘ Equiv.cast (indexType_eq h)) : T₁ = T₂ := by
|
||||
(h' : T₁.coord = T₂.coord ∘ Equiv.cast (indexType_eq h)) : T₁ = T₂ := by
|
||||
cases T₁
|
||||
cases T₂
|
||||
simp_all only [IndexType, mk.injEq]
|
||||
|
|
@ -97,7 +97,7 @@ def ch {X : FintypeCat} (x : X) (T : RealLorentzTensor d X) : Colors := T.color
|
|||
/-- An equivalence between `X → Fin 1 ⊕ Fin d` and `Y → Fin 1 ⊕ Fin d` given an isomorphism
|
||||
between `X` and `Y`. -/
|
||||
def congrSetIndexType (d : ℕ) (f : X ≃ Y) (i : X → Colors) :
|
||||
((x : X) → ColorsIndex d (i x)) ≃ ((y : Y) → ColorsIndex d ((Equiv.piCongrLeft' _ f) i y)) :=
|
||||
((x : X) → ColorsIndex d (i x)) ≃ ((y : Y) → ColorsIndex d ((Equiv.piCongrLeft' _ f) i y)) :=
|
||||
Equiv.piCongrLeft' _ (f)
|
||||
|
||||
/-- Given an equivalence of indexing sets, a map on Lorentz tensors. -/
|
||||
|
|
@ -106,8 +106,8 @@ def congrSetMap (f : X ≃ Y) (T : RealLorentzTensor d X) : RealLorentzTensor d
|
|||
color := (Equiv.piCongrLeft' _ f) T.color
|
||||
coord := (Equiv.piCongrLeft' _ (congrSetIndexType d f T.color)) T.coord
|
||||
|
||||
lemma congrSetMap_trans (f : X ≃ Y) (g : Y ≃ Z) (T : RealLorentzTensor d X) :
|
||||
congrSetMap g (congrSetMap f T) = congrSetMap (f.trans g) T := by
|
||||
lemma congrSetMap_trans (f : X ≃ Y) (g : Y ≃ Z) (T : RealLorentzTensor d X) :
|
||||
congrSetMap g (congrSetMap f T) = congrSetMap (f.trans g) T := by
|
||||
apply ext (by rfl)
|
||||
have h1 : (congrSetIndexType d (f.trans g) T.color) = (congrSetIndexType d f T.color).trans
|
||||
(congrSetIndexType d g ((Equiv.piCongrLeft' (fun _ => Colors) f) T.color)) := by
|
||||
|
|
|
|||
|
|
@ -81,7 +81,7 @@ noncomputable def toSelfAdjointMatrix :
|
|||
rw [← h01, RCLike.conj_eq_re_sub_im]
|
||||
rfl
|
||||
exact conj_eq_iff_re.mp (congrArg (fun M => M 1 1) $ selfAdjoint.mem_iff.mp x.2 )
|
||||
map_add' x y := by
|
||||
map_add' x y := by
|
||||
ext i j : 2
|
||||
simp only [toSelfAdjointMatrix'_coe, add_apply, ofReal_add, of_apply, cons_val', empty_val',
|
||||
cons_val_fin_one, AddSubmonoid.coe_add, AddSubgroup.coe_toAddSubmonoid, Matrix.add_apply]
|
||||
|
|
@ -109,22 +109,22 @@ noncomputable def toSelfAdjointMatrix :
|
|||
simp only [toSelfAdjointMatrix'_coe, Fin.isValue, of_apply, cons_val', empty_val',
|
||||
cons_val_fin_one, RingHom.id_apply, selfAdjoint.val_smul, smul_apply, real_smul]
|
||||
fin_cases i <;> fin_cases j
|
||||
· rw [show (r • x) (Sum.inl 0) = r * x (Sum.inl 0) from rfl]
|
||||
rw [show (r • x) (Sum.inr 2) = r * x (Sum.inr 2) from rfl]
|
||||
· rw [show (r • x) (Sum.inl 0) = r * x (Sum.inl 0) from rfl]
|
||||
rw [show (r • x) (Sum.inr 2) = r * x (Sum.inr 2) from rfl]
|
||||
simp only [Fin.isValue, ofReal_mul, Fin.zero_eta, cons_val_zero]
|
||||
ring
|
||||
· rw [show (r • x) (Sum.inr 0) = r * x (Sum.inr 0) from rfl]
|
||||
rw [show (r • x) (Sum.inr 1) = r * x (Sum.inr 1) from rfl]
|
||||
· rw [show (r • x) (Sum.inr 0) = r * x (Sum.inr 0) from rfl]
|
||||
rw [show (r • x) (Sum.inr 1) = r * x (Sum.inr 1) from rfl]
|
||||
simp only [Fin.isValue, ofReal_mul, Fin.mk_one, cons_val_one, head_cons, Fin.zero_eta,
|
||||
cons_val_zero]
|
||||
ring
|
||||
· rw [show (r • x) (Sum.inr 0) = r * x (Sum.inr 0) from rfl]
|
||||
rw [show (r • x) (Sum.inr 1) = r * x (Sum.inr 1) from rfl]
|
||||
· rw [show (r • x) (Sum.inr 0) = r * x (Sum.inr 0) from rfl]
|
||||
rw [show (r • x) (Sum.inr 1) = r * x (Sum.inr 1) from rfl]
|
||||
simp only [Fin.isValue, ofReal_mul, Fin.zero_eta, cons_val_zero, Fin.mk_one, cons_val_one,
|
||||
head_fin_const]
|
||||
ring
|
||||
· rw [show (r • x) (Sum.inl 0) = r * x (Sum.inl 0) from rfl]
|
||||
rw [show (r • x) (Sum.inr 2) = r * x (Sum.inr 2) from rfl]
|
||||
· rw [show (r • x) (Sum.inl 0) = r * x (Sum.inl 0) from rfl]
|
||||
rw [show (r • x) (Sum.inr 2) = r * x (Sum.inr 2) from rfl]
|
||||
simp only [Fin.isValue, ofReal_mul, Fin.mk_one, cons_val_one, head_cons, head_fin_const]
|
||||
ring
|
||||
|
||||
|
|
|
|||
|
|
@ -43,7 +43,7 @@ variable (v : LorentzVector d)
|
|||
|
||||
/-- The space components. -/
|
||||
@[simp]
|
||||
def space : EuclideanSpace ℝ (Fin d) := v ∘ Sum.inr
|
||||
def space : EuclideanSpace ℝ (Fin d) := v ∘ Sum.inr
|
||||
|
||||
/-- The time component. -/
|
||||
@[simp]
|
||||
|
|
|
|||
|
|
@ -36,7 +36,7 @@ def neg : NormOneLorentzVector d := ⟨- v, by
|
|||
simp only [map_neg, LinearMap.neg_apply, neg_neg]
|
||||
exact v.2⟩
|
||||
|
||||
lemma time_sq : v.1.time ^ 2 = 1 + ‖v.1.space‖ ^ 2 := by
|
||||
lemma time_sq : v.1.time ^ 2 = 1 + ‖v.1.space‖ ^ 2 := by
|
||||
rw [time_sq_eq_metric_add_space, v.2]
|
||||
|
||||
lemma abs_time_ge_one : 1 ≤ |v.1.time| := by
|
||||
|
|
@ -48,7 +48,7 @@ lemma norm_space_le_abs_time : ‖v.1.space‖ < |v.1.time| := by
|
|||
rw [(abs_norm _).symm, ← @sq_lt_sq, time_sq]
|
||||
exact lt_one_add (‖(v.1).space‖ ^ 2)
|
||||
|
||||
lemma norm_space_leq_abs_time : ‖v.1.space‖ ≤ |v.1.time| :=
|
||||
lemma norm_space_leq_abs_time : ‖v.1.space‖ ≤ |v.1.time| :=
|
||||
le_of_lt (norm_space_le_abs_time v)
|
||||
|
||||
lemma time_le_minus_one_or_ge_one : v.1.time ≤ -1 ∨ 1 ≤ v.1.time :=
|
||||
|
|
@ -77,7 +77,7 @@ lemma time_pos_iff : 0 < v.1.time ↔ 1 ≤ v.1.time := by
|
|||
· exact (time_nonneg_iff v).mp (le_of_lt h)
|
||||
· linarith
|
||||
|
||||
lemma time_abs_sub_space_norm :
|
||||
lemma time_abs_sub_space_norm :
|
||||
0 ≤ |v.1.time| * |w.1.time| - ‖v.1.space‖ * ‖w.1.space‖ := by
|
||||
apply sub_nonneg.mpr
|
||||
apply mul_le_mul (norm_space_leq_abs_time v) (norm_space_leq_abs_time w) ?_ ?_
|
||||
|
|
@ -167,7 +167,7 @@ lemma metric_reflect_mem_mem (h : v ∈ FuturePointing d) (hw : w ∈ FuturePoin
|
|||
exact abs_real_inner_le_norm (v.1).space (w.1).space
|
||||
|
||||
lemma metric_reflect_not_mem_not_mem (h : v ∉ FuturePointing d) (hw : w ∉ FuturePointing d) :
|
||||
0 ≤ ⟪v.1, w.1.spaceReflection⟫ₘ := by
|
||||
0 ≤ ⟪v.1, w.1.spaceReflection⟫ₘ := by
|
||||
have h1 := metric_reflect_mem_mem ((not_mem_iff_neg v).mp h) ((not_mem_iff_neg w).mp hw)
|
||||
apply le_of_le_of_eq h1 ?_
|
||||
simp [neg]
|
||||
|
|
@ -179,10 +179,10 @@ lemma metric_reflect_mem_not_mem (h : v ∈ FuturePointing d) (hw : w ∉ Future
|
|||
apply le_of_le_of_eq h1 ?_
|
||||
simp [neg]
|
||||
|
||||
lemma metric_reflect_not_mem_mem (h : v ∉ FuturePointing d) (hw : w ∈ FuturePointing d) :
|
||||
lemma metric_reflect_not_mem_mem (h : v ∉ FuturePointing d) (hw : w ∈ FuturePointing d) :
|
||||
⟪v.1, w.1.spaceReflection⟫ₘ ≤ 0 := by
|
||||
rw [show (0 : ℝ) = - 0 from zero_eq_neg.mpr rfl, le_neg]
|
||||
have h1 := metric_reflect_mem_mem ((not_mem_iff_neg v).mp h) hw
|
||||
have h1 := metric_reflect_mem_mem ((not_mem_iff_neg v).mp h) hw
|
||||
apply le_of_le_of_eq h1 ?_
|
||||
simp [neg]
|
||||
|
||||
|
|
@ -264,7 +264,7 @@ noncomputable def pathFromTime (u : FuturePointing d) : Path timeVecNormOneFutur
|
|||
|
||||
lemma isPathConnected : IsPathConnected (@Set.univ (FuturePointing d)) := by
|
||||
use timeVecNormOneFuture
|
||||
apply And.intro trivial ?_
|
||||
apply And.intro trivial ?_
|
||||
intro y a
|
||||
use pathFromTime y
|
||||
exact fun _ => a
|
||||
|
|
|
|||
|
|
@ -35,7 +35,7 @@ variable {d : ℕ}
|
|||
scoped[minkowskiMatrix] notation "η" => minkowskiMatrix
|
||||
|
||||
@[simp]
|
||||
lemma sq : @minkowskiMatrix d * minkowskiMatrix = 1 := by
|
||||
lemma sq : @minkowskiMatrix d * minkowskiMatrix = 1 := by
|
||||
simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
|
||||
ext1 i j
|
||||
rcases i with i | i <;> rcases j with j | j
|
||||
|
|
@ -58,7 +58,7 @@ lemma eq_transpose : minkowskiMatrixᵀ = @minkowskiMatrix d := by
|
|||
lemma det_eq_neg_one_pow_d : (@minkowskiMatrix d).det = (- 1) ^ d := by
|
||||
simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
|
||||
|
||||
lemma as_block : @minkowskiMatrix d = (
|
||||
lemma as_block : @minkowskiMatrix d = (
|
||||
Matrix.fromBlocks (1 : Matrix (Fin 1) (Fin 1) ℝ) 0 0 (-1 : Matrix (Fin d) (Fin d) ℝ)) := by
|
||||
rw [minkowskiMatrix]
|
||||
simp [LieAlgebra.Orthogonal.indefiniteDiagonal]
|
||||
|
|
@ -77,7 +77,7 @@ end minkowskiMatrix
|
|||
|
||||
-/
|
||||
|
||||
/-- Given a Lorentz vector `v` we define the the linear map `w ↦ v * η * w` -/
|
||||
/-- Given a Lorentz vector `v` we define the the linear map `w ↦ v * η * w`. -/
|
||||
@[simps!]
|
||||
def minkowskiLinearForm {d : ℕ} (v : LorentzVector d) : LorentzVector d →ₗ[ℝ] ℝ where
|
||||
toFun w := v ⬝ᵥ (minkowskiMatrix *ᵥ w)
|
||||
|
|
@ -90,7 +90,7 @@ def minkowskiLinearForm {d : ℕ} (v : LorentzVector d) : LorentzVector d →ₗ
|
|||
rfl
|
||||
|
||||
/-- The Minkowski metric as a bilinear map. -/
|
||||
def minkowskiMetric {d : ℕ} : LorentzVector d →ₗ[ℝ] LorentzVector d →ₗ[ℝ] ℝ where
|
||||
def minkowskiMetric {d : ℕ} : LorentzVector d →ₗ[ℝ] LorentzVector d →ₗ[ℝ] ℝ where
|
||||
toFun v := minkowskiLinearForm v
|
||||
map_add' y z := by
|
||||
ext1 x
|
||||
|
|
@ -134,7 +134,7 @@ lemma as_sum_self : ⟪v, v⟫ₘ = v.time ^ 2 - ‖v.space‖ ^ 2 := by
|
|||
rw [← real_inner_self_eq_norm_sq, PiLp.inner_apply, as_sum]
|
||||
noncomm_ring
|
||||
|
||||
lemma eq_time_minus_inner_prod : ⟪v, w⟫ₘ = v.time * w.time - ⟪v.space, w.space⟫_ℝ := by
|
||||
lemma eq_time_minus_inner_prod : ⟪v, w⟫ₘ = v.time * w.time - ⟪v.space, w.space⟫_ℝ := by
|
||||
rw [as_sum, @PiLp.inner_apply]
|
||||
noncomm_ring
|
||||
|
||||
|
|
@ -153,7 +153,7 @@ lemma time_sq_eq_metric_add_space : v.time ^ 2 = ⟪v, v⟫ₘ + ‖v.space‖ ^
|
|||
|
||||
/-!
|
||||
|
||||
# Minkowski metric and space reflections
|
||||
# Minkowski metric and space reflections
|
||||
|
||||
-/
|
||||
|
||||
|
|
@ -195,7 +195,7 @@ lemma nondegenerate : (∀ w, ⟪w, v⟫ₘ = 0) ↔ v = 0 := by
|
|||
|
||||
-/
|
||||
|
||||
lemma leq_time_sq : ⟪v, v⟫ₘ ≤ v.time ^ 2 := by
|
||||
lemma leq_time_sq : ⟪v, v⟫ₘ ≤ v.time ^ 2 := by
|
||||
rw [time_sq_eq_metric_add_space]
|
||||
exact (le_add_iff_nonneg_right _).mpr $ sq_nonneg ‖v.space‖
|
||||
|
||||
|
|
@ -227,7 +227,7 @@ lemma dual_id : @dual d 1 = 1 := by
|
|||
@[simp]
|
||||
lemma dual_mul : dual (Λ * Λ') = dual Λ' * dual Λ := by
|
||||
simp only [dual, transpose_mul]
|
||||
trans η * Λ'ᵀ * (η * η) * Λᵀ * η
|
||||
trans η * Λ'ᵀ * (η * η) * Λᵀ * η
|
||||
noncomm_ring [minkowskiMatrix.sq]
|
||||
noncomm_ring
|
||||
|
||||
|
|
@ -256,7 +256,7 @@ lemma det_dual : (dual Λ).det = Λ.det := by
|
|||
simp
|
||||
|
||||
@[simp]
|
||||
lemma dual_mulVec_right : ⟪x, (dual Λ) *ᵥ y⟫ₘ = ⟪Λ *ᵥ x, y⟫ₘ := by
|
||||
lemma dual_mulVec_right : ⟪x, (dual Λ) *ᵥ y⟫ₘ = ⟪Λ *ᵥ x, y⟫ₘ := by
|
||||
simp only [minkowskiMetric, LinearMap.coe_mk, AddHom.coe_mk, dual, minkowskiLinearForm_apply,
|
||||
mulVec_mulVec, ← mul_assoc, minkowskiMatrix.sq, one_mul, (vecMul_transpose Λ x).symm, ←
|
||||
dotProduct_mulVec]
|
||||
|
|
@ -265,7 +265,7 @@ lemma dual_mulVec_right : ⟪x, (dual Λ) *ᵥ y⟫ₘ = ⟪Λ *ᵥ x, y⟫ₘ
|
|||
lemma dual_mulVec_left : ⟪(dual Λ) *ᵥ x, y⟫ₘ = ⟪x, Λ *ᵥ y⟫ₘ := by
|
||||
rw [symm, dual_mulVec_right, symm]
|
||||
|
||||
lemma matrix_apply_eq_iff_sub : ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, Λ' *ᵥ w⟫ₘ ↔ ⟪v, (Λ - Λ') *ᵥ w⟫ₘ = 0 := by
|
||||
lemma matrix_apply_eq_iff_sub : ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, Λ' *ᵥ w⟫ₘ ↔ ⟪v, (Λ - Λ') *ᵥ w⟫ₘ = 0 := by
|
||||
rw [← sub_eq_zero, ← LinearMap.map_sub, sub_mulVec]
|
||||
|
||||
lemma matrix_eq_iff_eq_forall' : (∀ v, Λ *ᵥ v= Λ' *ᵥ v) ↔ ∀ w v, ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, Λ' *ᵥ w⟫ₘ := by
|
||||
|
|
@ -278,7 +278,7 @@ lemma matrix_eq_iff_eq_forall' : (∀ v, Λ *ᵥ v= Λ' *ᵥ v) ↔ ∀ w v, ⟪
|
|||
have h1 := h v
|
||||
rw [nondegenerate] at h1
|
||||
simp [sub_mulVec] at h1
|
||||
exact h1
|
||||
exact h1
|
||||
|
||||
lemma matrix_eq_iff_eq_forall : Λ = Λ' ↔ ∀ w v, ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, Λ' *ᵥ w⟫ₘ := by
|
||||
rw [← matrix_eq_iff_eq_forall']
|
||||
|
|
@ -302,7 +302,7 @@ lemma matrix_eq_id_iff : Λ = 1 ↔ ∀ w v, ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, w⟫
|
|||
-/
|
||||
|
||||
@[simp]
|
||||
lemma basis_left (μ : Fin 1 ⊕ Fin d) : ⟪e μ, v⟫ₘ = η μ μ * v μ := by
|
||||
lemma basis_left (μ : Fin 1 ⊕ Fin d) : ⟪e μ, v⟫ₘ = η μ μ * v μ := by
|
||||
rw [as_sum]
|
||||
rcases μ with μ | μ
|
||||
· fin_cases μ
|
||||
|
|
@ -314,7 +314,7 @@ lemma on_timeVec : ⟪timeVec, @timeVec d⟫ₘ = 1 := by
|
|||
LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_apply_eq, Sum.elim_inl, stdBasis_apply,
|
||||
↓reduceIte, mul_one]
|
||||
|
||||
lemma on_basis_mulVec (μ ν : Fin 1 ⊕ Fin d) : ⟪e μ, Λ *ᵥ e ν⟫ₘ = η μ μ * Λ μ ν := by
|
||||
lemma on_basis_mulVec (μ ν : Fin 1 ⊕ Fin d) : ⟪e μ, Λ *ᵥ e ν⟫ₘ = η μ μ * Λ μ ν := by
|
||||
simp [basis_left, mulVec, dotProduct, stdBasis_apply]
|
||||
|
||||
lemma on_basis (μ ν : Fin 1 ⊕ Fin d) : ⟪e μ, e ν⟫ₘ = η μ ν := by
|
||||
|
|
@ -324,8 +324,8 @@ lemma on_basis (μ ν : Fin 1 ⊕ Fin d) : ⟪e μ, e ν⟫ₘ = η μ ν := by
|
|||
· simp [h, LieAlgebra.Orthogonal.indefiniteDiagonal, minkowskiMatrix]
|
||||
exact fun a => False.elim (h (id (Eq.symm a)))
|
||||
|
||||
lemma matrix_apply_stdBasis (ν μ : Fin 1 ⊕ Fin d):
|
||||
Λ ν μ = η ν ν * ⟪e ν, Λ *ᵥ e μ⟫ₘ := by
|
||||
lemma matrix_apply_stdBasis (ν μ : Fin 1 ⊕ Fin d):
|
||||
Λ ν μ = η ν ν * ⟪e ν, Λ *ᵥ e μ⟫ₘ := by
|
||||
rw [on_basis_mulVec, ← mul_assoc]
|
||||
have h1 : η ν ν * η ν ν = 1 := by
|
||||
simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
|
||||
|
|
|
|||
|
|
@ -33,8 +33,8 @@ we can define a representation a representation of `SL(2, ℂ)` on spacetime.
|
|||
|
||||
-/
|
||||
|
||||
/-- Given an element `M ∈ SL(2, ℂ)` the linear map from `selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)` to
|
||||
itself defined by `A ↦ M * A * Mᴴ`. -/
|
||||
/-- Given an element `M ∈ SL(2, ℂ)` the linear map from `selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)` to
|
||||
itself defined by `A ↦ M * A * Mᴴ`. -/
|
||||
@[simps!]
|
||||
def toLinearMapSelfAdjointMatrix (M : SL(2, ℂ)) :
|
||||
selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) →ₗ[ℝ] selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) where
|
||||
|
|
@ -50,7 +50,7 @@ def toLinearMapSelfAdjointMatrix (M : SL(2, ℂ)) :
|
|||
noncomm_ring [selfAdjoint.val_smul, Algebra.mul_smul_comm, Algebra.smul_mul_assoc,
|
||||
RingHom.id_apply]
|
||||
|
||||
/-- The representation of `SL(2, ℂ)` on `selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)` given by
|
||||
/-- The representation of `SL(2, ℂ)` on `selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)` given by
|
||||
`M A ↦ M * A * Mᴴ`. -/
|
||||
@[simps!]
|
||||
def repSelfAdjointMatrix : Representation ℝ SL(2, ℂ) $ selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) where
|
||||
|
|
@ -63,7 +63,7 @@ def repSelfAdjointMatrix : Representation ℝ SL(2, ℂ) $ selfAdjoint (Matrix (
|
|||
noncomm_ring [toLinearMapSelfAdjointMatrix, SpecialLinearGroup.coe_mul, mul_assoc,
|
||||
conjTranspose_mul, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.mul_apply]
|
||||
|
||||
/-- The representation of `SL(2, ℂ)` on `spaceTime` obtained from `toSelfAdjointMatrix` and
|
||||
/-- The representation of `SL(2, ℂ)` on `spaceTime` obtained from `toSelfAdjointMatrix` and
|
||||
`repSelfAdjointMatrix`. -/
|
||||
def repLorentzVector : Representation ℝ SL(2, ℂ) (LorentzVector 3) where
|
||||
toFun M := toSelfAdjointMatrix.symm.comp ((repSelfAdjointMatrix M).comp
|
||||
|
|
@ -85,7 +85,7 @@ In the next section we will restrict this homomorphism to the restricted Lorentz
|
|||
|
||||
-/
|
||||
|
||||
lemma iff_det_selfAdjoint (Λ : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ): Λ ∈ LorentzGroup 3 ↔
|
||||
lemma iff_det_selfAdjoint (Λ : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ) : Λ ∈ LorentzGroup 3 ↔
|
||||
∀ (x : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)),
|
||||
det ((toSelfAdjointMatrix ∘
|
||||
toLin LorentzVector.stdBasis LorentzVector.stdBasis Λ ∘ toSelfAdjointMatrix.symm) x).1
|
||||
|
|
@ -107,7 +107,7 @@ def toLorentzGroupElem (M : SL(2, ℂ)) : LorentzGroup 3 :=
|
|||
|
||||
/-- The group homomorphism from ` SL(2, ℂ)` to the Lorentz group `𝓛`. -/
|
||||
@[simps!]
|
||||
def toLorentzGroup : SL(2, ℂ) →* LorentzGroup 3 where
|
||||
def toLorentzGroup : SL(2, ℂ) →* LorentzGroup 3 where
|
||||
toFun := toLorentzGroupElem
|
||||
map_one' := by
|
||||
simp only [toLorentzGroupElem, _root_.map_one, LinearMap.toMatrix_one]
|
||||
|
|
|
|||
|
|
@ -72,7 +72,7 @@ We also define the Higgs bundle.
|
|||
/-- The trivial vector bundle 𝓡² × ℂ². -/
|
||||
abbrev HiggsBundle := Bundle.Trivial SpaceTime HiggsVec
|
||||
|
||||
instance : SmoothVectorBundle HiggsVec HiggsBundle SpaceTime.asSmoothManifold :=
|
||||
instance : SmoothVectorBundle HiggsVec HiggsBundle SpaceTime.asSmoothManifold :=
|
||||
Bundle.Trivial.smoothVectorBundle HiggsVec 𝓘(ℝ, SpaceTime)
|
||||
|
||||
/-- A Higgs field is a smooth section of the Higgs bundle. -/
|
||||
|
|
@ -133,11 +133,11 @@ lemma apply_smooth (φ : HiggsField) :
|
|||
(smooth_pi_space).mp (φ.toVec_smooth)
|
||||
|
||||
lemma apply_re_smooth (φ : HiggsField) (i : Fin 2) :
|
||||
Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) (reCLM ∘ (fun (x : SpaceTime) => (φ x i))) :=
|
||||
Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) (reCLM ∘ (fun (x : SpaceTime) => (φ x i))) :=
|
||||
(ContinuousLinearMap.smooth reCLM).comp (φ.apply_smooth i)
|
||||
|
||||
lemma apply_im_smooth (φ : HiggsField) (i : Fin 2) :
|
||||
Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) (imCLM ∘ (fun (x : SpaceTime) => (φ x i))) :=
|
||||
Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) (imCLM ∘ (fun (x : SpaceTime) => (φ x i))) :=
|
||||
(ContinuousLinearMap.smooth imCLM).comp (φ.apply_smooth i)
|
||||
|
||||
/-!
|
||||
|
|
|
|||
|
|
@ -34,9 +34,9 @@ open ComplexConjugate
|
|||
@[simps!]
|
||||
noncomputable def higgsRepUnitary : GaugeGroup →* unitaryGroup (Fin 2) ℂ where
|
||||
toFun g := repU1 g.2.2 * fundamentalSU2 g.2.1
|
||||
map_mul' := by
|
||||
map_mul' := by
|
||||
intro ⟨_, a2, a3⟩ ⟨_, b2, b3⟩
|
||||
change repU1 (a3 * b3) * fundamentalSU2 (a2 * b2) = _
|
||||
change repU1 (a3 * b3) * fundamentalSU2 (a2 * b2) = _
|
||||
rw [repU1.map_mul, fundamentalSU2.map_mul, mul_assoc, mul_assoc,
|
||||
← mul_assoc (repU1 b3) _ _, repU1_fundamentalSU2_commute]
|
||||
repeat rw [mul_assoc]
|
||||
|
|
@ -97,31 +97,31 @@ def rotateMatrix (φ : HiggsVec) : Matrix (Fin 2) (Fin 2) ℂ :=
|
|||
|
||||
lemma rotateMatrix_star (φ : HiggsVec) :
|
||||
star φ.rotateMatrix =
|
||||
![![conj (φ 1) /‖φ‖ , φ 0 /‖φ‖], ![- conj (φ 0) / ‖φ‖ , φ 1 / ‖φ‖] ] := by
|
||||
![![conj (φ 1) /‖φ‖ , φ 0 /‖φ‖], ![- conj (φ 0) / ‖φ‖ , φ 1 / ‖φ‖] ] := by
|
||||
simp_rw [star, rotateMatrix, conjTranspose]
|
||||
ext i j
|
||||
fin_cases i <;> fin_cases j <;> simp [conj_ofReal]
|
||||
|
||||
lemma rotateMatrix_det {φ : HiggsVec} (hφ : φ ≠ 0) : (rotateMatrix φ).det = 1 := by
|
||||
have h1 : (‖φ‖ : ℂ) ≠ 0 := ofReal_inj.mp.mt (norm_ne_zero_iff.mpr hφ)
|
||||
have h1 : (‖φ‖ : ℂ) ≠ 0 := ofReal_inj.mp.mt (norm_ne_zero_iff.mpr hφ)
|
||||
field_simp [rotateMatrix, det_fin_two]
|
||||
rw [← ofReal_mul, ← sq, ← @real_inner_self_eq_norm_sq]
|
||||
simp [PiLp.inner_apply, Complex.inner, neg_mul, sub_neg_eq_add,
|
||||
simp [PiLp.inner_apply, Complex.inner, neg_mul, sub_neg_eq_add,
|
||||
Fin.sum_univ_two, ofReal_add, ofReal_mul, mul_conj, mul_comm, add_comm]
|
||||
|
||||
lemma rotateMatrix_unitary {φ : HiggsVec} (hφ : φ ≠ 0) :
|
||||
(rotateMatrix φ) ∈ unitaryGroup (Fin 2) ℂ := by
|
||||
rw [mem_unitaryGroup_iff', rotateMatrix_star, rotateMatrix]
|
||||
erw [mul_fin_two, one_fin_two]
|
||||
have : (‖φ‖ : ℂ) ≠ 0 := ofReal_inj.mp.mt (norm_ne_zero_iff.mpr hφ)
|
||||
have : (‖φ‖ : ℂ) ≠ 0 := ofReal_inj.mp.mt (norm_ne_zero_iff.mpr hφ)
|
||||
ext i j
|
||||
fin_cases i <;> fin_cases j <;> field_simp
|
||||
<;> rw [← ofReal_mul, ← sq, ← @real_inner_self_eq_norm_sq]
|
||||
· simp [PiLp.inner_apply, Complex.inner, neg_mul, sub_neg_eq_add,
|
||||
· simp [PiLp.inner_apply, Complex.inner, neg_mul, sub_neg_eq_add,
|
||||
Fin.sum_univ_two, ofReal_add, ofReal_mul, mul_conj, mul_comm, add_comm]
|
||||
· ring_nf
|
||||
· ring_nf
|
||||
· simp [PiLp.inner_apply, Complex.inner, neg_mul, sub_neg_eq_add,
|
||||
· simp [PiLp.inner_apply, Complex.inner, neg_mul, sub_neg_eq_add,
|
||||
Fin.sum_univ_two, ofReal_add, ofReal_mul, mul_conj, mul_comm]
|
||||
|
||||
lemma rotateMatrix_specialUnitary {φ : HiggsVec} (hφ : φ ≠ 0) :
|
||||
|
|
@ -147,10 +147,10 @@ lemma rotateGuageGroup_apply {φ : HiggsVec} (hφ : φ ≠ 0) :
|
|||
· simp only [Fin.mk_one, Fin.isValue, cons_val_one, head_cons, mulVec, Fin.isValue,
|
||||
cons_val', empty_val', cons_val_fin_one, vecHead, cons_dotProduct, vecTail, Nat.succ_eq_add_one,
|
||||
Nat.reduceAdd, Function.comp_apply, Fin.succ_zero_eq_one, dotProduct_empty, add_zero]
|
||||
have : (‖φ‖ : ℂ) ≠ 0 := ofReal_inj.mp.mt (norm_ne_zero_iff.mpr hφ)
|
||||
have : (‖φ‖ : ℂ) ≠ 0 := ofReal_inj.mp.mt (norm_ne_zero_iff.mpr hφ)
|
||||
field_simp
|
||||
rw [← ofReal_mul, ← sq, ← @real_inner_self_eq_norm_sq]
|
||||
simp [PiLp.inner_apply, Complex.inner, neg_mul, sub_neg_eq_add,
|
||||
simp [PiLp.inner_apply, Complex.inner, neg_mul, sub_neg_eq_add,
|
||||
Fin.sum_univ_two, ofReal_add, ofReal_mul, mul_conj, mul_comm]
|
||||
|
||||
theorem rotate_fst_zero_snd_real (φ : HiggsVec) :
|
||||
|
|
@ -166,7 +166,7 @@ theorem rotate_fst_zero_snd_real (φ : HiggsVec) :
|
|||
end HiggsVec
|
||||
|
||||
/-! TODO: Define the global gauge action on HiggsField. -/
|
||||
/-! TODO: Prove `⟪φ1, φ2⟫_H` invariant under the global gauge action. (norm_map_of_mem_unitary) -/
|
||||
/-! TODO: Prove `⟪φ1, φ2⟫_H` invariant under the global gauge action. (norm_map_of_mem_unitary) -/
|
||||
/-! TODO: Prove invariance of potential under global gauge action. -/
|
||||
|
||||
end StandardModel
|
||||
|
|
|
|||
|
|
@ -55,13 +55,13 @@ lemma innerProd_left_zero (φ : HiggsField) : ⟪0, φ⟫_H = 0 := by
|
|||
lemma innerProd_right_zero (φ : HiggsField) : ⟪φ, 0⟫_H = 0 := by
|
||||
funext x
|
||||
simp [innerProd]
|
||||
example (x : ℝ): RCLike.ofReal x = ofReal' x := by
|
||||
example (x : ℝ): RCLike.ofReal x = ofReal' x := by
|
||||
rfl
|
||||
lemma innerProd_expand (φ1 φ2 : HiggsField) :
|
||||
⟪φ1, φ2⟫_H = fun x => equivRealProdCLM.symm (((φ1 x 0).re * (φ2 x 0).re
|
||||
⟪φ1, φ2⟫_H = fun x => equivRealProdCLM.symm (((φ1 x 0).re * (φ2 x 0).re
|
||||
+ (φ1 x 1).re * (φ2 x 1).re+ (φ1 x 0).im * (φ2 x 0).im + (φ1 x 1).im * (φ2 x 1).im),
|
||||
((φ1 x 0).re * (φ2 x 0).im + (φ1 x 1).re * (φ2 x 1).im
|
||||
- (φ1 x 0).im * (φ2 x 0).re - (φ1 x 1).im * (φ2 x 1).re)) := by
|
||||
- (φ1 x 0).im * (φ2 x 0).re - (φ1 x 1).im * (φ2 x 1).re)) := by
|
||||
funext x
|
||||
simp only [innerProd, PiLp.inner_apply, RCLike.inner_apply, Fin.sum_univ_two,
|
||||
equivRealProdCLM_symm_apply, ofReal_add, ofReal_mul, ofReal_sub]
|
||||
|
|
@ -124,9 +124,9 @@ lemma normSq_eq_innerProd_self (φ : HiggsField) (x : SpaceTime) :
|
|||
-/
|
||||
|
||||
lemma toHiggsVec_norm (φ : HiggsField) (x : SpaceTime) :
|
||||
‖φ x‖ = ‖φ.toHiggsVec x‖ := rfl
|
||||
‖φ x‖ = ‖φ.toHiggsVec x‖ := rfl
|
||||
|
||||
lemma normSq_expand (φ : HiggsField) :
|
||||
lemma normSq_expand (φ : HiggsField) :
|
||||
φ.normSq = fun x => (conj (φ x 0) * (φ x 0) + conj (φ x 1) * (φ x 1)).re := by
|
||||
funext x
|
||||
simp [normSq, add_re, mul_re, conj_re, conj_im, neg_mul, sub_neg_eq_add, @norm_sq_eq_inner ℂ]
|
||||
|
|
|
|||
|
|
@ -34,7 +34,7 @@ open SpaceTime
|
|||
|
||||
/-- The Higgs potential of the form `- μ² * |φ|² + 𝓵 * |φ|⁴`. -/
|
||||
@[simp]
|
||||
def potential (μ2 𝓵 : ℝ ) (φ : HiggsField) (x : SpaceTime) : ℝ :=
|
||||
def potential (μ2 𝓵 : ℝ ) (φ : HiggsField) (x : SpaceTime) : ℝ :=
|
||||
- μ2 * ‖φ‖_H ^ 2 x + 𝓵 * ‖φ‖_H ^ 2 x * ‖φ‖_H ^ 2 x
|
||||
|
||||
/-!
|
||||
|
|
@ -94,7 +94,7 @@ lemma snd_term_nonneg (φ : HiggsField) (x : SpaceTime) :
|
|||
and_self]
|
||||
|
||||
lemma as_quad (μ2 𝓵 : ℝ) (φ : HiggsField) (x : SpaceTime) :
|
||||
𝓵 * ‖φ‖_H ^ 2 x * ‖φ‖_H ^ 2 x + (- μ2 ) * ‖φ‖_H ^ 2 x + (- potential μ2 𝓵 φ x) = 0 := by
|
||||
𝓵 * ‖φ‖_H ^ 2 x * ‖φ‖_H ^ 2 x + (- μ2 ) * ‖φ‖_H ^ 2 x + (- potential μ2 𝓵 φ x) = 0 := by
|
||||
simp only [normSq, neg_mul, potential, neg_add_rev, neg_neg]
|
||||
ring
|
||||
|
||||
|
|
@ -121,7 +121,7 @@ lemma eq_zero_at (φ : HiggsField) (x : SpaceTime)
|
|||
ring_nf
|
||||
linear_combination h2
|
||||
|
||||
lemma eq_zero_at_of_μSq_nonpos {μ2 : ℝ} (hμ2 : μ2 ≤ 0)
|
||||
lemma eq_zero_at_of_μSq_nonpos {μ2 : ℝ} (hμ2 : μ2 ≤ 0)
|
||||
(φ : HiggsField) (x : SpaceTime) (hV : potential μ2 𝓵 φ x = 0) : φ x = 0 := by
|
||||
cases' (eq_zero_at μ2 h𝓵 φ x hV) with h1 h1
|
||||
exact h1
|
||||
|
|
@ -141,7 +141,7 @@ lemma bounded_below (φ : HiggsField) (x : SpaceTime) :
|
|||
ring_nf at h1
|
||||
rw [← neg_le_iff_add_nonneg'] at h1
|
||||
rw [show 𝓵 * potential μ2 𝓵 φ x * 4 = (4 * 𝓵) * potential μ2 𝓵 φ x by ring] at h1
|
||||
have h2 := (div_le_iff' (by simp [h𝓵] : 0 < 4 * 𝓵)).mpr h1
|
||||
have h2 := (div_le_iff' (by simp [h𝓵] : 0 < 4 * 𝓵)).mpr h1
|
||||
ring_nf at h2 ⊢
|
||||
exact h2
|
||||
|
||||
|
|
@ -165,13 +165,13 @@ variable (h𝓵 : 0 < 𝓵)
|
|||
-/
|
||||
|
||||
lemma discrim_eq_zero_of_eq_bound (φ : HiggsField) (x : SpaceTime)
|
||||
(hV : potential μ2 𝓵 φ x = - μ2 ^ 2 / (4 * 𝓵)) :
|
||||
(hV : potential μ2 𝓵 φ x = - μ2 ^ 2 / (4 * 𝓵)) :
|
||||
discrim 𝓵 (- μ2) (- potential μ2 𝓵 φ x) = 0 := by
|
||||
rw [discrim, hV]
|
||||
field_simp
|
||||
|
||||
lemma normSq_of_eq_bound (φ : HiggsField) (x : SpaceTime)
|
||||
(hV : potential μ2 𝓵 φ x = - μ2 ^ 2 / (4 * 𝓵)) :
|
||||
(hV : potential μ2 𝓵 φ x = - μ2 ^ 2 / (4 * 𝓵)) :
|
||||
‖φ‖_H ^ 2 x = μ2 / (2 * 𝓵) := by
|
||||
have h1 := as_quad μ2 𝓵 φ x
|
||||
rw [quadratic_eq_zero_iff_of_discrim_eq_zero _
|
||||
|
|
@ -180,7 +180,7 @@ lemma normSq_of_eq_bound (φ : HiggsField) (x : SpaceTime)
|
|||
exact ne_of_gt h𝓵
|
||||
|
||||
lemma eq_bound_iff (φ : HiggsField) (x : SpaceTime) :
|
||||
potential μ2 𝓵 φ x = - μ2 ^ 2 / (4 * 𝓵) ↔ ‖φ‖_H ^ 2 x = μ2 / (2 * 𝓵) :=
|
||||
potential μ2 𝓵 φ x = - μ2 ^ 2 / (4 * 𝓵) ↔ ‖φ‖_H ^ 2 x = μ2 / (2 * 𝓵) :=
|
||||
Iff.intro (normSq_of_eq_bound μ2 h𝓵 φ x)
|
||||
(fun h ↦ by
|
||||
rw [potential, h]
|
||||
|
|
|
|||
|
|
@ -39,7 +39,7 @@ def doubleSpaceLinter : HepLeanTextLinter := fun lines ↦ Id.run do
|
|||
let k := (Substring.findAllSubstr l " ").toList.getLast?
|
||||
let col := match k with
|
||||
| none => 1
|
||||
| some k => k.stopPos.byteIdx
|
||||
| some k => String.offsetOfPos l k.stopPos
|
||||
some (s!" Non-initial double space in line.", lno, col)
|
||||
else none)
|
||||
errors.toArray
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue