Update Basic.lean
This commit is contained in:
Pietro Monticone
parent
4cdab9f4c5
commit
7427ce4207
1 changed files with 18 additions and 42 deletions
|
|
@ -51,7 +51,7 @@ instance : NormedAddCommGroup (Fin 2 → ℂ) := by
|
|||
/-- Given a vector `ℂ²` the constant higgs field with value equal to that
|
||||
section. -/
|
||||
noncomputable def higgsVec.toField (φ : higgsVec) : higgsField where
|
||||
toFun := fun _ => φ
|
||||
toFun := fun _ ↦ φ
|
||||
contMDiff_toFun := by
|
||||
intro x
|
||||
rw [Bundle.contMDiffAt_section]
|
||||
|
|
@ -63,7 +63,6 @@ open Complex Real
|
|||
/-- Given a `higgsField`, the corresponding map from `spaceTime` to `higgsVec`. -/
|
||||
def toHiggsVec (φ : higgsField) : spaceTime → higgsVec := φ
|
||||
|
||||
|
||||
lemma toHiggsVec_smooth (φ : higgsField) : Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, higgsVec) φ.toHiggsVec := by
|
||||
intro x0
|
||||
have h1 := φ.contMDiff x0
|
||||
|
|
@ -76,29 +75,25 @@ lemma toHiggsVec_smooth (φ : higgsField) : Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ
|
|||
exact h1
|
||||
|
||||
lemma toField_toHiggsVec_apply (φ : higgsField) (x : spaceTime) :
|
||||
(φ.toHiggsVec x).toField x = φ x := by
|
||||
rfl
|
||||
(φ.toHiggsVec x).toField x = φ x := rfl
|
||||
|
||||
lemma higgsVecToFin2ℂ_toHiggsVec (φ : higgsField) : higgsVecToFin2ℂ ∘ φ.toHiggsVec = φ := by
|
||||
ext x
|
||||
rfl
|
||||
lemma higgsVecToFin2ℂ_toHiggsVec (φ : higgsField) :
|
||||
higgsVecToFin2ℂ ∘ φ.toHiggsVec = φ := rfl
|
||||
|
||||
lemma toVec_smooth (φ : higgsField) : Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, Fin 2 → ℂ) φ := by
|
||||
rw [← φ.higgsVecToFin2ℂ_toHiggsVec]
|
||||
exact Smooth.comp smooth_higgsVecToFin2ℂ (φ.toHiggsVec_smooth)
|
||||
lemma toVec_smooth (φ : higgsField) : Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, Fin 2 → ℂ) φ :=
|
||||
smooth_higgsVecToFin2ℂ.comp φ.toHiggsVec_smooth
|
||||
|
||||
lemma apply_smooth (φ : higgsField) :
|
||||
∀ i, Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, ℂ) (fun (x : spaceTime) => (φ x i)) := by
|
||||
rw [← smooth_pi_space]
|
||||
exact φ.toVec_smooth
|
||||
∀ i, Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, ℂ) (fun (x : spaceTime) => (φ x i)) :=
|
||||
(smooth_pi_space).mp (φ.toVec_smooth)
|
||||
|
||||
lemma apply_re_smooth (φ : higgsField) (i : Fin 2):
|
||||
Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, ℝ) (reCLM ∘ (fun (x : spaceTime) => (φ x i))) :=
|
||||
Smooth.comp (ContinuousLinearMap.smooth reCLM) (φ.apply_smooth 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.comp (ContinuousLinearMap.smooth imCLM) (φ.apply_smooth i)
|
||||
(ContinuousLinearMap.smooth imCLM).comp (φ.apply_smooth i)
|
||||
|
||||
/-- Given two `higgsField`, the map `spaceTime → ℂ` obtained by taking their inner product. -/
|
||||
def innerProd (φ1 φ2 : higgsField) : spaceTime → ℂ := fun x => ⟪φ1 x, φ2 x⟫_ℂ
|
||||
|
|
@ -115,9 +110,7 @@ lemma toHiggsVec_norm (φ : higgsField) (x : spaceTime) :
|
|||
lemma normSq_expand (φ : higgsField) :
|
||||
φ.normSq = fun x => (conj (φ x 0) * (φ x 0) + conj (φ x 1) * (φ x 1) ).re := by
|
||||
funext x
|
||||
simp only [normSq, add_re, mul_re, conj_re, conj_im, neg_mul, sub_neg_eq_add]
|
||||
rw [@norm_sq_eq_inner ℂ]
|
||||
simp
|
||||
simp [normSq, add_re, mul_re, conj_re, conj_im, neg_mul, sub_neg_eq_add, @norm_sq_eq_inner ℂ]
|
||||
|
||||
lemma normSq_smooth (φ : higgsField) : Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, ℝ) φ.normSq := by
|
||||
rw [normSq_expand]
|
||||
|
|
@ -140,10 +133,10 @@ lemma normSq_smooth (φ : higgsField) : Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ,
|
|||
exact φ.apply_im_smooth 1
|
||||
|
||||
lemma normSq_nonneg (φ : higgsField) (x : spaceTime) : 0 ≤ φ.normSq x := by
|
||||
simp only [normSq, ge_iff_le, norm_nonneg, pow_nonneg]
|
||||
simp [normSq, ge_iff_le, norm_nonneg, pow_nonneg]
|
||||
|
||||
lemma normSq_zero (φ : higgsField) (x : spaceTime) : φ.normSq x = 0 ↔ φ x = 0 := by
|
||||
simp only [normSq, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, norm_eq_zero]
|
||||
simp [normSq, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, norm_eq_zero]
|
||||
|
||||
/-- The Higgs potential of the form `- μ² * |φ|² + λ * |φ|⁴`. -/
|
||||
@[simp]
|
||||
|
|
@ -153,10 +146,8 @@ def potential (φ : higgsField) (μSq lambda : ℝ ) (x : spaceTime) : ℝ :=
|
|||
lemma potential_smooth (φ : higgsField) (μSq lambda : ℝ) :
|
||||
Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, ℝ) (fun x => φ.potential μSq lambda x) := by
|
||||
simp only [potential, normSq, neg_mul]
|
||||
exact Smooth.add
|
||||
(Smooth.neg (Smooth.smul smooth_const φ.normSq_smooth))
|
||||
(Smooth.smul (Smooth.smul smooth_const φ.normSq_smooth) φ.normSq_smooth)
|
||||
|
||||
exact (smooth_const.smul φ.normSq_smooth).neg.add
|
||||
((smooth_const.smul φ.normSq_smooth).smul φ.normSq_smooth)
|
||||
|
||||
lemma potential_apply (φ : higgsField) (μSq lambda : ℝ) (x : spaceTime) :
|
||||
(φ.potential μSq lambda) x = higgsVec.potential μSq lambda (φ.toHiggsVec x) := by
|
||||
|
|
@ -171,35 +162,20 @@ lemma isConst_of_higgsVec (φ : higgsVec) : φ.toField.isConst := by
|
|||
intro x _
|
||||
simp [higgsVec.toField]
|
||||
|
||||
lemma isConst_iff_of_higgsVec (Φ : higgsField) : Φ.isConst ↔ ∃ (φ : higgsVec), Φ = φ.toField := by
|
||||
apply Iff.intro
|
||||
intro h
|
||||
use Φ 0
|
||||
ext x y
|
||||
rw [← h x 0]
|
||||
rfl
|
||||
intro h
|
||||
intro x y
|
||||
obtain ⟨φ, hφ⟩ := h
|
||||
subst hφ
|
||||
rfl
|
||||
lemma isConst_iff_of_higgsVec (Φ : higgsField) : Φ.isConst ↔ ∃ (φ : higgsVec), Φ = φ.toField :=
|
||||
Iff.intro (fun h ↦ ⟨Φ 0, by ext x y; rw [← h x 0]; rfl⟩) (fun ⟨φ, hφ⟩ x y ↦ by subst hφ; rfl)
|
||||
|
||||
lemma normSq_of_higgsVec (φ : higgsVec) : φ.toField.normSq = fun x => (norm φ) ^ 2 := by
|
||||
simp only [normSq, higgsVec.toField]
|
||||
funext x
|
||||
simp
|
||||
simp [normSq, higgsVec.toField]
|
||||
|
||||
lemma potential_of_higgsVec (φ : higgsVec) (μSq lambda : ℝ) :
|
||||
φ.toField.potential μSq lambda = fun _ => higgsVec.potential μSq lambda φ := by
|
||||
simp [higgsVec.potential]
|
||||
unfold potential
|
||||
rw [normSq_of_higgsVec]
|
||||
funext x
|
||||
simp only [neg_mul, add_right_inj]
|
||||
ring_nf
|
||||
|
||||
|
||||
|
||||
end higgsField
|
||||
end
|
||||
end StandardModel
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue