Update TargetSpace.lean

This commit is contained in:
Pietro Monticone 2024-06-08 03:47:17 +02:00
parent 7427ce4207
commit ea6c61eb29

View file

@ -46,10 +46,8 @@ section higgsVec
casting vectors. -/
def higgsVecToFin2 : higgsVec →L[] (Fin 2 → ) where
toFun x := x
map_add' x y := by
simp
map_smul' a x := by
simp
map_add' x y := by simp
map_smul' a x := by simp
lemma smooth_higgsVecToFin2 : Smooth 𝓘(, higgsVec) 𝓘(, Fin 2 → ) higgsVecToFin2 :=
ContinuousLinearMap.smooth higgsVecToFin2
@ -63,11 +61,10 @@ noncomputable def higgsRepUnitary : gaugeGroup →* unitaryGroup (Fin 2) whe
map_mul' := by
intro ⟨_, a2, a3⟩ ⟨_, b2, b3⟩
change repU1 (a3 * b3) * fundamentalSU2 (a2 * b2) = _
rw [repU1.map_mul, fundamentalSU2.map_mul]
rw [mul_assoc, mul_assoc, ← mul_assoc (repU1 b3) _ _, repU1_fundamentalSU2_commute]
rw [repU1.map_mul, fundamentalSU2.map_mul, mul_assoc, mul_assoc,
← mul_assoc (repU1 b3) _ _, repU1_fundamentalSU2_commute]
repeat rw [mul_assoc]
map_one' := by
simp only [Prod.snd_one, _root_.map_one, Prod.fst_one, mul_one]
map_one' := by simp
/-- An orthonormal basis of higgsVec. -/
noncomputable def orthonormBasis : OrthonormalBasis (Fin 2) higgsVec :=
@ -87,20 +84,16 @@ lemma matrixToLin_star (g : Matrix (Fin 2) (Fin 2) ) :
lemma matrixToLin_unitary (g : unitaryGroup (Fin 2) ) :
matrixToLin g ∈ unitary (higgsVec →L[] higgsVec) := by
rw [@unitary.mem_iff, ← matrixToLin_star, ← matrixToLin.map_mul, ← matrixToLin.map_mul]
rw [mem_unitaryGroup_iff.mp g.prop, mem_unitaryGroup_iff'.mp g.prop, matrixToLin.map_one]
rw [@unitary.mem_iff, ← matrixToLin_star, ← matrixToLin.map_mul, ← matrixToLin.map_mul,
mem_unitaryGroup_iff.mp g.prop, mem_unitaryGroup_iff'.mp g.prop, matrixToLin.map_one]
simp
/-- The natural homomorphism from unitary `2×2` complex matrices to unitary transformations
of `higgsVec`. -/
noncomputable def unitaryToLin : unitaryGroup (Fin 2) →* unitary (higgsVec →L[] higgsVec) where
toFun g := ⟨matrixToLin g, matrixToLin_unitary g⟩
map_mul' g h := by
ext
simp
map_one' := by
ext
simp
map_mul' g h := by simp
map_one' := by simp
/-- The inclusion of unitary transformations on `higgsVec` into all linear transformations. -/
@[simps!]
@ -114,8 +107,7 @@ def rep : Representation gaugeGroup higgsVec :=
lemma higgsRepUnitary_mul (g : gaugeGroup) (φ : higgsVec) :
(higgsRepUnitary g).1 *ᵥ φ = g.2.2 ^ 3 • (g.2.1.1 *ᵥ φ) := by
simp only [higgsRepUnitary_apply_coe]
exact smul_mulVec_assoc (g.2.2 ^ 3) (g.2.1.1) φ
simp [higgsRepUnitary_apply_coe, smul_mulVec_assoc]
lemma rep_apply (g : gaugeGroup) (φ : higgsVec) : rep g φ = g.2.2 ^ 3 • (g.2.1.1 *ᵥ φ) :=
higgsRepUnitary_mul g φ
@ -133,13 +125,11 @@ def potential (φ : higgsVec) : := - μSq * ‖φ‖ ^ 2 + λ * ‖φ‖ ^
lemma potential_invariant (φ : higgsVec) (g : gaugeGroup) :
potential μSq (λ) (rep g φ) = potential μSq (λ) φ := by
simp only [potential, neg_mul]
rw [norm_invariant]
simp only [potential, neg_mul, norm_invariant]
lemma potential_as_quad (φ : higgsVec) :
λ * ‖φ‖ ^ 2 * ‖φ‖ ^ 2 + (- μSq ) * ‖φ‖ ^ 2 + (- potential μSq (λ) φ) = 0 := by
simp [potential]
ring
simp [potential]; ring
end potentialDefn
section potentialProp
@ -161,11 +151,9 @@ lemma zero_le_potential_discrim (φ : higgsVec) :
0 ≤ discrim (λ) (- μSq ) (- potential μSq (λ) φ) := by
have h1 := potential_as_quad μSq (λ) φ
rw [quadratic_eq_zero_iff_discrim_eq_sq] at h1
rw [h1]
exact sq_nonneg (2 * (lambda ) * ‖φ‖ ^ 2 + -μSq)
simp only [ne_eq, div_eq_zero_iff, OfNat.ofNat_ne_zero, or_false]
exact ne_of_gt hLam
· simp only [h1, ne_eq, div_eq_zero_iff, OfNat.ofNat_ne_zero, or_false]
exact sq_nonneg (2 * lambda * ‖φ‖ ^ 2 + -μSq)
· exact ne_of_gt hLam
lemma potential_eq_zero_sol (φ : higgsVec)
(hV : potential μSq (λ) φ = 0) : φ = 0 ‖φ‖ ^ 2 = μSq / λ := by
@ -209,19 +197,14 @@ lemma potential_bounded_below (φ : higgsVec) :
lemma potential_bounded_below_of_μSq_nonpos {μSq : }
(hμSq : μSq ≤ 0) (φ : higgsVec) : 0 ≤ potential μSq (λ) φ := by
simp only [potential, neg_mul, add_zero]
refine add_nonneg ?_ (potential_snd_term_nonneg hLam φ)
field_simp
rw [@mul_nonpos_iff]
simp_all only [ge_iff_le, norm_nonneg, pow_nonneg, and_self, or_true]
field_simp [mul_nonpos_iff]
simp_all [ge_iff_le, norm_nonneg, pow_nonneg, and_self, or_true]
lemma potential_eq_bound_discrim_zero (φ : higgsVec)
(hV : potential μSq (λ) φ = - μSq ^ 2 / (4 * λ)) :
discrim (λ) (- μSq) (- potential μSq (λ) φ) = 0 := by
simp [discrim, hV]
field_simp
ring
field_simp [discrim, hV]
lemma potential_eq_bound_higgsVec_sq (φ : higgsVec)
(hV : potential μSq (λ) φ = - μSq ^ 2 / (4 * (λ))) :
@ -229,81 +212,59 @@ lemma potential_eq_bound_higgsVec_sq (φ : higgsVec)
have h1 := potential_as_quad μSq (λ) φ
rw [quadratic_eq_zero_iff_of_discrim_eq_zero _
(potential_eq_bound_discrim_zero μSq hLam φ hV)] at h1
rw [h1]
field_simp
ring_nf
simp only [ne_eq, div_eq_zero_iff, OfNat.ofNat_ne_zero, or_false]
simp_rw [h1, neg_neg]
exact ne_of_gt hLam
lemma potential_eq_bound_iff (φ : higgsVec) :
potential μSq (λ) φ = - μSq ^ 2 / (4 * (λ)) ↔ ‖φ‖ ^ 2 = μSq / (2 * (λ)) := by
apply Iff.intro
· intro h
exact potential_eq_bound_higgsVec_sq μSq hLam φ h
· intro h
have hv : ‖φ‖ ^ 4 = ‖φ‖ ^ 2 * ‖φ‖ ^ 2 := by
ring_nf
potential μSq (λ) φ = - μSq ^ 2 / (4 * (λ)) ↔ ‖φ‖ ^ 2 = μSq / (2 * (λ)) :=
Iff.intro (potential_eq_bound_higgsVec_sq μSq hLam φ)
(fun h ↦ by
have hv : ‖φ‖ ^ 4 = ‖φ‖ ^ 2 * ‖φ‖ ^ 2 := by ring_nf
field_simp [potential, hv, h]
ring
ring_nf)
lemma potential_eq_bound_iff_of_μSq_nonpos {μSq : }
(hμSq : μSq ≤ 0) (φ : higgsVec) : potential μSq (λ) φ = 0 ↔ φ = 0 := by
apply Iff.intro
· intro h
exact potential_eq_zero_sol_of_μSq_nonpos μSq hLam hμSq φ h
· intro h
simp [potential, h]
(hμSq : μSq ≤ 0) (φ : higgsVec) : potential μSq (λ) φ = 0 ↔ φ = 0 :=
Iff.intro (fun h ↦ potential_eq_zero_sol_of_μSq_nonpos μSq hLam hμSq φ h) (fun h ↦ by simp [potential, h])
lemma potential_eq_bound_IsMinOn (φ : higgsVec)
(hv : potential μSq lambda φ = - μSq ^ 2 / (4 * lambda)) :
IsMinOn (potential μSq lambda) Set.univ φ := by
rw [isMinOn_univ_iff]
intro x
rw [hv]
exact potential_bounded_below μSq hLam x
rw [isMinOn_univ_iff, hv]
exact fun x ↦ potential_bounded_below μSq hLam x
lemma potential_eq_bound_IsMinOn_of_μSq_nonpos {μSq : }
(hμSq : μSq ≤ 0) (φ : higgsVec) (hv : potential μSq lambda φ = 0) :
IsMinOn (potential μSq lambda) Set.univ φ := by
rw [isMinOn_univ_iff]
intro x
rw [hv]
exact potential_bounded_below_of_μSq_nonpos hLam hμSq x
rw [isMinOn_univ_iff, hv]
exact fun x ↦ potential_bounded_below_of_μSq_nonpos hLam hμSq x
lemma potential_bound_reached_of_μSq_nonneg {μSq : } (hμSq : 0 ≤ μSq) :
∃ (φ : higgsVec), potential μSq lambda φ = - μSq ^ 2 / (4 * lambda) := by
use ![√(μSq/(2 * lambda)), 0]
refine (potential_eq_bound_iff μSq hLam _).mpr ?_
simp [@PiLp.norm_sq_eq_of_L2, Fin.sum_univ_two]
simp [PiLp.norm_sq_eq_of_L2]
field_simp [mul_pow]
lemma IsMinOn_potential_iff_of_μSq_nonneg {μSq : } (hμSq : 0 ≤ μSq) :
IsMinOn (potential μSq lambda) Set.univ φ ↔ ‖φ‖ ^ 2 = μSq /(2 * lambda) := by
apply Iff.intro
apply Iff.intro <;> rw [← potential_eq_bound_iff μSq hLam φ]
· intro h
obtain ⟨φm, hφ⟩ := potential_bound_reached_of_μSq_nonneg hLam hμSq
have hm := isMinOn_univ_iff.mp h φm
rw [hφ] at hm
have h1 := potential_bounded_below μSq hLam φ
rw [← potential_eq_bound_iff μSq hLam φ]
exact (Real.partialOrder.le_antisymm _ _ h1 hm).symm
· intro h
rw [← potential_eq_bound_iff μSq hLam φ] at h
exact potential_eq_bound_IsMinOn μSq hLam φ h
exact (Real.partialOrder.le_antisymm _ _ (potential_bounded_below μSq hLam φ) hm).symm
· exact potential_eq_bound_IsMinOn μSq hLam φ
lemma IsMinOn_potential_iff_of_μSq_nonpos {μSq : } (hμSq : μSq ≤ 0) :
IsMinOn (potential μSq lambda) Set.univ φ ↔ φ = 0 := by
apply Iff.intro
apply Iff.intro <;> rw [← potential_eq_bound_iff_of_μSq_nonpos hLam hμSq φ]
· intro h
have h0 := isMinOn_univ_iff.mp h 0
rw [(potential_eq_bound_iff_of_μSq_nonpos hLam hμSq 0).mpr (by rfl)] at h0
have h1 := potential_bounded_below_of_μSq_nonpos hLam hμSq φ
rw [(potential_eq_bound_iff_of_μSq_nonpos hLam hμSq φ)]
rw [(potential_eq_bound_iff_of_μSq_nonpos hLam hμSq 0).mpr (by rfl)] at h0
exact (Real.partialOrder.le_antisymm _ _ h1 h0).symm
· intro h
rw [← potential_eq_bound_iff_of_μSq_nonpos hLam hμSq φ] at h
exact potential_eq_bound_IsMinOn_of_μSq_nonpos hLam hμSq φ h
· exact potential_eq_bound_IsMinOn_of_μSq_nonpos hLam hμSq φ
end potentialProp
/-- Given a Higgs vector, a rotation matrix which puts the first component of the
@ -314,40 +275,30 @@ def rotateMatrix (φ : higgsVec) : Matrix (Fin 2) (Fin 2) :=
lemma rotateMatrix_star (φ : higgsVec) :
star φ.rotateMatrix =
![![conj (φ 1) /‖φ‖ , φ 0 /‖φ‖], ![- conj (φ 0) / ‖φ‖ , φ 1 / ‖φ‖] ] := by
simp [star]
rw [rotateMatrix, conjTranspose]
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
simp [rotateMatrix, det_fin_two]
have h1 : (‖φ‖ : ) ≠ 0 := ofReal_inj.mp.mt (norm_ne_zero_iff.mpr hφ)
field_simp
field_simp [rotateMatrix, det_fin_two]
rw [← ofReal_mul, ← sq, ← @real_inner_self_eq_norm_sq]
simp only [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]
rfl
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φ)
congr
field_simp
ext i j
fin_cases i <;> fin_cases j <;> field_simp
· rw [← ofReal_mul, ← sq, ← @real_inner_self_eq_norm_sq]
simp only [PiLp.inner_apply, Complex.inner, neg_mul, sub_neg_eq_add,
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,
Fin.sum_univ_two, ofReal_add, ofReal_mul, mul_conj, mul_comm, add_comm]
rfl
· ring_nf
· ring_nf
· rw [← ofReal_mul, ← sq, ← @real_inner_self_eq_norm_sq]
simp only [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]
rfl
lemma rotateMatrix_specialUnitary {φ : higgsVec} (hφ : φ ≠ 0) :
(rotateMatrix φ) ∈ specialUnitaryGroup (Fin 2) :=
@ -361,19 +312,22 @@ def rotateGuageGroup {φ : higgsVec} (hφ : φ ≠ 0) : gaugeGroup :=
lemma rotateGuageGroup_apply {φ : higgsVec} (hφ : φ ≠ 0) :
rep (rotateGuageGroup hφ) φ = ![0, ofReal ‖φ‖] := by
rw [rep_apply]
simp [rotateGuageGroup, rotateMatrix]
simp only [rotateGuageGroup, rotateMatrix, one_pow, one_smul,
Nat.succ_eq_add_one, Nat.reduceAdd, ofReal_eq_coe]
ext i
fin_cases i
simp [mulVec, vecHead, vecTail]
· simp only [mulVec, Fin.zero_eta, Fin.isValue, cons_val', empty_val', cons_val_fin_one,
cons_val_zero, cons_dotProduct, vecHead, vecTail, Nat.succ_eq_add_one, Nat.reduceAdd,
Function.comp_apply, Fin.succ_zero_eq_one, dotProduct_empty, add_zero]
ring_nf
simp only [Fin.mk_one, Fin.isValue, cons_val_one, head_cons]
simp [mulVec, vecHead, vecTail]
· 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φ)
field_simp
rw [← ofReal_mul, ← sq, ← @real_inner_self_eq_norm_sq]
simp only [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]
rfl
theorem rotate_fst_zero_snd_real (φ : higgsVec) :
∃ (g : gaugeGroup), rep g φ = ![0, ofReal ‖φ‖] := by