diff --git a/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean b/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean index c6429d7..a3432b5 100644 --- a/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean +++ b/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean @@ -18,20 +18,89 @@ namespace TwoHDM open StandardModel open ComplexConjugate +open HiggsField noncomputable section -/-- The potential of the two Higgs doublet model. -/ -def potential (Φ1 Φ2 : HiggsField) - (m11Sq m22Sq lam₁ lam₂ lam₃ lam₄ : ℝ) (m12Sq lam₅ lam₆ lam₇ : ℂ) (x : SpaceTime) : ℝ := - m11Sq * Φ1.normSq x + m22Sq * Φ2.normSq x - - (m12Sq * (Φ1.innerProd Φ2) x + conj m12Sq * (Φ2.innerProd Φ1) x).re - + 1/2 * lam₁ * Φ1.normSq x ^ 2 + 1/2 * lam₂ * Φ2.normSq x ^ 2 - + lam₃ * Φ1.normSq x * Φ2.normSq x - + lam₄ * ‖Φ1.innerProd Φ2 x‖ - + (1/2 * lam₅ * (Φ1.innerProd Φ2) x ^ 2 + 1/2 * conj lam₅ * (Φ2.innerProd Φ1) x ^ 2).re - + (lam₆ * Φ1.normSq x * (Φ1.innerProd Φ2) x + conj lam₆ * Φ1.normSq x * (Φ2.innerProd Φ1) x).re - + (lam₇ * Φ2.normSq x * (Φ1.innerProd Φ2) x + conj lam₇ * Φ2.normSq x * (Φ2.innerProd Φ1) x).re +/-- The potential of the two Higgs doublet model. -/ +def potential (Φ1 Φ2 : HiggsField) (m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ : ℝ) + (m₁₂2 𝓵₅ 𝓵₆ 𝓵₇ : ℂ) (x : SpaceTime) : ℝ := + m₁₁2 * ‖Φ1‖_H ^ 2 x + m₂₂2 * ‖Φ2‖_H ^ 2 x - (m₁₂2 * ⟪Φ1, Φ2⟫_H x + conj m₁₂2 * ⟪Φ2, Φ1⟫_H x).re + + 1/2 * 𝓵₁ * ‖Φ1‖_H ^ 2 x * ‖Φ1‖_H ^ 2 x + 1/2 * 𝓵₂ * ‖Φ2‖_H ^ 2 x * ‖Φ2‖_H ^ 2 x + + 𝓵₃ * ‖Φ1‖_H ^ 2 x * ‖Φ2‖_H ^ 2 x + + 𝓵₄ * ‖⟪Φ1, Φ2⟫_H x‖ ^ 2 + (1/2 * 𝓵₅ * ⟪Φ1, Φ2⟫_H x ^ 2 + 1/2 * conj 𝓵₅ * ⟪Φ2, Φ1⟫_H x ^ 2).re + + (𝓵₆ * ‖Φ1‖_H ^ 2 x * ⟪Φ1, Φ2⟫_H x + conj 𝓵₆ * ‖Φ1‖_H ^ 2 x * ⟪Φ2, Φ1⟫_H x).re + + (𝓵₇ * ‖Φ2‖_H ^ 2 x * ⟪Φ1, Φ2⟫_H x + conj 𝓵₇ * ‖Φ2‖_H ^ 2 x * ⟪Φ2, Φ1⟫_H x).re + +namespace potential + +variable (Φ1 Φ2 : HiggsField) +variable (m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ : ℝ) +variable (m₁₂2 𝓵₅ 𝓵₆ 𝓵₇ : ℂ) +/-! + +## Simple properties of the potential + +-/ + +/-- Swapping `Φ1` with `Φ2`, and a number of the parameters (with possible conjugation) leads + to an identical potential. -/ +lemma swap_fields : + potential Φ1 Φ2 m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ m₁₂2 𝓵₅ 𝓵₆ 𝓵₇ + = potential Φ2 Φ1 m₂₂2 m₁₁2 𝓵₂ 𝓵₁ 𝓵₃ 𝓵₄ (conj m₁₂2) (conj 𝓵₅) (conj 𝓵₇) (conj 𝓵₆) := by + funext x + simp only [potential, HiggsField.normSq, Complex.add_re, Complex.mul_re, Complex.conj_re, + Complex.conj_im, neg_mul, sub_neg_eq_add, one_div, Complex.norm_eq_abs, Complex.inv_re, + Complex.re_ofNat, Complex.normSq_ofNat, div_self_mul_self', Complex.inv_im, Complex.im_ofNat, + neg_zero, zero_div, zero_mul, sub_zero, Complex.mul_im, add_zero, mul_neg, Complex.ofReal_pow, + RingHomCompTriple.comp_apply, RingHom.id_apply] + ring_nf + simp only [one_div, add_left_inj, add_right_inj, mul_eq_mul_left_iff] + apply Or.inl + rw [HiggsField.innerProd, HiggsField.innerProd, ← InnerProductSpace.conj_symm, Complex.abs_conj] + +/-- If `Φ₂` is zero the potential reduces to the Higgs potential on `Φ₁`. -/ +lemma right_zero : potential Φ1 0 m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ m₁₂2 𝓵₅ 𝓵₆ 𝓵₇ = + StandardModel.HiggsField.potential Φ1 (- m₁₁2) (𝓵₁/2) := by + funext x + simp only [potential, normSq, ContMDiffSection.coe_zero, Pi.zero_apply, norm_zero, ne_eq, + OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, mul_zero, add_zero, innerProd_right_zero, + innerProd_left_zero, Complex.zero_re, sub_zero, one_div, Complex.ofReal_pow, + Complex.ofReal_zero, HiggsField.potential, neg_neg, add_right_inj, mul_eq_mul_right_iff, + pow_eq_zero_iff, norm_eq_zero, or_self_right] + ring_nf + simp only [true_or] + +/-- If `Φ₁` is zero the potential reduces to the Higgs potential on `Φ₂`. -/ +lemma left_zero : potential 0 Φ2 m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ m₁₂2 𝓵₅ 𝓵₆ 𝓵₇ = + StandardModel.HiggsField.potential Φ2 (- m₂₂2) (𝓵₂/2) := by + rw [swap_fields, right_zero] + +/-! + +## Potential bounded from below + +TODO: Complete this section. + +-/ + +/-! + +## Smoothness of the potential + +TODO: Complete this section. + +-/ + +/-! + +## Invariance of the potential under gauge transformations + +TODO: Complete this section. + +-/ + +end potential end end TwoHDM diff --git a/HepLean/StandardModel/HiggsBoson/Basic.lean b/HepLean/StandardModel/HiggsBoson/Basic.lean index 70f15e4..74dfc17 100644 --- a/HepLean/StandardModel/HiggsBoson/Basic.lean +++ b/HepLean/StandardModel/HiggsBoson/Basic.lean @@ -35,6 +35,11 @@ open Matrix open Complex open ComplexConjugate open SpaceTime +/-! + +## Definition of the Higgs bundle + +-/ /-- The trivial vector bundle 𝓡² × ℂ². (TODO: Make associated bundle.) -/ abbrev HiggsBundle := Bundle.Trivial SpaceTime HiggsVec @@ -60,6 +65,12 @@ noncomputable def HiggsVec.toField (φ : HiggsVec) : HiggsField where namespace HiggsField open Complex Real +/-! + +## Relation to `HiggsVec` + +-/ + /-- Given a `higgsField`, the corresponding map from `spaceTime` to `higgsVec`. -/ def toHiggsVec (φ : HiggsField) : SpaceTime → HiggsVec := φ @@ -80,6 +91,88 @@ lemma toField_toHiggsVec_apply (φ : HiggsField) (x : SpaceTime) : lemma higgsVecToFin2ℂ_toHiggsVec (φ : HiggsField) : higgsVecToFin2ℂ ∘ φ.toHiggsVec = φ := rfl +/-! + +## The inner product and norm of Higgs fields + +-/ + +/-- Given two `HiggsField`, the map `spaceTime → ℂ` obtained by taking their inner product. -/ +def innerProd (φ1 φ2 : HiggsField) : SpaceTime → ℂ := fun x => ⟪φ1 x, φ2 x⟫_ℂ + +/-- Notation for the inner product of two Higgs fields. -/ +scoped[StandardModel.HiggsField] notation "⟪" φ1 "," φ2 "⟫_H" => innerProd φ1 φ2 + +@[simp] +lemma innerProd_left_zero (φ : HiggsField) : ⟪0, φ⟫_H = 0 := by + funext x + simp [innerProd] + +@[simp] +lemma innerProd_right_zero (φ : HiggsField) : ⟪φ, 0⟫_H = 0 := by + funext x + simp [innerProd] + +lemma innerProd_expand (φ1 φ2 : HiggsField) : + ⟪φ1, φ2⟫_H = fun x => (conj (φ1 x 0) * (φ2 x 0) + conj (φ1 x 1) * (φ2 x 1) ) := by + funext x + simp only [innerProd, PiLp.inner_apply, RCLike.inner_apply, Fin.sum_univ_two] + +/-- Given a `higgsField`, the map `spaceTime → ℝ` obtained by taking the square norm of the + higgs vector. -/ +@[simp] +def normSq (φ : HiggsField) : SpaceTime → ℝ := fun x => ( ‖φ x‖ ^ 2) + +/-- Notation for the norm squared of a Higgs field. -/ +scoped[StandardModel.HiggsField] notation "‖" φ1 "‖_H ^ 2" => normSq φ1 + +lemma innerProd_self_eq_normSq (φ : HiggsField) (x : SpaceTime) : + ⟪φ, φ⟫_H x = ‖φ‖_H ^ 2 x := by + erw [normSq, @PiLp.norm_sq_eq_of_L2, Fin.sum_univ_two] + simp only [ ofReal_add, ofReal_pow, innerProd, PiLp.inner_apply, + RCLike.inner_apply, Fin.sum_univ_two, conj_mul'] + +lemma normSq_eq_innerProd_self (φ : HiggsField) (x : SpaceTime) : + ‖φ x‖ ^ 2 = (⟪φ, φ⟫_H x).re := by + rw [innerProd_self_eq_normSq] + rfl + +lemma toHiggsVec_norm (φ : HiggsField) (x : SpaceTime) : + ‖φ x‖ = ‖φ.toHiggsVec x‖ := rfl + +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 ℂ] + +lemma normSq_nonneg (φ : HiggsField) (x : SpaceTime) : 0 ≤ φ.normSq x := by + simp [normSq, ge_iff_le, norm_nonneg, pow_nonneg] + +lemma normSq_zero (φ : HiggsField) (x : SpaceTime) : φ.normSq x = 0 ↔ φ x = 0 := by + simp [normSq, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, norm_eq_zero] + +/-! + +## The Higgs potential + +-/ + +/-- The Higgs potential of the form `- μ² * |φ|² + λ * |φ|⁴`. -/ +@[simp] +def potential (φ : HiggsField) (μSq lambda : ℝ ) (x : SpaceTime) : ℝ := + - μSq * φ.normSq x + lambda * φ.normSq x * φ.normSq x + +lemma potential_apply (φ : HiggsField) (μSq lambda : ℝ) (x : SpaceTime) : + (φ.potential μSq lambda) x = HiggsVec.potential μSq lambda (φ.toHiggsVec x) := by + simp [HiggsVec.potential, toHiggsVec_norm] + ring + +/-! + +## Smoothness + +-/ + lemma toVec_smooth (φ : HiggsField) : Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, Fin 2 → ℂ) φ := smooth_higgsVecToFin2ℂ.comp φ.toHiggsVec_smooth @@ -95,22 +188,6 @@ lemma apply_im_smooth (φ : HiggsField) (i : Fin 2): Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) (imCLM ∘ (fun (x : SpaceTime) => (φ x 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⟫_ℂ - -/-- Given a `higgsField`, the map `spaceTime → ℝ` obtained by taking the square norm of the - higgs vector. -/ -@[simp] -def normSq (φ : HiggsField) : SpaceTime → ℝ := fun x => ( ‖φ x‖ ^ 2) - -lemma toHiggsVec_norm (φ : HiggsField) (x : SpaceTime) : - ‖φ x‖ = ‖φ.toHiggsVec x‖ := rfl - -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 ℂ] - lemma normSq_smooth (φ : HiggsField) : Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) φ.normSq := by rw [normSq_expand] refine Smooth.add ?_ ?_ @@ -131,27 +208,17 @@ lemma normSq_smooth (φ : HiggsField) : Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, exact φ.apply_im_smooth 1 exact φ.apply_im_smooth 1 -lemma normSq_nonneg (φ : HiggsField) (x : SpaceTime) : 0 ≤ φ.normSq x := by - simp [normSq, ge_iff_le, norm_nonneg, pow_nonneg] - -lemma normSq_zero (φ : HiggsField) (x : SpaceTime) : φ.normSq x = 0 ↔ φ x = 0 := by - 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] -def potential (φ : HiggsField) (μSq lambda : ℝ ) (x : SpaceTime) : ℝ := - - μSq * φ.normSq x + lambda * φ.normSq x * φ.normSq x - lemma potential_smooth (φ : HiggsField) (μSq lambda : ℝ) : Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) (fun x => φ.potential μSq lambda x) := by simp only [potential, normSq, neg_mul] 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 - simp [HiggsVec.potential, toHiggsVec_norm] - ring +/-! + +## Constant higgs fields + +-/ /-- A higgs field is constant if it is equal for all `x` `y` in `spaceTime`. -/ def IsConst (Φ : HiggsField) : Prop := ∀ x y, Φ x = Φ y