The pointwise inner product

We define the pointwise inner product of two Higgs fields.

The notation for the inner product is ⟪φ, ψ⟫_H.

We also define the pointwise norm squared of a Higgs field ∥φ∥_H ^ 2.

The pointwise inner product

def StandardModel.HiggsField.innerProd (φ1 φ2 : HiggsField) : SpaceTime → ℂ

Given two HiggsField, the map SpaceTime → ℂ obtained by taking their pointwise inner product.

Equations

• φ1.innerProd φ2 x = inner (φ1 x) (φ2 x)

def StandardModel.HiggsField.«term⟪_,_⟫_H» : Lean.ParserDescr

Notation for the inner product of two Higgs fields.

Equations

• One or more equations did not get rendered due to their size.

Properties of the inner product

@[simp]

theorem StandardModel.HiggsField.innerProd_neg_left (φ1 φ2 : HiggsField) : (-φ1).innerProd φ2 = -φ1.innerProd φ2

@[simp]

theorem StandardModel.HiggsField.innerProd_neg_right (φ1 φ2 : HiggsField) : φ1.innerProd (-φ2) = -φ1.innerProd φ2

@[simp]

theorem StandardModel.HiggsField.innerProd_left_zero (φ : HiggsField) : innerProd 0 φ = 0

@[simp]

theorem StandardModel.HiggsField.innerProd_right_zero (φ : HiggsField) : φ.innerProd 0 = 0

theorem StandardModel.HiggsField.innerProd_expand' (φ1 φ2 : HiggsField) (x : SpaceTime) : φ1.innerProd φ2 x = (starRingEnd ((fun (x : Fin 2) => ℂ) 0)) (φ1 x 0) * φ2 x 0 + (starRingEnd ((fun (x : Fin 2) => ℂ) 1)) (φ1 x 1) * φ2 x 1

Expands the inner product on Higgs fields in terms of complex components of the Higgs fields.

theorem StandardModel.HiggsField.innerProd_expand (φ1 φ2 : HiggsField) : φ1.innerProd φ2 = fun (x : SpaceTime) => Complex.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)

Expands the inner product on Higgs fields in terms of real components of the Higgs fields.

theorem StandardModel.HiggsField.smooth_innerProd (φ1 φ2 : HiggsField) : ContMDiff (modelWithCornersSelf ℝ SpaceTime) (modelWithCornersSelf ℝ ℂ) ⊤ (φ1.innerProd φ2)

The pointwise norm squared

def StandardModel.HiggsField.normSq (φ : HiggsField) : SpaceTime → ℝ

Given an element φ of HiggsField, normSq φ is defined as the the function SpaceTime → ℝ obtained by taking the square norm of the pointwise Higgs vector. In other words, normSq φ x = ‖φ x‖ ^ 2.

The notation ‖φ‖_H^2 is used for the normSq φ.

Equations

• φ.normSq x = ‖φ x‖ ^ 2

def StandardModel.HiggsField.«term‖_‖_H^2» : Lean.ParserDescr

Given an element φ of HiggsField, normSq φ is defined as the the function SpaceTime → ℝ obtained by taking the square norm of the pointwise Higgs vector. In other words, normSq φ x = ‖φ x‖ ^ 2.

The notation ‖φ‖_H^2 is used for the normSq φ.

Equations

• One or more equations did not get rendered due to their size.

Relation between inner prod and norm squared

@[simp]

theorem StandardModel.HiggsField.innerProd_self_eq_normSq (φ : HiggsField) (x : SpaceTime) : φ.innerProd φ x = ↑(φ.normSq x)

theorem StandardModel.HiggsField.normSq_eq_innerProd_self (φ : HiggsField) (x : SpaceTime) : ‖φ x‖ ^ 2 = (φ.innerProd φ x).re

Properties of the norm squared

theorem StandardModel.HiggsField.normSq_apply_im_zero (φ : HiggsField) (x : SpaceTime) : (Complex.ofRealHom ‖φ x‖ ^ 2).im = 0

theorem StandardModel.HiggsField.normSq_apply_re_self (φ : HiggsField) (x : SpaceTime) : (Complex.ofRealHom ‖φ x‖ ^ 2).re = φ.normSq x

theorem StandardModel.HiggsField.toHiggsVec_norm (φ : HiggsField) (x : SpaceTime) : ‖φ x‖ = ‖φ.toHiggsVec x‖

theorem StandardModel.HiggsField.normSq_expand (φ : HiggsField) : φ.normSq = fun (x : SpaceTime) => ((starRingEnd ((fun (x : Fin 2) => ℂ) 0)) (φ x 0) * φ x 0 + (starRingEnd ((fun (x : Fin 2) => ℂ) 1)) (φ x 1) * φ x 1).re

The expansion of the norm squared of into components.

theorem StandardModel.HiggsField.normSq_nonneg (φ : HiggsField) (x : SpaceTime) : 0 ≤ φ.normSq x

The norm squared of a higgs field at any point is non-negative.

theorem StandardModel.HiggsField.normSq_zero (φ : HiggsField) (x : SpaceTime) : φ.normSq x = 0 ↔ φ x = 0

If the norm square of a Higgs field at a point x is zero, then the Higgs field at that point is zero.

theorem StandardModel.HiggsField.normSq_smooth (φ : HiggsField) : ContMDiff (modelWithCornersSelf ℝ SpaceTime) (modelWithCornersSelf ℝ ℝ) ⊤ φ.normSq

The norm squared of the Higgs field is a smooth function on space-time.

theorem StandardModel.HiggsField.ofReal_normSq {a : ℝ} (ha : 0 ≤ a) (x : SpaceTime) : (ofReal a).normSq x = a

The norm-squared of the Higgs field HiggsField.ofReal a for a non-negative real number a, is equal to a.