PhysLean Documentation

PhysLean.QFT.PerturbationTheory.FieldOpFreeAlgebra.TimeOrder

Time Ordering in the FieldOpFreeAlgebra #

Time order #

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

For a field specification 𝓕, timeOrderF is the linear map

FieldOpFreeAlgebra 𝓕 β†’β‚—[β„‚] FieldOpFreeAlgebra 𝓕

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

crAnTimeOrderSign Ο†s β€’ ofCrAnListF (crAnTimeOrderList Ο†s).

That is, timeOrderF time-orders the field operators and multiplies by the sign of the time order.

The notation 𝓣ᢠ(a) is used for timeOrderF a

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 𝓕, timeOrderF is the linear map

    FieldOpFreeAlgebra 𝓕 β†’β‚—[β„‚] FieldOpFreeAlgebra 𝓕

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

    crAnTimeOrderSign Ο†s β€’ ofCrAnListF (crAnTimeOrderList Ο†s).

    That is, timeOrderF time-orders the field operators and multiplies by the sign of the time order.

    The notation 𝓣ᢠ(a) is used for timeOrderF a

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.timeOrderF_ofCrAnListF {𝓕 : FieldSpecification} (Ο†s : List 𝓕.CrAnFieldOp) :
      timeOrderF (ofCrAnListF Ο†s) = crAnTimeOrderSign Ο†s β€’ ofCrAnListF (crAnTimeOrderList Ο†s)
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.timeOrderF_timeOrderF_mid {𝓕 : FieldSpecification} (a b c : 𝓕.FieldOpFreeAlgebra) :
      timeOrderF (a * b * c) = timeOrderF (a * timeOrderF b * c)
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.timeOrderF_timeOrderF_right {𝓕 : FieldSpecification} (a b : 𝓕.FieldOpFreeAlgebra) :
      timeOrderF (a * b) = timeOrderF (a * timeOrderF b)
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.timeOrderF_timeOrderF_left {𝓕 : FieldSpecification} (a b : 𝓕.FieldOpFreeAlgebra) :
      timeOrderF (a * b) = timeOrderF (timeOrderF a * b)
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.timeOrderF_ofFieldOpListF {𝓕 : FieldSpecification} (Ο†s : List 𝓕.FieldOp) :
      timeOrderF (ofFieldOpListF Ο†s) = timeOrderSign Ο†s β€’ ofFieldOpListF (timeOrderList Ο†s)
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.timeOrderF_ofFieldOpListF_nil {𝓕 : FieldSpecification} :
      timeOrderF (ofFieldOpListF []) = 1
      source
      @[simp]
      theorem FieldSpecification.FieldOpFreeAlgebra.timeOrderF_ofFieldOpListF_singleton {𝓕 : FieldSpecification} (Ο† : 𝓕.FieldOp) :
      timeOrderF (ofFieldOpListF [Ο†]) = ofFieldOpListF [Ο†]
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.timeOrderF_ofFieldOpF_ofFieldOpF_ordered {𝓕 : FieldSpecification} {Ο† ψ : 𝓕.FieldOp} (h : timeOrderRel Ο† ψ) :
      timeOrderF (ofFieldOpF Ο† * ofFieldOpF ψ) = ofFieldOpF Ο† * ofFieldOpF ψ
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.timeOrderF_ofFieldOpF_ofFieldOpF_not_ordered {𝓕 : FieldSpecification} {Ο† ψ : 𝓕.FieldOp} (h : Β¬timeOrderRel Ο† ψ) :
      timeOrderF (ofFieldOpF Ο† * ofFieldOpF ψ) = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic Ο†)) (𝓕.fieldOpStatistic ψ) β€’ ofFieldOpF ψ * ofFieldOpF Ο†
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.timeOrderF_ofFieldOpF_ofFieldOpF_not_ordered_eq_timeOrderF {𝓕 : FieldSpecification} {Ο† ψ : 𝓕.FieldOp} (h : Β¬timeOrderRel Ο† ψ) :
      timeOrderF (ofFieldOpF Ο† * ofFieldOpF ψ) = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic Ο†)) (𝓕.fieldOpStatistic ψ) β€’ timeOrderF (ofFieldOpF ψ * ofFieldOpF Ο†)
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel {𝓕 : FieldSpecification} {Ο† ψ : 𝓕.CrAnFieldOp} (h : Β¬crAnTimeOrderRel Ο† ψ) :
      timeOrderF ((superCommuteF (ofCrAnOpF Ο†)) (ofCrAnOpF ψ)) = 0
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_right {𝓕 : FieldSpecification} {Ο† ψ : 𝓕.CrAnFieldOp} (h : Β¬crAnTimeOrderRel Ο† ψ) (a : 𝓕.FieldOpFreeAlgebra) :
      timeOrderF (a * (superCommuteF (ofCrAnOpF Ο†)) (ofCrAnOpF ψ)) = 0
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_left {𝓕 : FieldSpecification} {Ο† ψ : 𝓕.CrAnFieldOp} (h : Β¬crAnTimeOrderRel Ο† ψ) (a : 𝓕.FieldOpFreeAlgebra) :
      timeOrderF ((superCommuteF (ofCrAnOpF Ο†)) (ofCrAnOpF ψ) * a) = 0
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_mid {𝓕 : FieldSpecification} {Ο† ψ : 𝓕.CrAnFieldOp} (h : Β¬crAnTimeOrderRel Ο† ψ) (a b : 𝓕.FieldOpFreeAlgebra) :
      timeOrderF (a * (superCommuteF (ofCrAnOpF Ο†)) (ofCrAnOpF ψ) * b) = 0
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.timeOrderF_superCommuteF_superCommuteF_ofCrAnOpF_not_crAnTimeOrderRel {𝓕 : FieldSpecification} {Ο†1 Ο†2 : 𝓕.CrAnFieldOp} (h : Β¬crAnTimeOrderRel Ο†1 Ο†2) (a : 𝓕.FieldOpFreeAlgebra) :
      timeOrderF ((superCommuteF a) ((superCommuteF (ofCrAnOpF Ο†1)) (ofCrAnOpF Ο†2))) = 0
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_not_crAnTimeOrderRel {𝓕 : FieldSpecification} {Ο†1 Ο†2 Ο†3 : 𝓕.CrAnFieldOp} (h12 : Β¬crAnTimeOrderRel Ο†1 Ο†2) (h13 : Β¬crAnTimeOrderRel Ο†1 Ο†3) :
      timeOrderF ((superCommuteF (ofCrAnOpF Ο†1)) ((superCommuteF (ofCrAnOpF Ο†2)) (ofCrAnOpF Ο†3))) = 0
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_not_crAnTimeOrderRel' {𝓕 : FieldSpecification} {Ο†1 Ο†2 Ο†3 : 𝓕.CrAnFieldOp} (h12 : Β¬crAnTimeOrderRel Ο†2 Ο†1) (h13 : Β¬crAnTimeOrderRel Ο†3 Ο†1) :
      timeOrderF ((superCommuteF (ofCrAnOpF Ο†1)) ((superCommuteF (ofCrAnOpF Ο†2)) (ofCrAnOpF Ο†3))) = 0
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_all_not_crAnTimeOrderRel {𝓕 : FieldSpecification} (Ο†1 Ο†2 Ο†3 : 𝓕.CrAnFieldOp) (h : Β¬(crAnTimeOrderRel Ο†1 Ο†2 ∧ crAnTimeOrderRel Ο†1 Ο†3 ∧ crAnTimeOrderRel Ο†2 Ο†1 ∧ crAnTimeOrderRel Ο†2 Ο†3 ∧ crAnTimeOrderRel Ο†3 Ο†1 ∧ crAnTimeOrderRel Ο†3 Ο†2)) :
      timeOrderF ((superCommuteF (ofCrAnOpF Ο†1)) ((superCommuteF (ofCrAnOpF Ο†2)) (ofCrAnOpF Ο†3))) = 0
      source
      theorem FieldSpecification.FieldOpFreeAlgebra.timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_eq_time {𝓕 : FieldSpecification} {Ο† ψ : 𝓕.CrAnFieldOp} (h1 : crAnTimeOrderRel Ο† ψ) (h2 : crAnTimeOrderRel ψ Ο†) :
      timeOrderF ((superCommuteF (ofCrAnOpF Ο†)) (ofCrAnOpF ψ)) = (superCommuteF (ofCrAnOpF Ο†)) (ofCrAnOpF ψ)

      Interaction with maxTimeField #

      source
      theorem FieldSpecification.FieldOpFreeAlgebra.timeOrderF_eq_maxTimeField_mul {𝓕 : FieldSpecification} (Ο† : 𝓕.FieldOp) (Ο†s : List 𝓕.FieldOp) :
      timeOrderF (ofFieldOpListF (Ο† :: Ο†s)) = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic (maxTimeField Ο† Ο†s))) (FieldStatistic.ofList 𝓕.fieldOpStatistic (List.take (maxTimeFieldPos Ο† Ο†s) (Ο† :: Ο†s))) β€’ ofFieldOpF (maxTimeField Ο† Ο†s) * timeOrderF (ofFieldOpListF (eraseMaxTimeField Ο† Ο†s))

      In the state algebra time, ordering obeys T(φ₀φ₁…φₙ) = s * Ο†α΅’ * T(Ο†β‚€Ο†β‚β€¦Ο†α΅’β‚‹β‚Ο†α΅’β‚Šβ‚β€¦Ο†β‚™) where Ο†α΅’ is the state which has maximum time and s is the exchange sign of Ο†α΅’ and φ₀φ₁…φᡒ₋₁.

      source
      theorem FieldSpecification.FieldOpFreeAlgebra.timeOrderF_eq_maxTimeField_mul_finset {𝓕 : FieldSpecification} (Ο† : 𝓕.FieldOp) (Ο†s : List 𝓕.FieldOp) :
      timeOrderF (ofFieldOpListF (Ο† :: Ο†s)) = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic (maxTimeField Ο† Ο†s))) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic (eraseMaxTimeField Ο† Ο†s).get (Finset.filter (fun (x : Fin (eraseMaxTimeField Ο† Ο†s).length) => (maxTimeFieldPosFin Ο† Ο†s).succAbove x < maxTimeFieldPosFin Ο† Ο†s) Finset.univ)) β€’ ofFieldOpF (maxTimeField Ο† Ο†s) * timeOrderF (ofFieldOpListF (eraseMaxTimeField Ο† Ο†s))

      In the state algebra time, ordering obeys T(φ₀φ₁…φₙ) = s * Ο†α΅’ * T(Ο†β‚€Ο†β‚β€¦Ο†α΅’β‚‹β‚Ο†α΅’β‚Šβ‚β€¦Ο†β‚™) where Ο†α΅’ is the state which has maximum time and s is the exchange sign of Ο†α΅’ and φ₀φ₁…φᡒ₋₁. Here s is written using finite sets.