Static Wick's terms

def WickContraction.staticWickTerm {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : 𝓕.WickAlgebra

For a list φs of 𝓕.FieldOp, and a Wick contraction φsΛ of φs, the element of 𝓕.WickAlgebra, φsΛ.staticWickTerm is defined as

φsΛ.sign • φsΛ.staticContract * 𝓝([φsΛ]ᵘᶜ).

This is a term which appears in the static version Wick's theorem.

Equations

• φsΛ.staticWickTerm = WickContraction.sign φs φsΛ • ↑φsΛ.staticContract * FieldSpecification.WickAlgebra.normalOrder (FieldSpecification.WickAlgebra.ofFieldOpList φsΛ.uncontractedListGet)

@[simp]

theorem WickContraction.staticWickTerm_empty_nil {𝓕 : FieldSpecification} : empty.staticWickTerm = 1

For the empty list [] of 𝓕.FieldOp, the staticWickTerm of the Wick contraction corresponding to the empty set ∅ (the only Wick contraction of []) is 1.

theorem WickContraction.staticWickTerm_insert_zero_none {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) : (insertAndContract φ φsΛ 0 none).staticWickTerm = sign φs φsΛ • ↑φsΛ.staticContract * FieldSpecification.WickAlgebra.normalOrder (FieldSpecification.WickAlgebra.ofFieldOpList (φ :: φsΛ.uncontractedListGet))

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, and an element φ of 𝓕.FieldOp, then (φsΛ ↩Λ φ 0 none).staticWickTerm is equal to

φsΛ.sign • φsΛ.staticWickTerm * 𝓝(φ :: [φsΛ]ᵘᶜ)

The proof of this result relies on

• staticContract_insert_none to rewrite the static contract.
• sign_insert_none_zero to rewrite the sign.

theorem WickContraction.staticWickTerm_insert_zero_some {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (k : { x : Fin φs.length // x ∈ φsΛ.uncontracted }) : (insertAndContract φ φsΛ 0 (some k)).staticWickTerm = sign φs φsΛ • (↑φsΛ.staticContract * (FieldSpecification.WickAlgebra.contractStateAtIndex φ φsΛ.uncontractedListGet ((uncontractedFieldOpEquiv φs φsΛ) (some k)) * FieldSpecification.WickAlgebra.normalOrder (FieldSpecification.WickAlgebra.ofFieldOpList (PhysLean.List.optionEraseZ φsΛ.uncontractedListGet φ ((uncontractedFieldOpEquiv φs φsΛ) (some k))))))

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp, and a k in φsΛ.uncontracted, (φsΛ ↩Λ φ 0 (some k)).wickTerm is equal to the product of

• the sign 𝓢(φ, φ₀…φᵢ₋₁)
• the sign φsΛ.sign
• φsΛ.staticContract
• s • [anPart φ, ofFieldOp φs[k]]ₛ where s is the sign associated with moving φ through uncontracted fields in φ₀…φₖ₋₁
• the normal ordering of [φsΛ]ᵘᶜ with the field operator φs[k] removed.

The proof of this result ultimately relies on

• staticContract_insert_some to rewrite static contractions.
• normalOrder_uncontracted_some to rewrite normal orderings.
• sign_insert_some_zero to rewrite signs.

theorem WickContraction.mul_staticWickTerm_eq_sum {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) : FieldSpecification.WickAlgebra.ofFieldOp φ * φsΛ.staticWickTerm = ∑ k : Option { x : Fin φs.length // x ∈ φsΛ.uncontracted }, (insertAndContract φ φsΛ 0 k).staticWickTerm

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, the following relation holds

φ * φsΛ.staticWickTerm = ∑ k, (φsΛ ↩Λ φ 0 k).staticWickTerm

where the sum is over all k in Option φsΛ.uncontracted, so k is either none or some k.

The proof proceeds as follows:

• ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum is used to expand φ 𝓝([φsΛ]ᵘᶜ) as a sum over k in Option φsΛ.uncontracted of terms involving [anPart φ, φs[k]]ₛ.
• Then staticWickTerm_insert_zero_none and staticWickTerm_insert_zero_some are used to equate terms.