Basic properties of normal ordering

Properties of normal ordering.

theorem FieldSpecification.FieldOpAlgebra.normalOrder_eq_ι_normalOrderF {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) : normalOrder (ι a) = ι (FieldOpFreeAlgebra.normalOrderF a)

theorem FieldSpecification.FieldOpAlgebra.normalOrder_ofCrAnList {𝓕 : FieldSpecification} (φs : List 𝓕.CrAnFieldOp) : normalOrder (ofCrAnList φs) = normalOrderSign φs • ofCrAnList (normalOrderList φs)

@[simp]

theorem FieldSpecification.FieldOpAlgebra.normalOrder_one_eq_one {𝓕 : FieldSpecification} : normalOrder 1 = 1

@[simp]

theorem FieldSpecification.FieldOpAlgebra.normalOrder_ofFieldOpList_nil {𝓕 : FieldSpecification} : normalOrder (ofFieldOpList []) = 1

@[simp]

theorem FieldSpecification.FieldOpAlgebra.normalOrder_ofCrAnList_nil {𝓕 : FieldSpecification} : normalOrder (ofCrAnList []) = 1

theorem FieldSpecification.FieldOpAlgebra.ofCrAnList_eq_normalOrder {𝓕 : FieldSpecification} (φs : List 𝓕.CrAnFieldOp) : ofCrAnList (normalOrderList φs) = normalOrderSign φs • normalOrder (ofCrAnList φs)

theorem FieldSpecification.FieldOpAlgebra.normalOrder_normalOrder_mid {𝓕 : FieldSpecification} (a b c : 𝓕.FieldOpAlgebra) : normalOrder (a * b * c) = normalOrder (a * normalOrder b * c)

theorem FieldSpecification.FieldOpAlgebra.normalOrder_normalOrder_left {𝓕 : FieldSpecification} (a b : 𝓕.FieldOpAlgebra) : normalOrder (a * b) = normalOrder (normalOrder a * b)

theorem FieldSpecification.FieldOpAlgebra.normalOrder_normalOrder_right {𝓕 : FieldSpecification} (a b : 𝓕.FieldOpAlgebra) : normalOrder (a * b) = normalOrder (a * normalOrder b)

theorem FieldSpecification.FieldOpAlgebra.normalOrder_normalOrder {𝓕 : FieldSpecification} (a : 𝓕.FieldOpAlgebra) : normalOrder (normalOrder a) = normalOrder a

mul anpart and crpart

theorem FieldSpecification.FieldOpAlgebra.normalOrder_mul_anPart {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (a : 𝓕.FieldOpAlgebra) : normalOrder (a * anPart φ) = normalOrder a * anPart φ

theorem FieldSpecification.FieldOpAlgebra.crPart_mul_normalOrder {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (a : 𝓕.FieldOpAlgebra) : normalOrder (crPart φ * a) = crPart φ * normalOrder a

Normal order and super commutes

@[simp]

theorem FieldSpecification.FieldOpAlgebra.normalOrder_superCommute_eq_zero {𝓕 : FieldSpecification} (a b : 𝓕.FieldOpAlgebra) : normalOrder ((superCommute a) b) = 0

For a field specification 𝓕, and a and b in 𝓕.FieldOpAlgebra the normal ordering of the super commutator of a and b vanishes, i.e. 𝓝([a,b]ₛ) = 0.

@[simp]

theorem FieldSpecification.FieldOpAlgebra.normalOrder_superCommute_left_eq_zero {𝓕 : FieldSpecification} (a b c : 𝓕.FieldOpAlgebra) : normalOrder ((superCommute a) b * c) = 0

@[simp]

theorem FieldSpecification.FieldOpAlgebra.normalOrder_superCommute_right_eq_zero {𝓕 : FieldSpecification} (a b c : 𝓕.FieldOpAlgebra) : normalOrder (c * (superCommute a) b) = 0

@[simp]

theorem FieldSpecification.FieldOpAlgebra.normalOrder_superCommute_mid_eq_zero {𝓕 : FieldSpecification} (a b c d : 𝓕.FieldOpAlgebra) : normalOrder (a * (superCommute c) d * b) = 0

Swapping terms in a normal order.

theorem FieldSpecification.FieldOpAlgebra.normalOrder_ofFieldOp_ofFieldOp_swap {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : normalOrder (ofFieldOp φ * ofFieldOp φ') = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φ') • normalOrder (ofFieldOp φ' * ofFieldOp φ)

theorem FieldSpecification.FieldOpAlgebra.normalOrder_ofCrAnOp_ofCrAnList {𝓕 : FieldSpecification} (φ : 𝓕.CrAnFieldOp) (φs : List 𝓕.CrAnFieldOp) : normalOrder (ofCrAnOp φ * ofCrAnList φs) = (FieldStatistic.exchangeSign (𝓕.crAnStatistics φ)) (FieldStatistic.ofList 𝓕.crAnStatistics φs) • normalOrder (ofCrAnList φs * ofCrAnOp φ)

theorem FieldSpecification.FieldOpAlgebra.normalOrder_ofCrAnOp_ofFieldOpList_swap {𝓕 : FieldSpecification} (φ : 𝓕.CrAnFieldOp) (φ' : List 𝓕.FieldOp) : normalOrder (ofCrAnOp φ * ofFieldOpList φ') = (FieldStatistic.exchangeSign (𝓕.crAnStatistics φ)) (FieldStatistic.ofList 𝓕.fieldOpStatistic φ') • normalOrder (ofFieldOpList φ' * ofCrAnOp φ)

theorem FieldSpecification.FieldOpAlgebra.normalOrder_anPart_ofFieldOpList_swap {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φ' : List 𝓕.FieldOp) : normalOrder (anPart φ * ofFieldOpList φ') = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofList 𝓕.fieldOpStatistic φ') • normalOrder (ofFieldOpList φ' * anPart φ)

theorem FieldSpecification.FieldOpAlgebra.normalOrder_ofFieldOpList_anPart_swap {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φ' : List 𝓕.FieldOp) : normalOrder (ofFieldOpList φ' * anPart φ) = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofList 𝓕.fieldOpStatistic φ') • normalOrder (anPart φ * ofFieldOpList φ')

theorem FieldSpecification.FieldOpAlgebra.normalOrder_ofFieldOpList_mul_anPart_swap {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : normalOrder (ofFieldOpList φs) * anPart φ = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofList 𝓕.fieldOpStatistic φs) • normalOrder (anPart φ * ofFieldOpList φs)

theorem FieldSpecification.FieldOpAlgebra.anPart_mul_normalOrder_ofFieldOpList_eq_superCommute {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs' : List 𝓕.FieldOp) : anPart φ * normalOrder (ofFieldOpList φs') = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofList 𝓕.fieldOpStatistic φs') • normalOrder (ofFieldOpList φs' * anPart φ) + (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs'))

Super commutators with a normal ordered term as sums

theorem FieldSpecification.FieldOpAlgebra.ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum {𝓕 : FieldSpecification} (φ : 𝓕.CrAnFieldOp) (φs : List 𝓕.CrAnFieldOp) : (superCommute (ofCrAnOp φ)) (normalOrder (ofCrAnList φs)) = ∑ n : Fin φs.length, (FieldStatistic.exchangeSign (𝓕.crAnStatistics φ)) (FieldStatistic.ofList 𝓕.crAnStatistics (List.take (↑n) φs)) • (superCommute (ofCrAnOp φ)) (ofCrAnOp φs[n]) * normalOrder (ofCrAnList (φs.eraseIdx ↑n))

For a field specification 𝓕, an element φ of 𝓕.CrAnFieldOp, a list φs of 𝓕.CrAnFieldOp, the following relation holds

[φ, 𝓝(φ₀…φₙ)]ₛ = ∑ i, 𝓢(φ, φ₀…φᵢ₋₁) • [φ, φᵢ]ₛ * 𝓝(φ₀…φᵢ₋₁φᵢ₊₁…φₙ).

The proof of this result ultimately goes as follows

• The definition of normalOrder is used to rewrite 𝓝(φ₀…φₙ) as a scalar multiple of a ofCrAnList φsn where φsn is the normal ordering of φ₀…φₙ.
• superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum is used to rewrite the super commutator of φ (considered as a list with one element) with ofCrAnList φsn as a sum of super commutators, one for each element of φsn.
• The fact that super-commutators are in the center of 𝓕.FieldOpAlgebra is used to rearrange terms.
• Properties of ordered lists, and normalOrderSign_eraseIdx are then used to complete the proof.

theorem FieldSpecification.FieldOpAlgebra.ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum {𝓕 : FieldSpecification} (φ : 𝓕.CrAnFieldOp) (φs : List 𝓕.FieldOp) : (superCommute (ofCrAnOp φ)) (normalOrder (ofFieldOpList φs)) = ∑ n : Fin φs.length, (FieldStatistic.exchangeSign (𝓕.crAnStatistics φ)) (FieldStatistic.ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) • (superCommute (ofCrAnOp φ)) (ofFieldOp φs[n]) * normalOrder (ofFieldOpList (φs.eraseIdx ↑n))

theorem FieldSpecification.FieldOpAlgebra.anPart_superCommute_normalOrder_ofFieldOpList_sum {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs)) = ∑ n : Fin φs.length, (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) • (superCommute (anPart φ)) ↑(FieldOpFreeAlgebra.ofFieldOpF φs[n]) * normalOrder (ofFieldOpList (φs.eraseIdx ↑n))

The commutator of the annihilation part of a field operator with a normal ordered list of field operators can be decomposed into the sum of the commutators of the annihilation part with each element of the list of field operators, i.e. [anPart φ, 𝓝(φ₀…φₙ)]ₛ= ∑ i, 𝓢(φ, φ₀…φᵢ₋₁) • [anPart φ, φᵢ]ₛ * 𝓝(φ₀…φᵢ₋₁φᵢ₊₁…φₙ).

Multiplying with normal ordered terms

theorem FieldSpecification.FieldOpAlgebra.anPart_mul_normalOrder_ofFieldOpList_eq_superCommute_reorder {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : anPart φ * normalOrder (ofFieldOpList φs) = normalOrder (anPart φ * ofFieldOpList φs) + (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs))

Within a proto-operator algebra we have that anPartF φ * 𝓝(φ₀φ₁…φₙ) = 𝓝((anPart φ)φ₀φ₁…φₙ) + [anpart φ, 𝓝(φ₀φ₁…φₙ)]ₛ.

theorem FieldSpecification.FieldOpAlgebra.ofFieldOp_mul_normalOrder_ofFieldOpList_eq_superCommute {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : ofFieldOp φ * normalOrder (ofFieldOpList φs) = normalOrder (ofFieldOp φ * ofFieldOpList φs) + (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs))

Within a proto-operator algebra we have that φ * 𝓝ᶠ(φ₀φ₁…φₙ) = 𝓝ᶠ(φφ₀φ₁…φₙ) + [anpart φ, 𝓝ᶠ(φ₀φ₁…φₙ)]ₛF.

noncomputable def FieldSpecification.FieldOpAlgebra.contractStateAtIndex {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (n : Option (Fin φs.length)) : 𝓕.FieldOpAlgebra

In the expansion of ofFieldOpF φ * normalOrderF (ofFieldOpListF φs) the element of 𝓞.A associated with contracting φ with the (optional) nth element of φs.

Equations

• One or more equations did not get rendered due to their size.
• FieldSpecification.FieldOpAlgebra.contractStateAtIndex φ φs none = 1

theorem FieldSpecification.FieldOpAlgebra.ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) : ofFieldOp φ * normalOrder (ofFieldOpList φs) = ∑ n : Option (Fin φs.length), contractStateAtIndex φ φs n * normalOrder (ofFieldOpList (PhysLean.List.optionEraseZ φs φ n))

For a field specification 𝓕, a φ in 𝓕.FieldOp and a list φs of 𝓕.FieldOp then φ * 𝓝(φ₀φ₁…φₙ) is equal to

𝓝(φφ₀φ₁…φₙ) + ∑ i, (𝓢(φ,φ₀φ₁…φᵢ₋₁) • [anPart φ, φᵢ]ₛ) * 𝓝(φ₀…φᵢ₋₁φᵢ₊₁…φₙ).

The proof ultimately goes as follows:

• ofFieldOp_eq_crPart_add_anPart is used to split φ into its creation and annihilation parts.

• The following relation is then used

  crPart φ * 𝓝(φ₀φ₁…φₙ) = 𝓝(crPart φ * φ₀φ₁…φₙ).

• It used that anPart φ * 𝓝(φ₀φ₁…φₙ) is equal to

  𝓢(φ, φ₀φ₁…φₙ) 𝓝(φ₀φ₁…φₙ) * anPart φ + [anPart φ, 𝓝(φ₀φ₁…φₙ)]

• Then it is used that

  𝓢(φ, φ₀φ₁…φₙ) 𝓝(φ₀φ₁…φₙ) * anPart φ = 𝓝(anPart φ * φ₀φ₁…φₙ)

• The result ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum is used to expand [anPart φ, 𝓝(φ₀φ₁…φₙ)] as a sum.

Cons vs insertIdx for a normal ordered term.

theorem FieldSpecification.FieldOpAlgebra.ofFieldOpList_normalOrder_insert {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (k : Fin φs.length.succ) : normalOrder (ofFieldOpList (φ :: φs)) = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofList 𝓕.fieldOpStatistic (List.take (↑k) φs)) • normalOrder (ofFieldOpList (List.insertIdx (↑k) φ φs))

Within a proto-operator algebra, N(φφ₀φ₁…φₙ) = s • N(φ₀…φₖ₋₁φφₖ…φₙ), where s is the exchange sign for φ and φ₀…φₖ₋₁.

The normal ordering of a product of two states

@[simp]

theorem FieldSpecification.FieldOpAlgebra.normalOrder_crPart_mul_crPart {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : normalOrder (crPart φ * crPart φ') = crPart φ * crPart φ'

@[simp]

theorem FieldSpecification.FieldOpAlgebra.normalOrder_anPart_mul_anPart {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : normalOrder (anPart φ * anPart φ') = anPart φ * anPart φ'

@[simp]

theorem FieldSpecification.FieldOpAlgebra.normalOrder_crPart_mul_anPart {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : normalOrder (crPart φ * anPart φ') = crPart φ * anPart φ'

@[simp]

theorem FieldSpecification.FieldOpAlgebra.normalOrder_anPart_mul_crPart {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : normalOrder (anPart φ * crPart φ') = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φ') • crPart φ' * anPart φ

theorem FieldSpecification.FieldOpAlgebra.normalOrder_ofFieldOp_mul_ofFieldOp {𝓕 : FieldSpecification} (φ φ' : 𝓕.FieldOp) : normalOrder (ofFieldOp φ * ofFieldOp φ') = crPart φ * crPart φ' + (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (𝓕.fieldOpStatistic φ') • (crPart φ' * anPart φ) + crPart φ * anPart φ' + anPart φ * anPart φ'