PhysLean Documentation

PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.NormalOrder

Normal Ordering in the FieldOpFreeAlgebra #

In the module PhysLean.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.

source
def FieldSpecification.FieldOpFreeAlgebra.normalOrderF {𝓕 : FieldSpecification} :
𝓕.FieldOpFreeAlgebra β†’β‚—[β„‚] 𝓕.FieldOpFreeAlgebra

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 𝓕.

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

    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 𝓕.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_ofCrAnListF {𝓕 : FieldSpecification} (Ο†s : List 𝓕.CrAnFieldOp) :
      normalOrderF (ofCrAnListF Ο†s) = normalOrderSign Ο†s β€’ ofCrAnListF (normalOrderList Ο†s)
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_eq_normalOrderF {𝓕 : FieldSpecification} (Ο†s : List 𝓕.CrAnFieldOp) :
      ofCrAnListF (normalOrderList Ο†s) = normalOrderSign Ο†s β€’ normalOrderF (ofCrAnListF Ο†s)
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_one {𝓕 : FieldSpecification} :
      normalOrderF 1 = 1
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_normalOrderF_mid {𝓕 : FieldSpecification} (a b c : 𝓕.FieldOpFreeAlgebra) :
      normalOrderF (a * b * c) = normalOrderF (a * normalOrderF b * c)
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_normalOrderF_right {𝓕 : FieldSpecification} (a b : 𝓕.FieldOpFreeAlgebra) :
      normalOrderF (a * b) = normalOrderF (a * normalOrderF b)
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_normalOrderF_left {𝓕 : FieldSpecification} (a b : 𝓕.FieldOpFreeAlgebra) :
      normalOrderF (a * b) = normalOrderF (normalOrderF a * b)

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

      source
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_ofCrAnListF_cons_create {𝓕 : FieldSpecification} (Ο† : 𝓕.CrAnFieldOp) (hΟ† : 𝓕.crAnFieldOpToCreateAnnihilate Ο† = CreateAnnihilate.create) (Ο†s : List 𝓕.CrAnFieldOp) :
      normalOrderF (ofCrAnListF (Ο† :: Ο†s)) = ofCrAnOpF Ο† * normalOrderF (ofCrAnListF Ο†s)
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_create_mul {𝓕 : FieldSpecification} (Ο† : 𝓕.CrAnFieldOp) (hΟ† : 𝓕.crAnFieldOpToCreateAnnihilate Ο† = CreateAnnihilate.create) (a : 𝓕.FieldOpFreeAlgebra) :
      normalOrderF (ofCrAnOpF Ο† * a) = ofCrAnOpF Ο† * normalOrderF a
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_ofCrAnListF_append_annihilate {𝓕 : FieldSpecification} (Ο† : 𝓕.CrAnFieldOp) (hΟ† : 𝓕.crAnFieldOpToCreateAnnihilate Ο† = CreateAnnihilate.annihilate) (Ο†s : List 𝓕.CrAnFieldOp) :
      normalOrderF (ofCrAnListF (Ο†s ++ [Ο†])) = normalOrderF (ofCrAnListF Ο†s) * ofCrAnOpF Ο†
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_mul_annihilate {𝓕 : FieldSpecification} (Ο† : 𝓕.CrAnFieldOp) (hΟ† : 𝓕.crAnFieldOpToCreateAnnihilate Ο† = CreateAnnihilate.annihilate) (a : 𝓕.FieldOpFreeAlgebra) :
      normalOrderF (a * ofCrAnOpF Ο†) = normalOrderF a * ofCrAnOpF Ο†
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_crPartF_mul {𝓕 : FieldSpecification} (Ο† : 𝓕.FieldOp) (a : 𝓕.FieldOpFreeAlgebra) :
      normalOrderF (crPartF Ο† * a) = crPartF Ο† * normalOrderF a
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_mul_anPartF {𝓕 : FieldSpecification} (Ο† : 𝓕.FieldOp) (a : 𝓕.FieldOpFreeAlgebra) :
      normalOrderF (a * anPartF Ο†) = normalOrderF a * anPartF Ο†

      Normal ordering for an adjacent creation and annihilation state #

      The main result of this section is normalOrderF_superCommuteF_annihilate_create.

      source
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_swap_create_annihilate_ofCrAnListF_ofCrAnListF {𝓕 : FieldSpecification} (Ο†c Ο†a : 𝓕.CrAnFieldOp) (hΟ†c : 𝓕.crAnFieldOpToCreateAnnihilate Ο†c = CreateAnnihilate.create) (hΟ†a : 𝓕.crAnFieldOpToCreateAnnihilate Ο†a = CreateAnnihilate.annihilate) (Ο†s Ο†s' : List 𝓕.CrAnFieldOp) :
      normalOrderF (ofCrAnListF Ο†s' * ofCrAnOpF Ο†c * ofCrAnOpF Ο†a * ofCrAnListF Ο†s) = (FieldStatistic.exchangeSign (𝓕.crAnStatistics Ο†c)) (𝓕.crAnStatistics Ο†a) β€’ normalOrderF (ofCrAnListF Ο†s' * ofCrAnOpF Ο†a * ofCrAnOpF Ο†c * ofCrAnListF Ο†s)
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_swap_create_annihilate_ofCrAnListF {𝓕 : FieldSpecification} (Ο†c Ο†a : 𝓕.CrAnFieldOp) (hΟ†c : 𝓕.crAnFieldOpToCreateAnnihilate Ο†c = CreateAnnihilate.create) (hΟ†a : 𝓕.crAnFieldOpToCreateAnnihilate Ο†a = CreateAnnihilate.annihilate) (Ο†s : List 𝓕.CrAnFieldOp) (a : 𝓕.FieldOpFreeAlgebra) :
      normalOrderF (ofCrAnListF Ο†s * ofCrAnOpF Ο†c * ofCrAnOpF Ο†a * a) = (FieldStatistic.exchangeSign (𝓕.crAnStatistics Ο†c)) (𝓕.crAnStatistics Ο†a) β€’ normalOrderF (ofCrAnListF Ο†s * ofCrAnOpF Ο†a * ofCrAnOpF Ο†c * a)
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_swap_create_annihilate {𝓕 : FieldSpecification} (Ο†c Ο†a : 𝓕.CrAnFieldOp) (hΟ†c : 𝓕.crAnFieldOpToCreateAnnihilate Ο†c = CreateAnnihilate.create) (hΟ†a : 𝓕.crAnFieldOpToCreateAnnihilate Ο†a = CreateAnnihilate.annihilate) (a b : 𝓕.FieldOpFreeAlgebra) :
      normalOrderF (a * ofCrAnOpF Ο†c * ofCrAnOpF Ο†a * b) = (FieldStatistic.exchangeSign (𝓕.crAnStatistics Ο†c)) (𝓕.crAnStatistics Ο†a) β€’ normalOrderF (a * ofCrAnOpF Ο†a * ofCrAnOpF Ο†c * b)
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_superCommuteF_create_annihilate {𝓕 : FieldSpecification} (Ο†c Ο†a : 𝓕.CrAnFieldOp) (hΟ†c : 𝓕.crAnFieldOpToCreateAnnihilate Ο†c = CreateAnnihilate.create) (hΟ†a : 𝓕.crAnFieldOpToCreateAnnihilate Ο†a = CreateAnnihilate.annihilate) (a b : 𝓕.FieldOpFreeAlgebra) :
      normalOrderF (a * (superCommuteF (ofCrAnOpF Ο†c)) (ofCrAnOpF Ο†a) * b) = 0
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_superCommuteF_annihilate_create {𝓕 : FieldSpecification} (Ο†c Ο†a : 𝓕.CrAnFieldOp) (hΟ†c : 𝓕.crAnFieldOpToCreateAnnihilate Ο†c = CreateAnnihilate.create) (hΟ†a : 𝓕.crAnFieldOpToCreateAnnihilate Ο†a = CreateAnnihilate.annihilate) (a b : 𝓕.FieldOpFreeAlgebra) :
      normalOrderF (a * (superCommuteF (ofCrAnOpF Ο†a)) (ofCrAnOpF Ο†c) * b) = 0
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_swap_crPartF_anPartF {𝓕 : FieldSpecification} (Ο† Ο†' : 𝓕.FieldOp) (a b : 𝓕.FieldOpFreeAlgebra) :
      normalOrderF (a * crPartF Ο† * anPartF Ο†' * b) = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic Ο†)) (𝓕.fieldOpStatistic Ο†') β€’ normalOrderF (a * anPartF Ο†' * crPartF Ο† * b)

      Normal ordering for an anPartF and crPartF #

      Using the results from above.

      source
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_swap_anPartF_crPartF {𝓕 : FieldSpecification} (Ο† Ο†' : 𝓕.FieldOp) (a b : 𝓕.FieldOpFreeAlgebra) :
      normalOrderF (a * anPartF Ο† * crPartF Ο†' * b) = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic Ο†)) (𝓕.fieldOpStatistic Ο†') β€’ normalOrderF (a * crPartF Ο†' * anPartF Ο† * b)
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_superCommuteF_crPartF_anPartF {𝓕 : FieldSpecification} (Ο† Ο†' : 𝓕.FieldOp) (a b : 𝓕.FieldOpFreeAlgebra) :
      normalOrderF (a * (superCommuteF (crPartF Ο†)) (anPartF Ο†') * b) = 0
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_superCommuteF_anPartF_crPartF {𝓕 : FieldSpecification} (Ο† Ο†' : 𝓕.FieldOp) (a b : 𝓕.FieldOpFreeAlgebra) :
      normalOrderF (a * (superCommuteF (anPartF Ο†)) (crPartF Ο†') * b) = 0

      The normal ordering of a product of two states #

      source
      @[simp]
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_crPartF_mul_crPartF {𝓕 : FieldSpecification} (Ο† Ο†' : 𝓕.FieldOp) :
      normalOrderF (crPartF Ο† * crPartF Ο†') = crPartF Ο† * crPartF Ο†'
      source
      @[simp]
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_anPartF_mul_anPartF {𝓕 : FieldSpecification} (Ο† Ο†' : 𝓕.FieldOp) :
      normalOrderF (anPartF Ο† * anPartF Ο†') = anPartF Ο† * anPartF Ο†'
      source
      @[simp]
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_crPartF_mul_anPartF {𝓕 : FieldSpecification} (Ο† Ο†' : 𝓕.FieldOp) :
      normalOrderF (crPartF Ο† * anPartF Ο†') = crPartF Ο† * anPartF Ο†'
      source
      @[simp]
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_anPartF_mul_crPartF {𝓕 : FieldSpecification} (Ο† Ο†' : 𝓕.FieldOp) :
      normalOrderF (anPartF Ο† * crPartF Ο†') = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic Ο†)) (𝓕.fieldOpStatistic Ο†') β€’ (crPartF Ο†' * anPartF Ο†)
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_ofFieldOpF_mul_ofFieldOpF {𝓕 : FieldSpecification} (Ο† Ο†' : 𝓕.FieldOp) :
      normalOrderF (ofFieldOpF Ο† * ofFieldOpF Ο†') = crPartF Ο† * crPartF Ο†' + (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic Ο†)) (𝓕.fieldOpStatistic Ο†') β€’ (crPartF Ο†' * anPartF Ο†) + crPartF Ο† * anPartF Ο†' + anPartF Ο† * anPartF Ο†'

      Normal order with super commutators #

      source
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_superCommuteF_ofCrAnListF_create_create_ofCrAnListF {𝓕 : FieldSpecification} (Ο†c Ο†c' : 𝓕.CrAnFieldOp) (hΟ†c : 𝓕.crAnFieldOpToCreateAnnihilate Ο†c = CreateAnnihilate.create) (hΟ†c' : 𝓕.crAnFieldOpToCreateAnnihilate Ο†c' = CreateAnnihilate.create) (Ο†s Ο†s' : List 𝓕.CrAnFieldOp) :
      normalOrderF (ofCrAnListF Ο†s * (superCommuteF (ofCrAnOpF Ο†c)) (ofCrAnOpF Ο†c') * ofCrAnListF Ο†s') = normalOrderSign (Ο†s ++ Ο†c' :: Ο†c :: Ο†s') β€’ (ofCrAnListF (createFilter Ο†s) * (superCommuteF (ofCrAnOpF Ο†c)) (ofCrAnOpF Ο†c') * ofCrAnListF (createFilter Ο†s') * ofCrAnListF (annihilateFilter (Ο†s ++ Ο†s')))
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.normalOrderF_superCommuteF_ofCrAnListF_annihilate_annihilate_ofCrAnListF {𝓕 : FieldSpecification} (Ο†a Ο†a' : 𝓕.CrAnFieldOp) (hΟ†a : 𝓕.crAnFieldOpToCreateAnnihilate Ο†a = CreateAnnihilate.annihilate) (hΟ†a' : 𝓕.crAnFieldOpToCreateAnnihilate Ο†a' = CreateAnnihilate.annihilate) (Ο†s Ο†s' : List 𝓕.CrAnFieldOp) :
      normalOrderF (ofCrAnListF Ο†s * (superCommuteF (ofCrAnOpF Ο†a)) (ofCrAnOpF Ο†a') * ofCrAnListF Ο†s') = normalOrderSign (Ο†s ++ Ο†a' :: Ο†a :: Ο†s') β€’ (ofCrAnListF (createFilter (Ο†s ++ Ο†s')) * ofCrAnListF (annihilateFilter Ο†s) * (superCommuteF (ofCrAnOpF Ο†a)) (ofCrAnOpF Ο†a') * ofCrAnListF (annihilateFilter Ο†s'))

      Super commutators involving a normal order. #

      source
      theorem FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_superCommuteF_normalOrderF_ofCrAnListF {𝓕 : FieldSpecification} (Ο†s Ο†s' : List 𝓕.CrAnFieldOp) :
      (superCommuteF (ofCrAnListF Ο†s)) (normalOrderF (ofCrAnListF Ο†s')) = ofCrAnListF Ο†s * normalOrderF (ofCrAnListF Ο†s') - (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.crAnStatistics Ο†s)) (FieldStatistic.ofList 𝓕.crAnStatistics Ο†s') β€’ normalOrderF (ofCrAnListF Ο†s') * ofCrAnListF Ο†s
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_superCommuteF_normalOrderF_ofFieldOpListF {𝓕 : FieldSpecification} (Ο†s : List 𝓕.CrAnFieldOp) (Ο†s' : List 𝓕.FieldOp) :
      (superCommuteF (ofCrAnListF Ο†s)) (normalOrderF (ofFieldOpListF Ο†s')) = ofCrAnListF Ο†s * normalOrderF (ofFieldOpListF Ο†s') - (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.crAnStatistics Ο†s)) (FieldStatistic.ofList 𝓕.fieldOpStatistic Ο†s') β€’ normalOrderF (ofFieldOpListF Ο†s') * ofCrAnListF Ο†s

      Multiplications with normal order written in terms of super commute. #

      source
      theorem FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF {𝓕 : FieldSpecification} (Ο†s : List 𝓕.CrAnFieldOp) (Ο†s' : List 𝓕.FieldOp) :
      ofCrAnListF Ο†s * normalOrderF (ofFieldOpListF Ο†s') = (FieldStatistic.exchangeSign (FieldStatistic.ofList 𝓕.crAnStatistics Ο†s)) (FieldStatistic.ofList 𝓕.fieldOpStatistic Ο†s') β€’ normalOrderF (ofFieldOpListF Ο†s') * ofCrAnListF Ο†s + (superCommuteF (ofCrAnListF Ο†s)) (normalOrderF (ofFieldOpListF Ο†s'))
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF {𝓕 : FieldSpecification} (Ο† : 𝓕.CrAnFieldOp) (Ο†s' : List 𝓕.FieldOp) :
      ofCrAnOpF Ο† * normalOrderF (ofFieldOpListF Ο†s') = (FieldStatistic.exchangeSign (𝓕.crAnStatistics Ο†)) (FieldStatistic.ofList 𝓕.fieldOpStatistic Ο†s') β€’ normalOrderF (ofFieldOpListF Ο†s') * ofCrAnOpF Ο† + (superCommuteF (ofCrAnOpF Ο†)) (normalOrderF (ofFieldOpListF Ο†s'))
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.anPartF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF {𝓕 : FieldSpecification} (Ο† : 𝓕.FieldOp) (Ο†s' : List 𝓕.FieldOp) :
      anPartF Ο† * normalOrderF (ofFieldOpListF Ο†s') = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic Ο†)) (FieldStatistic.ofList 𝓕.fieldOpStatistic Ο†s') β€’ normalOrderF (ofFieldOpListF Ο†s' * anPartF Ο†) + (superCommuteF (anPartF Ο†)) (normalOrderF (ofFieldOpListF Ο†s'))