1. Physlib
  2. QFT
  3. PerturbationTheory
  4. WickAlgebra
  5. WicksTheoremNormal
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.WickAlgebra.StaticWickTheorem public import Physlib.QFT.PerturbationTheory.WickAlgebra.WicksTheorem public import Physlib.QFT.PerturbationTheory.WickContraction.Sign.Join public import Physlib.QFT.PerturbationTheory.WickContraction.TimeCond

Wick's theorem for normal ordered lists

@[expose] public section

For a list φs of 𝓕.FieldOp, then

𝓣(φs) = ∑ φsΛ, φsΛ.sign • φsΛ.timeContract * 𝓣(𝓝([φsΛ]ᵘᶜ))

where the sum is over all Wick contraction φsΛ which only have equal time contractions.

This result follows from

    static_wick_theorem to rewrite 𝓣(φs) on the left hand side as a sum of 𝓣(φsΛ.staticWickTerm).

    EqTimeOnly.timeOrder_staticContract_of_not_mem and timeOrder_timeOrder_mid to set to those 𝓣(φsΛ.staticWickTerm) for which φsΛ has a contracted pair which are not equal time to zero.

    staticContract_eq_timeContract_of_eqTimeOnly to rewrite the static contract in the remaining 𝓣(φsΛ.staticWickTerm) as a time contract.

    timeOrder_timeContract_mul_of_eqTimeOnly_left to move the time contracts out of the time ordering.

𝓕:FieldSpecificationφs:List 𝓕.FieldOpe2:WickContraction φs.length ≃ { φsΛ // φsΛ.EqTimeOnly } ⊕ { φsΛ // ¬φsΛ.EqTimeOnly } := (Equiv.sumCompl EqTimeOnly).symmx:{ φsΛ // φsΛ.EqTimeOnly }⊢ (↑x).EqTimeOnly𝓕:FieldSpecificationφs:List 𝓕.FieldOpe2:WickContraction φs.length ≃ { φsΛ // φsΛ.EqTimeOnly } ⊕ { φsΛ // ¬φsΛ.EqTimeOnly } := (Equiv.sumCompl EqTimeOnly).symmx:{ φsΛ // φsΛ.EqTimeOnly }⊢ (↑x).EqTimeOnly 𝓕:FieldSpecificationφs:List 𝓕.FieldOpe2:WickContraction φs.length ≃ { φsΛ // φsΛ.EqTimeOnly } ⊕ { φsΛ // ¬φsΛ.EqTimeOnly } := (Equiv.sumCompl EqTimeOnly).symmx:{ φsΛ // φsΛ.EqTimeOnly }⊢ (↑x).EqTimeOnly𝓕:FieldSpecificationφs:List 𝓕.FieldOpe2:WickContraction φs.length ≃ { φsΛ // φsΛ.EqTimeOnly } ⊕ { φsΛ // ¬φsΛ.EqTimeOnly } := (Equiv.sumCompl EqTimeOnly).symmx:{ φsΛ // φsΛ.EqTimeOnly }⊢ (↑x).EqTimeOnly All goals completed! 🐙
𝓕:FieldSpecificationφs:List 𝓕.FieldOpe1:{ φsΛ // φsΛ.EqTimeOnly } ≃ { φsΛ // ↑φsΛ = empty } ⊕ { φsΛ // ¬↑φsΛ = empty } := (Equiv.sumCompl fun φsΛ => ↑φsΛ = empty).symm⊢ ∑ i, sign φs ↑↑((Equiv.subtypeSubtypeEquivSubtypeInter (fun φsΛ => φsΛ.EqTimeOnly) fun x => x ≠ empty).symm i) • (↑(↑↑((Equiv.subtypeSubtypeEquivSubtypeInter (fun φsΛ => φsΛ.EqTimeOnly) fun x => x ≠ empty).symm i)).timeContract * timeOrder (normalOrder (ofFieldOpList [↑↑((Equiv.subtypeSubtypeEquivSubtypeInter (fun φsΛ => φsΛ.EqTimeOnly) fun x => x ≠ empty).symm i)]ᵘᶜ))) = ∑ x, sign φs ↑x • (↑(↑x).timeContract * timeOrder (normalOrder (ofFieldOpList [↑x]ᵘᶜ))) All goals completed! 🐙

For a list φs of 𝓕.FieldOp, then

𝓣(𝓝(φs)) = 𝓣(φs) - ∑ φsΛ, φsΛ.sign • φsΛ.timeContract.1 * 𝓣(𝓝([φsΛ]ᵘᶜ))

where the sum is over all non-empty Wick contraction φsΛ which only have equal time contractions.

This result follows directly from

    timeOrder_ofFieldOpList_eqTimeOnly

lemma normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty (φs : List 𝓕.FieldOp) : 𝓣(𝓝(ofFieldOpList φs)) = 𝓣(ofFieldOpList φs) - ∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs) ∧ φsΛ ≠ empty}), φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)) := 𝓕:FieldSpecificationφs:List 𝓕.FieldOp⊢ timeOrder (normalOrder (ofFieldOpList φs)) = timeOrder (ofFieldOpList φs) - ∑ φsΛ, sign φs ↑φsΛ • ↑(↑φsΛ).timeContract * timeOrder (normalOrder (ofFieldOpList [↑φsΛ]ᵘᶜ)) All goals completed! 🐙

For a list φs of 𝓕.FieldOp, then 𝓣(φs) is equal to the sum of

    ∑ φsΛ, φsΛ.wickTerm where the sum is over all Wick contraction φsΛ which have no contractions of equal time.

    ∑ φsΛ, φsΛ.sign • φsΛ.timeContract * (∑ φssucΛ, φssucΛ.wickTerm), where the first sum is over all Wick contraction φsΛ which only have equal time contractions and the second sum is over all Wick contraction φssucΛ of the uncontracted elements of φsΛ which do not have any equal time contractions.

The proof proceeds as follows

    wicks_theorem is used to rewrite 𝓣(φs) as a sum over all Wick contractions.

    The sum over all Wick contractions is then split additively into two parts based on having or not having an equal time contractions.

    Using join, the sum ∑ φsΛ, _ over Wick contractions which do have equal time contractions is split into two sums ∑ φsΛ, ∑ φsucΛ, _, the first over non-zero elements which only have equal time contractions and the second over Wick contractions φsucΛ of [φsΛ]ᵘᶜ which do not have equal time contractions.

    join_sign_timeContract is then used to equate terms.

All goals completed! 🐙
𝓕:FieldSpecificationφs:List 𝓕.FieldOp⊢ ∑ φsΛ, sign φs ↑φsΛ • ↑(↑φsΛ).timeContract * normalOrder (ofFieldOpList [↑φsΛ]ᵘᶜ) + (∑ φsΛ, sign φs ↑φsΛ • ↑(↑φsΛ).timeContract * ∑ φssucΛ, (↑φssucΛ).wickTerm - ∑ φsΛ, sign φs ↑φsΛ • ↑(↑φsΛ).timeContract * timeOrder (normalOrder (ofFieldOpList [↑φsΛ]ᵘᶜ))) = ∑ φsΛ, (↑φsΛ).wickTerm + ∑ φsΛ, sign φs ↑φsΛ • ↑(↑φsΛ).timeContract * (∑ φssucΛ, (↑φssucΛ).wickTerm - timeOrder (normalOrder (ofFieldOpList [↑φsΛ]ᵘᶜ))) 𝓕:FieldSpecificationφs:List 𝓕.FieldOp⊢ ∑ φsΛ, sign φs ↑φsΛ • ↑(↑φsΛ).timeContract * ∑ φssucΛ, (↑φssucΛ).wickTerm - ∑ φsΛ, sign φs ↑φsΛ • ↑(↑φsΛ).timeContract * timeOrder (normalOrder (ofFieldOpList [↑φsΛ]ᵘᶜ)) = ∑ φsΛ, sign φs ↑φsΛ • ↑(↑φsΛ).timeContract * (∑ φssucΛ, (↑φssucΛ).wickTerm - timeOrder (normalOrder (ofFieldOpList [↑φsΛ]ᵘᶜ))) All goals completed! 🐙𝓕:FieldSpecificatione2:{ φsΛ // ¬φsΛ.HaveEqTime } ≃ Unit := { toFun := fun x => (), invFun := fun x => ⟨empty, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }h1':ofFieldOpList [] = ofCrAnList []⊢ ι (crAnTimeOrderSign [] • ofCrAnListF (crAnTimeOrderList [])) = ι (ofCrAnListF []) All goals completed! 🐙

For a list φs of 𝓕.FieldOp, the normal-ordered version of Wick's theorem states that

𝓣(𝓝(φs)) = ∑ φsΛ, φsΛ.wickTerm

where the sum is over all Wick contraction φsΛ in which no two contracted elements have the same time.

The proof proceeds by induction on φs, with the base case [] holding by following through definitions. and the inductive case holding as a result of

    timeOrder_haveEqTime_split

    normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty

    and the induction hypothesis on 𝓣(𝓝([φsΛ.1]ᵘᶜ)) for contractions φsΛ of φs which only have equal time contractions and are non-empty.

𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpa✝:∀ (y : List 𝓕.FieldOp), InvImage (fun x1 x2 => x1 < x2) (fun x => x.length) y φs✝ → timeOrder (normalOrder (ofFieldOpList y)) = ∑ φsΛ, (↑φsΛ).wickTermφ:𝓕.FieldOpφs:List 𝓕.FieldOpx✝:∀ (y : List 𝓕.FieldOp), InvImage (fun x1 x2 => x1 < x2) (fun x => x.length) y (φ :: φs) → timeOrder (normalOrder (ofFieldOpList y)) = ∑ φsΛ, (↑φsΛ).wickTermφsΛ:{ φsΛ // φsΛ.EqTimeOnly ∧ ¬φsΛ = empty }hφsΛ:φsΛ ∈ Finset.univ⊢ (↑φsΛ).uncontracted.card < φs.length + 1 𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpa✝:∀ (y : List 𝓕.FieldOp), InvImage (fun x1 x2 => x1 < x2) (fun x => x.length) y φs✝ → timeOrder (normalOrder (ofFieldOpList y)) = ∑ φsΛ, (↑φsΛ).wickTermφ:𝓕.FieldOpφs:List 𝓕.FieldOpx✝:∀ (y : List 𝓕.FieldOp), InvImage (fun x1 x2 => x1 < x2) (fun x => x.length) y (φ :: φs) → timeOrder (normalOrder (ofFieldOpList y)) = ∑ φsΛ, (↑φsΛ).wickTermφsΛ:{ φsΛ // φsΛ.EqTimeOnly ∧ ¬φsΛ = empty }hφsΛ:φsΛ ∈ Finset.univhc:(↑φsΛ).uncontracted.card = (φ :: φs).length ↔ ↑φsΛ = empty⊢ (↑φsΛ).uncontracted.card < φs.length + 1 𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpa✝:∀ (y : List 𝓕.FieldOp), InvImage (fun x1 x2 => x1 < x2) (fun x => x.length) y φs✝ → timeOrder (normalOrder (ofFieldOpList y)) = ∑ φsΛ, (↑φsΛ).wickTermφ:𝓕.FieldOpφs:List 𝓕.FieldOpx✝:∀ (y : List 𝓕.FieldOp), InvImage (fun x1 x2 => x1 < x2) (fun x => x.length) y (φ :: φs) → timeOrder (normalOrder (ofFieldOpList y)) = ∑ φsΛ, (↑φsΛ).wickTermφsΛ:{ φsΛ // φsΛ.EqTimeOnly ∧ ¬φsΛ = empty }hφsΛ:φsΛ ∈ Finset.univhc:¬(↑φsΛ).uncontracted.card = φs.length + 1⊢ (↑φsΛ).uncontracted.card < φs.length + 1 𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpa✝:∀ (y : List 𝓕.FieldOp), InvImage (fun x1 x2 => x1 < x2) (fun x => x.length) y φs✝ → timeOrder (normalOrder (ofFieldOpList y)) = ∑ φsΛ, (↑φsΛ).wickTermφ:𝓕.FieldOpφs:List 𝓕.FieldOpx✝:∀ (y : List 𝓕.FieldOp), InvImage (fun x1 x2 => x1 < x2) (fun x => x.length) y (φ :: φs) → timeOrder (normalOrder (ofFieldOpList y)) = ∑ φsΛ, (↑φsΛ).wickTermφsΛ:{ φsΛ // φsΛ.EqTimeOnly ∧ ¬φsΛ = empty }hφsΛ:φsΛ ∈ Finset.univhc:¬(↑φsΛ).uncontracted.card = φs.length + 1hc':(↑φsΛ).uncontracted.card ≤ (φ :: φs).length⊢ (↑φsΛ).uncontracted.card < φs.length + 1 𝓕:FieldSpecificationφs✝:List 𝓕.FieldOpa✝:∀ (y : List 𝓕.FieldOp), InvImage (fun x1 x2 => x1 < x2) (fun x => x.length) y φs✝ → timeOrder (normalOrder (ofFieldOpList y)) = ∑ φsΛ, (↑φsΛ).wickTermφ:𝓕.FieldOpφs:List 𝓕.FieldOpx✝:∀ (y : List 𝓕.FieldOp), InvImage (fun x1 x2 => x1 < x2) (fun x => x.length) y (φ :: φs) → timeOrder (normalOrder (ofFieldOpList y)) = ∑ φsΛ, (↑φsΛ).wickTermφsΛ:{ φsΛ // φsΛ.EqTimeOnly ∧ ¬φsΛ = empty }hc:¬(↑φsΛ).uncontracted.card = φs.length + 1hc':(↑φsΛ).uncontracted.card ≤ φs.length + 1⊢ (↑φsΛ).uncontracted.card < φs.length + 1 All goals completed! 🐙