Wick's theorem for normal ordered lists

theorem FieldSpecification.FieldOpAlgebra.timeOrder_ofFieldOpList_eqTimeOnly {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) : timeOrder (ofFieldOpList φs) = ∑ φsΛ : { φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly }, WickContraction.sign φs ↑φsΛ • ↑(↑φsΛ).timeContract * timeOrder (normalOrder (ofFieldOpList (↑φsΛ).uncontractedListGet))

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.

theorem FieldSpecification.FieldOpAlgebra.timeOrder_ofFieldOpList_eq_eqTimeOnly_empty {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) : timeOrder (ofFieldOpList φs) = timeOrder (normalOrder (ofFieldOpList φs)) + ∑ φsΛ : { φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly ∧ φsΛ ≠ WickContraction.empty }, WickContraction.sign φs ↑φsΛ • ↑(↑φsΛ).timeContract * timeOrder (normalOrder (ofFieldOpList (↑φsΛ).uncontractedListGet))

theorem FieldSpecification.FieldOpAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) : timeOrder (normalOrder (ofFieldOpList φs)) = timeOrder (ofFieldOpList φs) - ∑ φsΛ : { φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly ∧ φsΛ ≠ WickContraction.empty }, WickContraction.sign φs ↑φsΛ • ↑(↑φsΛ).timeContract * timeOrder (normalOrder (ofFieldOpList (↑φsΛ).uncontractedListGet))

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

theorem FieldSpecification.FieldOpAlgebra.timeOrder_haveEqTime_split {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) : timeOrder (ofFieldOpList φs) = ∑ φsΛ : { φsΛ : WickContraction φs.length // ¬φsΛ.HaveEqTime }, WickContraction.sign φs ↑φsΛ • ↑(↑φsΛ).timeContract * normalOrder (ofFieldOpList (↑φsΛ).uncontractedListGet) + ∑ φsΛ : { φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly ∧ φsΛ ≠ WickContraction.empty }, WickContraction.sign φs ↑φsΛ • ↑(↑φsΛ).timeContract * ∑ φssucΛ : { φssucΛ : WickContraction (↑φsΛ).uncontractedListGet.length // ¬φssucΛ.HaveEqTime }, (↑φssucΛ).wickTerm

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.

theorem FieldSpecification.FieldOpAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) : timeOrder (normalOrder (ofFieldOpList φs)) = ∑ φsΛ : { φsΛ : WickContraction φs.length // ¬φsΛ.HaveEqTime }, (↑φsΛ).wickTerm + ∑ φsΛ : { φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly ∧ φsΛ ≠ WickContraction.empty }, WickContraction.sign φs ↑φsΛ • ↑(↑φsΛ).timeContract * (∑ φssucΛ : { φssucΛ : WickContraction (↑φsΛ).uncontractedListGet.length // ¬φssucΛ.HaveEqTime }, (↑φssucΛ).wickTerm - timeOrder (normalOrder (ofFieldOpList (↑φsΛ).uncontractedListGet)))

theorem FieldSpecification.FieldOpAlgebra.wicks_theorem_normal_order_empty {𝓕 : FieldSpecification} : timeOrder (normalOrder (ofFieldOpList [])) = ∑ φsΛ : { φsΛ : WickContraction [].length // ¬φsΛ.HaveEqTime }, (↑φsΛ).wickTerm

@[irreducible]

theorem FieldSpecification.FieldOpAlgebra.wicks_theorem_normal_order {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) : timeOrder (normalOrder (ofFieldOpList φs)) = ∑ φsΛ : { φsΛ : WickContraction φs.length // ¬φsΛ.HaveEqTime }, (↑φsΛ).wickTerm

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.