PhysLean Documentation

PhysLean.QFT.PerturbationTheory.FieldOpAlgebra.NormalOrder.Basic

Normal Ordering on Field operator algebra #

Normal order on super-commutators. #

The main result of this is ι_normalOrderF_superCommuteF_eq_zero_mul which states that applying ι to the normal order of something containing a super-commutator is zero.

source
theorem FieldSpecification.FieldOpAlgebra.ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero {𝓕 : FieldSpecification} (φa φa' : 𝓕.CrAnFieldOp) (φs φs' : List 𝓕.CrAnFieldOp) :
ι (FieldOpFreeAlgebra.normalOrderF (FieldOpFreeAlgebra.ofCrAnListF φs * (FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φa)) (FieldOpFreeAlgebra.ofCrAnOpF φa') * FieldOpFreeAlgebra.ofCrAnListF φs')) = 0
source
theorem FieldSpecification.FieldOpAlgebra.ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero {𝓕 : FieldSpecification} (φa φa' : 𝓕.CrAnFieldOp) (φs : List 𝓕.CrAnFieldOp) (a : 𝓕.FieldOpFreeAlgebra) :
ι (FieldOpFreeAlgebra.normalOrderF (FieldOpFreeAlgebra.ofCrAnListF φs * (FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φa)) (FieldOpFreeAlgebra.ofCrAnOpF φa') * a)) = 0
source
theorem FieldSpecification.FieldOpAlgebra.ι_normalOrderF_superCommuteF_ofCrAnOpF_eq_zero_mul {𝓕 : FieldSpecification} (φa φa' : 𝓕.CrAnFieldOp) (a b : 𝓕.FieldOpFreeAlgebra) :
ι (FieldOpFreeAlgebra.normalOrderF (a * (FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φa)) (FieldOpFreeAlgebra.ofCrAnOpF φa') * b)) = 0
source
theorem FieldSpecification.FieldOpAlgebra.ι_normalOrderF_superCommuteF_ofCrAnOpF_ofCrAnListF_eq_zero_mul {𝓕 : FieldSpecification} (φa : 𝓕.CrAnFieldOp) (φs : List 𝓕.CrAnFieldOp) (a b : 𝓕.FieldOpFreeAlgebra) :
ι (FieldOpFreeAlgebra.normalOrderF (a * (FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnOpF φa)) (FieldOpFreeAlgebra.ofCrAnListF φs) * b)) = 0
source
theorem FieldSpecification.FieldOpAlgebra.ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnOpF_eq_zero_mul {𝓕 : FieldSpecification} (φa : 𝓕.CrAnFieldOp) (φs : List 𝓕.CrAnFieldOp) (a b : 𝓕.FieldOpFreeAlgebra) :
ι (FieldOpFreeAlgebra.normalOrderF (a * (FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnListF φs)) (FieldOpFreeAlgebra.ofCrAnOpF φa) * b)) = 0
source
theorem FieldSpecification.FieldOpAlgebra.ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero_mul {𝓕 : FieldSpecification} (φs φs' : List 𝓕.CrAnFieldOp) (a b : 𝓕.FieldOpFreeAlgebra) :
ι (FieldOpFreeAlgebra.normalOrderF (a * (FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnListF φs)) (FieldOpFreeAlgebra.ofCrAnListF φs') * b)) = 0
source
theorem FieldSpecification.FieldOpAlgebra.ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero_mul {𝓕 : FieldSpecification} (φs : List 𝓕.CrAnFieldOp) (a b c : 𝓕.FieldOpFreeAlgebra) :
ι (FieldOpFreeAlgebra.normalOrderF (a * (FieldOpFreeAlgebra.superCommuteF (FieldOpFreeAlgebra.ofCrAnListF φs)) c * b)) = 0
source
@[simp]
theorem FieldSpecification.FieldOpAlgebra.ι_normalOrderF_superCommuteF_eq_zero_mul {𝓕 : FieldSpecification} (a b c d : 𝓕.FieldOpFreeAlgebra) :
ι (FieldOpFreeAlgebra.normalOrderF (a * (FieldOpFreeAlgebra.superCommuteF d) c * b)) = 0
source
@[simp]
theorem FieldSpecification.FieldOpAlgebra.ι_normalOrder_superCommuteF_eq_zero_mul_right {𝓕 : FieldSpecification} (b c d : 𝓕.FieldOpFreeAlgebra) :
ι (FieldOpFreeAlgebra.normalOrderF ((FieldOpFreeAlgebra.superCommuteF d) c * b)) = 0
source
@[simp]
theorem FieldSpecification.FieldOpAlgebra.ι_normalOrderF_superCommuteF_eq_zero_mul_left {𝓕 : FieldSpecification} (a c d : 𝓕.FieldOpFreeAlgebra) :
ι (FieldOpFreeAlgebra.normalOrderF (a * (FieldOpFreeAlgebra.superCommuteF d) c)) = 0
source
@[simp]
theorem FieldSpecification.FieldOpAlgebra.ι_normalOrderF_superCommuteF_eq_zero_mul_mul_right {𝓕 : FieldSpecification} (a b1 b2 c d : 𝓕.FieldOpFreeAlgebra) :
ι (FieldOpFreeAlgebra.normalOrderF (a * (FieldOpFreeAlgebra.superCommuteF d) c * b1 * b2)) = 0
source
@[simp]
theorem FieldSpecification.FieldOpAlgebra.ι_normalOrderF_superCommuteF_eq_zero {𝓕 : FieldSpecification} (c d : 𝓕.FieldOpFreeAlgebra) :
ι (FieldOpFreeAlgebra.normalOrderF ((FieldOpFreeAlgebra.superCommuteF d) c)) = 0

Defining normal order for FiedOpAlgebra. #

source
theorem FieldSpecification.FieldOpAlgebra.ι_normalOrderF_zero_of_mem_ideal {𝓕 : FieldSpecification} (a : 𝓕.FieldOpFreeAlgebra) (h : a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet) :
ι (FieldOpFreeAlgebra.normalOrderF a) = 0
source
theorem FieldSpecification.FieldOpAlgebra.ι_normalOrderF_eq_of_equiv {𝓕 : FieldSpecification} (a b : 𝓕.FieldOpFreeAlgebra) (h : a ≈ b) :
ι (FieldOpFreeAlgebra.normalOrderF a) = ι (FieldOpFreeAlgebra.normalOrderF b)
source
noncomputable def FieldSpecification.FieldOpAlgebra.normalOrder {𝓕 : FieldSpecification} :
𝓕.FieldOpAlgebra →ₗ[ℂ] 𝓕.FieldOpAlgebra

For a field specification 𝓕, normalOrder is the linear map

FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕

defined as the descent of ι ∘ₗ normalOrderF : FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 from FieldOpFreeAlgebra 𝓕 to FieldOpAlgebra 𝓕. This descent exists because ι ∘ₗ normalOrderF is well-defined on equivalence classes.

The notation 𝓝(a) is used for normalOrder a for a an element of FieldOpAlgebra 𝓕.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def FieldSpecification.FieldOpAlgebra.«term𝓝(_)» :
    Lean.ParserDescr

    For a field specification 𝓕, normalOrder is the linear map

    FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕

    defined as the descent of ι ∘ₗ normalOrderF : FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 from FieldOpFreeAlgebra 𝓕 to FieldOpAlgebra 𝓕. This descent exists because ι ∘ₗ normalOrderF is well-defined on equivalence classes.

    The notation 𝓝(a) is used for normalOrder a for a an element of FieldOpAlgebra 𝓕.

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