Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.QFT.PerturbationTheory.FieldSpecification.NormalOrder public import Physlib.QFT.PerturbationTheory.FieldOpFreeAlgebra.SuperCommute

Normal Ordering in the FieldOpFreeAlgebra

In the module Physlib.QFT.PerturbationTheory.FieldSpecification.NormalOrder we defined the normal ordering of a list of CrAnFieldOp. In this module we extend the normal ordering to a linear map on FieldOpFreeAlgebra.

We derive properties of this normal ordering.

@[expose] public section

For a field specification 𝓕, normalOrderF is the linear map

FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpFreeAlgebra 𝓕

defined by its action on the basis ofCrAnListF φs, taking ofCrAnListF φs to

normalOrderSign φs • ofCrAnListF (normalOrderList φs).

That is, normalOrderF normal-orders the field operators and multiplies by the sign of the normal order.

The notation 𝓝ᶠ(a) is used for normalOrderF a for a an element of FieldOpFreeAlgebra 𝓕.

def normalOrderF : FieldOpFreeAlgebra 𝓕 →ₗ[] FieldOpFreeAlgebra 𝓕 := Basis.constr ofCrAnListFBasis fun φs => normalOrderSign φs ofCrAnListF (normalOrderList φs)
@[inherit_doc normalOrderF] scoped[FieldSpecification.FieldOpFreeAlgebra] notation "𝓝ᶠ(" a ")" => normalOrderF aAll goals completed! 🐙All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun c hc => normalOrderF (a * b * c) = normalOrderF (a * normalOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun b hb => normalOrderF (a * b * ofCrAnListF φs) = normalOrderF (a * normalOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun a ha => normalOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = normalOrderF (a * normalOrderF (ofCrAnListF φs') * ofCrAnListF φs)pa 0 All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun c hc => normalOrderF (a * b * c) = normalOrderF (a * normalOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun b hb => normalOrderF (a * b * ofCrAnListF φs) = normalOrderF (a * normalOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun a ha => normalOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = normalOrderF (a * normalOrderF (ofCrAnListF φs') * ofCrAnListF φs) (x y : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span (Set.range ofCrAnListFBasis)) (hy : y Submodule.span (Set.range ofCrAnListFBasis)), pa x hx pa y hy pa (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun c hc => normalOrderF (a * b * c) = normalOrderF (a * normalOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun b hb => normalOrderF (a * b * ofCrAnListF φs) = normalOrderF (a * normalOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun a ha => normalOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = normalOrderF (a * normalOrderF (ofCrAnListF φs') * ofCrAnListF φs)x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span (Set.range ofCrAnListFBasis)hy:y Submodule.span (Set.range ofCrAnListFBasis)h1:pa x hxh2:pa y hypa (x + y) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun c hc => normalOrderF (a * b * c) = normalOrderF (a * normalOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun b hb => normalOrderF (a * b * ofCrAnListF φs) = normalOrderF (a * normalOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun a ha => normalOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = normalOrderF (a * normalOrderF (ofCrAnListF φs') * ofCrAnListF φs) (a : ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span (Set.range ofCrAnListFBasis)), pa x hx pa (a x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun c hc => normalOrderF (a * b * c) = normalOrderF (a * normalOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun b hb => normalOrderF (a * b * ofCrAnListF φs) = normalOrderF (a * normalOrderF b * ofCrAnListF φs)φs':List 𝓕.CrAnFieldOppa:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun a ha => normalOrderF (a * ofCrAnListF φs' * ofCrAnListF φs) = normalOrderF (a * normalOrderF (ofCrAnListF φs') * ofCrAnListF φs)x:hx:𝓕.FieldOpFreeAlgebrah:hx Submodule.span (Set.range ofCrAnListFBasis)pa hx h pa (x hx) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun c hc => normalOrderF (a * b * c) = normalOrderF (a * normalOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun b hb => normalOrderF (a * b * ofCrAnListF φs) = normalOrderF (a * normalOrderF b * ofCrAnListF φs)pb 0 All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun c hc => normalOrderF (a * b * c) = normalOrderF (a * normalOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun b hb => normalOrderF (a * b * ofCrAnListF φs) = normalOrderF (a * normalOrderF b * ofCrAnListF φs) (x y : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span (Set.range ofCrAnListFBasis)) (hy : y Submodule.span (Set.range ofCrAnListFBasis)), pb x hx pb y hy pb (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun c hc => normalOrderF (a * b * c) = normalOrderF (a * normalOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun b hb => normalOrderF (a * b * ofCrAnListF φs) = normalOrderF (a * normalOrderF b * ofCrAnListF φs)x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span (Set.range ofCrAnListFBasis)hy:y Submodule.span (Set.range ofCrAnListFBasis)h1:pb x hxh2:pb y hypb (x + y) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun c hc => normalOrderF (a * b * c) = normalOrderF (a * normalOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun b hb => normalOrderF (a * b * ofCrAnListF φs) = normalOrderF (a * normalOrderF b * ofCrAnListF φs) (a : ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span (Set.range ofCrAnListFBasis)), pb x hx pb (a x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun c hc => normalOrderF (a * b * c) = normalOrderF (a * normalOrderF b * c)φs:List 𝓕.CrAnFieldOppb:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun b hb => normalOrderF (a * b * ofCrAnListF φs) = normalOrderF (a * normalOrderF b * ofCrAnListF φs)x:hx:𝓕.FieldOpFreeAlgebrah:hx Submodule.span (Set.range ofCrAnListFBasis)pb hx h pb (x hx) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun c hc => normalOrderF (a * b * c) = normalOrderF (a * normalOrderF b * c)pc 0 All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun c hc => normalOrderF (a * b * c) = normalOrderF (a * normalOrderF b * c) (x y : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span (Set.range ofCrAnListFBasis)) (hy : y Submodule.span (Set.range ofCrAnListFBasis)), pc x hx pc y hy pc (x + y) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun c hc => normalOrderF (a * b * c) = normalOrderF (a * normalOrderF b * c)x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebrahx:x Submodule.span (Set.range ofCrAnListFBasis)hy:y Submodule.span (Set.range ofCrAnListFBasis)h1:pc x hxh2:pc y hypc (x + y) All goals completed! 🐙 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun c hc => normalOrderF (a * b * c) = normalOrderF (a * normalOrderF b * c) (a : ) (x : 𝓕.FieldOpFreeAlgebra) (hx : x Submodule.span (Set.range ofCrAnListFBasis)), pc x hx pc (a x) 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrapc:(c : 𝓕.FieldOpFreeAlgebra) c Submodule.span (Set.range ofCrAnListFBasis) Prop := fun c hc => normalOrderF (a * b * c) = normalOrderF (a * normalOrderF b * c)x:hx:𝓕.FieldOpFreeAlgebrah:hx Submodule.span (Set.range ofCrAnListFBasis)hp:pc hx hpc (x hx) All goals completed! 🐙lemma normalOrderF_normalOrderF_right (a b : 𝓕.FieldOpFreeAlgebra) : 𝓝ᶠ(a * b) = 𝓝ᶠ(a * 𝓝ᶠ(b)) := 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebranormalOrderF (a * b) = normalOrderF (a * normalOrderF b) All goals completed! 🐙lemma normalOrderF_normalOrderF_left (a b : 𝓕.FieldOpFreeAlgebra) : 𝓝ᶠ(a * b) = 𝓝ᶠ(𝓝ᶠ(a) * b) := 𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebranormalOrderF (a * b) = normalOrderF (normalOrderF a * b) All goals completed! 🐙

Normal ordering with a creation operator on the left or annihilation on the right

All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙lemma normalOrderF_crPartF_mul (φ : 𝓕.FieldOp) (a : FieldOpFreeAlgebra 𝓕) : 𝓝ᶠ(crPartF φ * a) = crPartF φ * 𝓝ᶠ(a) := 𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebranormalOrderF (crPartF φ * a) = crPartF φ * normalOrderF a match φ with 𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebraa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimenormalOrderF (crPartF (FieldOp.position a✝) * a) = crPartF (FieldOp.position a✝) * normalOrderF a𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebraa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × MomentumnormalOrderF (crPartF (FieldOp.inAsymp a✝) * a) = crPartF (FieldOp.inAsymp a✝) * normalOrderF a All goals completed! 🐙 𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebraa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × MomentumnormalOrderF (crPartF (FieldOp.outAsymp a✝) * a) = crPartF (FieldOp.outAsymp a✝) * normalOrderF a All goals completed! 🐙lemma normalOrderF_mul_anPartF (φ : 𝓕.FieldOp) (a : FieldOpFreeAlgebra 𝓕) : 𝓝ᶠ(a * anPartF φ) = 𝓝ᶠ(a) * anPartF φ := 𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebranormalOrderF (a * anPartF φ) = normalOrderF a * anPartF φ match φ with 𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebraa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × MomentumnormalOrderF (a * anPartF (FieldOp.inAsymp a✝)) = normalOrderF a * anPartF (FieldOp.inAsymp a✝) All goals completed! 🐙 𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebraa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × MomentumnormalOrderF (a * anPartF (FieldOp.outAsymp a✝)) = normalOrderF a * anPartF (FieldOp.outAsymp a✝)𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebraa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimenormalOrderF (a * anPartF (FieldOp.position a✝)) = normalOrderF a * anPartF (FieldOp.position a✝) All goals completed! 🐙

Normal ordering for an adjacent creation and annihilation state

The main result of this section is normalOrderF_superCommuteF_annihilate_create.

𝓕:FieldSpecificationφc:𝓕.CrAnFieldOpφa:𝓕.CrAnFieldOphφc:𝓕|>ᶜφc = CreateAnnihilate.createhφa:𝓕|>ᶜφa = CreateAnnihilate.annihilateφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp(exchangeSign (𝓕.crAnStatistics φc)) (𝓕.crAnStatistics φa) normalOrderF (ofCrAnListF φs' * (ofCrAnOpF φa * (ofCrAnOpF φc * ofCrAnListF φs))) = (exchangeSign (𝓕.crAnStatistics φc)) (𝓕.crAnStatistics φa) normalOrderF (ofCrAnListF φs' * ofCrAnOpF φa * ofCrAnOpF φc * ofCrAnListF φs) All goals completed! 🐙𝓕:FieldSpecificationφc:𝓕.CrAnFieldOpφa:𝓕.CrAnFieldOphφc:𝓕|>ᶜφc = CreateAnnihilate.createhφa:𝓕|>ᶜφa = CreateAnnihilate.annihilateφs:List 𝓕.CrAnFieldOpa:𝓕.FieldOpFreeAlgebral:List 𝓕.CrAnFieldOp(exchangeSign (𝓕.crAnStatistics φc)) (𝓕.crAnStatistics φa) normalOrderF (ofCrAnListF φs * ofCrAnOpF φa * ofCrAnOpF φc * ofCrAnListF l) = (smulLinearMap ((exchangeSign (𝓕.crAnStatistics φc)) (𝓕.crAnStatistics φa))) (normalOrderF (ofCrAnListF φs * ofCrAnOpF φa * ofCrAnOpF φc * ofCrAnListF l)) All goals completed! 🐙𝓕:FieldSpecificationφc:𝓕.CrAnFieldOpφa:𝓕.CrAnFieldOphφc:𝓕|>ᶜφc = CreateAnnihilate.createhφa:𝓕|>ᶜφa = CreateAnnihilate.annihilatea:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebranormalOrderF (a * (ofCrAnOpF φc * (ofCrAnOpF φa * b))) = (exchangeSign (𝓕.crAnStatistics φc)) (𝓕.crAnStatistics φa) normalOrderF (a * (ofCrAnOpF φa * (ofCrAnOpF φc * b))) 𝓕:FieldSpecificationφc:𝓕.CrAnFieldOpφa:𝓕.CrAnFieldOphφc:𝓕|>ᶜφc = CreateAnnihilate.createhφa:𝓕|>ᶜφa = CreateAnnihilate.annihilatea:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra(normalOrderF ∘ₗ mulLinearMap.flip (ofCrAnOpF φc * (ofCrAnOpF φa * b))) a = (smulLinearMap ((exchangeSign (𝓕.crAnStatistics φc)) (𝓕.crAnStatistics φa)) ∘ₗ normalOrderF ∘ₗ mulLinearMap.flip (ofCrAnOpF φa * (ofCrAnOpF φc * b))) a 𝓕:FieldSpecificationφc:𝓕.CrAnFieldOpφa:𝓕.CrAnFieldOphφc:𝓕|>ᶜφc = CreateAnnihilate.createhφa:𝓕|>ᶜφa = CreateAnnihilate.annihilatea:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebral:List 𝓕.CrAnFieldOp(normalOrderF ∘ₗ mulLinearMap.flip (ofCrAnOpF φc * (ofCrAnOpF φa * b))) (ofCrAnListFBasis l) = (smulLinearMap ((exchangeSign (𝓕.crAnStatistics φc)) (𝓕.crAnStatistics φa)) ∘ₗ normalOrderF ∘ₗ mulLinearMap.flip (ofCrAnOpF φa * (ofCrAnOpF φc * b))) (ofCrAnListFBasis l) 𝓕:FieldSpecificationφc:𝓕.CrAnFieldOpφa:𝓕.CrAnFieldOphφc:𝓕|>ᶜφc = CreateAnnihilate.createhφa:𝓕|>ᶜφa = CreateAnnihilate.annihilatea:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebral:List 𝓕.CrAnFieldOp(exchangeSign (𝓕.crAnStatistics φc)) (𝓕.crAnStatistics φa) normalOrderF (ofCrAnListF l * ofCrAnOpF φa * ofCrAnOpF φc * b) = (smulLinearMap ((exchangeSign (𝓕.crAnStatistics φc)) (𝓕.crAnStatistics φa))) (normalOrderF (ofCrAnListF l * ofCrAnOpF φa * ofCrAnOpF φc * b)) All goals completed! 🐙𝓕:FieldSpecificationφc:𝓕.CrAnFieldOpφa:𝓕.CrAnFieldOphφc:𝓕|>ᶜφc = CreateAnnihilate.createhφa:𝓕|>ᶜφa = CreateAnnihilate.annihilatea:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra(exchangeSign (𝓕.crAnStatistics φc)) (𝓕.crAnStatistics φa) normalOrderF (a * ofCrAnOpF φa * ofCrAnOpF φc * b) - normalOrderF (a * (exchangeSign (𝓕.crAnStatistics φc)) (𝓕.crAnStatistics φa) ofCrAnOpF φa * ofCrAnOpF φc * b) = 0 All goals completed! 🐙𝓕:FieldSpecificationφc:𝓕.CrAnFieldOpφa:𝓕.CrAnFieldOphφc:𝓕|>ᶜφc = CreateAnnihilate.createhφa:𝓕|>ᶜφa = CreateAnnihilate.annihilatea:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebranormalOrderF (a * -(exchangeSign (𝓕.crAnStatistics φa)) (𝓕.crAnStatistics φc) (superCommuteF (ofCrAnOpF φc)) (ofCrAnOpF φa) * b) = 0 All goals completed! 🐙lemma normalOrderF_swap_crPartF_anPartF (φ φ' : 𝓕.FieldOp) (a b : FieldOpFreeAlgebra 𝓕) : 𝓝ᶠ(a * (crPartF φ) * (anPartF φ') * b) = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') 𝓝ᶠ(a * (anPartF φ') * (crPartF φ) * b) := 𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebranormalOrderF (a * crPartF φ * anPartF φ' * b) = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') normalOrderF (a * anPartF φ' * crPartF φ * b) match φ, φ' with 𝓕:FieldSpecificationφ:𝓕.FieldOpφ'✝:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrax✝:𝓕.FieldOpφ':((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × MomentumnormalOrderF (a * crPartF x✝ * anPartF (FieldOp.inAsymp φ') * b) = (exchangeSign (𝓕|>ₛx✝)) (𝓕|>ₛFieldOp.inAsymp φ') normalOrderF (a * anPartF (FieldOp.inAsymp φ') * crPartF x✝ * b) All goals completed! 🐙 𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ':𝓕.FieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumx✝:𝓕.FieldOpnormalOrderF (a * crPartF (FieldOp.outAsymp φ) * anPartF x✝ * b) = (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (𝓕|>ₛx✝) normalOrderF (a * anPartF x✝ * crPartF (FieldOp.outAsymp φ) * b) All goals completed! 🐙 𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraa✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × MomentumnormalOrderF (a * crPartF (FieldOp.position a✝¹) * anPartF (FieldOp.outAsymp a✝) * b) = (exchangeSign (𝓕|>ₛFieldOp.position a✝¹)) (𝓕|>ₛFieldOp.outAsymp a✝) normalOrderF (a * anPartF (FieldOp.outAsymp a✝) * crPartF (FieldOp.position a✝¹) * b)𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraa✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimenormalOrderF (a * crPartF (FieldOp.position a✝¹) * anPartF (FieldOp.position a✝) * b) = (exchangeSign (𝓕|>ₛFieldOp.position a✝¹)) (𝓕|>ₛFieldOp.position a✝) normalOrderF (a * anPartF (FieldOp.position a✝) * crPartF (FieldOp.position a✝¹) * b)𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × MomentumnormalOrderF (a * crPartF (FieldOp.inAsymp a✝¹) * anPartF (FieldOp.outAsymp a✝) * b) = (exchangeSign (𝓕|>ₛFieldOp.inAsymp a✝¹)) (𝓕|>ₛFieldOp.outAsymp a✝) normalOrderF (a * anPartF (FieldOp.outAsymp a✝) * crPartF (FieldOp.inAsymp a✝¹) * b)𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimenormalOrderF (a * crPartF (FieldOp.inAsymp a✝¹) * anPartF (FieldOp.position a✝) * b) = (exchangeSign (𝓕|>ₛFieldOp.inAsymp a✝¹)) (𝓕|>ₛFieldOp.position a✝) normalOrderF (a * anPartF (FieldOp.position a✝) * crPartF (FieldOp.inAsymp a✝¹) * b) All goals completed! 🐙

Normal ordering for an anPartF and crPartF

Using the results from above.

lemma normalOrderF_swap_anPartF_crPartF (φ φ' : 𝓕.FieldOp) (a b : FieldOpFreeAlgebra 𝓕) : 𝓝ᶠ(a * (anPartF φ) * (crPartF φ') * b) = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') 𝓝ᶠ(a * (crPartF φ') * (anPartF φ) * b) := 𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebranormalOrderF (a * anPartF φ * crPartF φ' * b) = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') normalOrderF (a * crPartF φ' * anPartF φ * b) All goals completed! 🐙lemma normalOrderF_superCommuteF_crPartF_anPartF (φ φ' : 𝓕.FieldOp) (a b : FieldOpFreeAlgebra 𝓕) : 𝓝ᶠ(a * superCommuteF (crPartF φ) (anPartF φ') * b) = 0 := 𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebranormalOrderF (a * (superCommuteF (crPartF φ)) (anPartF φ') * b) = 0 match φ, φ' with 𝓕:FieldSpecificationφ:𝓕.FieldOpφ'✝:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrax✝:𝓕.FieldOpφ':((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × MomentumnormalOrderF (a * (superCommuteF (crPartF x✝)) (anPartF (FieldOp.inAsymp φ')) * b) = 0 All goals completed! 🐙 𝓕:FieldSpecificationφ:𝓕.FieldOpφ'✝:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraφ':((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumx✝:𝓕.FieldOpnormalOrderF (a * (superCommuteF (crPartF (FieldOp.outAsymp φ'))) (anPartF x✝) * b) = 0 All goals completed! 🐙 𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraa✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × MomentumnormalOrderF (a * (superCommuteF (crPartF (FieldOp.position a✝¹))) (anPartF (FieldOp.outAsymp a✝)) * b) = 0𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraa✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimenormalOrderF (a * (superCommuteF (crPartF (FieldOp.position a✝¹))) (anPartF (FieldOp.position a✝)) * b) = 0𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × MomentumnormalOrderF (a * (superCommuteF (crPartF (FieldOp.inAsymp a✝¹))) (anPartF (FieldOp.outAsymp a✝)) * b) = 0𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimenormalOrderF (a * (superCommuteF (crPartF (FieldOp.inAsymp a✝¹))) (anPartF (FieldOp.position a✝)) * b) = 0 All goals completed! 🐙lemma normalOrderF_superCommuteF_anPartF_crPartF (φ φ' : 𝓕.FieldOp) (a b : FieldOpFreeAlgebra 𝓕) : 𝓝ᶠ(a * superCommuteF (anPartF φ) (crPartF φ') * b) = 0 := 𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebranormalOrderF (a * (superCommuteF (anPartF φ)) (crPartF φ') * b) = 0 match φ, φ' with 𝓕:FieldSpecificationφ:𝓕.FieldOpφ'✝:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraφ':((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentumx✝:𝓕.FieldOpnormalOrderF (a * (superCommuteF (anPartF (FieldOp.inAsymp φ'))) (crPartF x✝) * b) = 0 All goals completed! 🐙 𝓕:FieldSpecificationφ:𝓕.FieldOpφ'✝:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrax✝:𝓕.FieldOpφ':((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × MomentumnormalOrderF (a * (superCommuteF (anPartF x✝)) (crPartF (FieldOp.outAsymp φ')) * b) = 0 All goals completed! 🐙 𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × MomentumnormalOrderF (a * (superCommuteF (anPartF (FieldOp.outAsymp a✝¹))) (crPartF (FieldOp.inAsymp a✝)) * b) = 0𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraa✝¹:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentuma✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimenormalOrderF (a * (superCommuteF (anPartF (FieldOp.outAsymp a✝¹))) (crPartF (FieldOp.position a✝)) * b) = 0𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraa✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × MomentumnormalOrderF (a * (superCommuteF (anPartF (FieldOp.position a✝¹))) (crPartF (FieldOp.inAsymp a✝)) * b) = 0𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebraa✝¹:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimea✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimenormalOrderF (a * (superCommuteF (anPartF (FieldOp.position a✝¹))) (crPartF (FieldOp.position a✝)) * b) = 0 All goals completed! 🐙

The normal ordering of a product of two states

All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙@[simp] lemma normalOrderF_anPartF_mul_crPartF (φ φ' : 𝓕.FieldOp) : 𝓝ᶠ(anPartF φ * crPartF φ') = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') (crPartF φ' * anPartF φ) := 𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpnormalOrderF (anPartF φ * crPartF φ') = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') (crPartF φ' * anPartF φ) All goals completed! 🐙lemma normalOrderF_ofFieldOpF_mul_ofFieldOpF (φ φ' : 𝓕.FieldOp) : 𝓝ᶠ(ofFieldOpF φ * ofFieldOpF φ') = crPartF φ * crPartF φ' + 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') (crPartF φ' * anPartF φ) + crPartF φ * anPartF φ' + anPartF φ * anPartF φ' := 𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpnormalOrderF (ofFieldOpF φ * ofFieldOpF φ') = crPartF φ * crPartF φ' + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') (crPartF φ' * anPartF φ) + crPartF φ * anPartF φ' + anPartF φ * anPartF φ' 𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOpcrPartF φ * crPartF φ' + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') (crPartF φ' * anPartF φ) + (crPartF φ * anPartF φ' + anPartF φ * anPartF φ') = crPartF φ * crPartF φ' + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') (crPartF φ' * anPartF φ) + crPartF φ * anPartF φ' + anPartF φ * anPartF φ' All goals completed! 🐙

Normal order with super commutators

TODO "Split the following two lemmas up into smaller parts."All goals completed! 🐙All goals completed! 🐙

Super commutators involving a normal order.

lemma ofCrAnListF_superCommuteF_normalOrderF_ofCrAnListF (φs φs' : List 𝓕.CrAnFieldOp) : [ofCrAnListF φs, 𝓝ᶠ(ofCrAnListF φs')]ₛF = ofCrAnListF φs * 𝓝ᶠ(ofCrAnListF φs') - 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') 𝓝ᶠ(ofCrAnListF φs') * ofCrAnListF φs := 𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.CrAnFieldOp(superCommuteF (ofCrAnListF φs)) (normalOrderF (ofCrAnListF φs')) = ofCrAnListF φs * normalOrderF (ofCrAnListF φs') - (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.crAnStatistics φs') normalOrderF (ofCrAnListF φs') * ofCrAnListF φs All goals completed! 🐙All goals completed! 🐙

Multiplications with normal order written in terms of super commute.

lemma ofCrAnListF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF (φs : List 𝓕.CrAnFieldOp) (φs' : List 𝓕.FieldOp) : ofCrAnListF φs * 𝓝ᶠ(ofFieldOpListF φs') = 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') 𝓝ᶠ(ofFieldOpListF φs') * ofCrAnListF φs + [ofCrAnListF φs, 𝓝ᶠ(ofFieldOpListF φs')]ₛF := 𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOpφs':List 𝓕.FieldOpofCrAnListF φs * normalOrderF (ofFieldOpListF φs') = (exchangeSign (ofList 𝓕.crAnStatistics φs)) (ofList 𝓕.fieldOpStatistic φs') normalOrderF (ofFieldOpListF φs') * ofCrAnListF φs + (superCommuteF (ofCrAnListF φs)) (normalOrderF (ofFieldOpListF φs')) All goals completed! 🐙lemma ofCrAnOpF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF (φ : 𝓕.CrAnFieldOp) (φs' : List 𝓕.FieldOp) : ofCrAnOpF φ * 𝓝ᶠ(ofFieldOpListF φs') = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs') 𝓝ᶠ(ofFieldOpListF φs') * ofCrAnOpF φ + [ofCrAnOpF φ, 𝓝ᶠ(ofFieldOpListF φs')]ₛF := 𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs':List 𝓕.FieldOpofCrAnOpF φ * normalOrderF (ofFieldOpListF φs') = (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic φs') normalOrderF (ofFieldOpListF φs') * ofCrAnOpF φ + (superCommuteF (ofCrAnOpF φ)) (normalOrderF (ofFieldOpListF φs')) All goals completed! 🐙𝓕:FieldSpecificationφ:𝓕.FieldOpφs':List 𝓕.FieldOpanPartF φ * normalOrderF (ofFieldOpListF φs') = (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs') (normalOrderF (ofFieldOpListF φs') * anPartF φ) + (superCommuteF (anPartF φ)) (normalOrderF (ofFieldOpListF φs')) match φ with 𝓕:FieldSpecificationφ:𝓕.FieldOpφs':List 𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × MomentumanPartF (FieldOp.inAsymp a✝) * normalOrderF (ofFieldOpListF φs') = (exchangeSign (𝓕|>ₛFieldOp.inAsymp a✝)) (ofList 𝓕.fieldOpStatistic φs') (normalOrderF (ofFieldOpListF φs') * anPartF (FieldOp.inAsymp a✝)) + (superCommuteF (anPartF (FieldOp.inAsymp a✝))) (normalOrderF (ofFieldOpListF φs')) All goals completed! 🐙 𝓕:FieldSpecificationφ:𝓕.FieldOpφs':List 𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × MomentumanPartF (FieldOp.outAsymp a✝) * normalOrderF (ofFieldOpListF φs') = (exchangeSign (𝓕|>ₛFieldOp.outAsymp a✝)) (ofList 𝓕.fieldOpStatistic φs') (normalOrderF (ofFieldOpListF φs') * anPartF (FieldOp.outAsymp a✝)) + (superCommuteF (anPartF (FieldOp.outAsymp a✝))) (normalOrderF (ofFieldOpListF φs'))𝓕:FieldSpecificationφ:𝓕.FieldOpφs':List 𝓕.FieldOpa✝:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTimeanPartF (FieldOp.position a✝) * normalOrderF (ofFieldOpListF φs') = (exchangeSign (𝓕|>ₛFieldOp.position a✝)) (ofList 𝓕.fieldOpStatistic φs') (normalOrderF (ofFieldOpListF φs') * anPartF (FieldOp.position a✝)) + (superCommuteF (anPartF (FieldOp.position a✝))) (normalOrderF (ofFieldOpListF φs')) All goals completed! 🐙