Wick's theorem

This file contrains the time-dependent version of Wick's theorem for lists of fields containing both fermions and bosons.

Wick's theorem is related to Isserlis' theorem in mathematics.

Wick terms

Wick's theorem

theorem FieldSpecification.wicks_theorem_congr {𝓕 : FieldSpecification} {φs φs' : List 𝓕.FieldOp} (h : φs = φs') : ∑ φsΛ : WickContraction φs.length, φsΛ.wickTerm = ∑ φs'Λ : WickContraction φs'.length, φs'Λ.wickTerm

@[irreducible]

theorem FieldSpecification.wicks_theorem {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) : FieldOpAlgebra.timeOrder (FieldOpAlgebra.ofFieldOpList φs) = ∑ φsΛ : WickContraction φs.length, φsΛ.wickTerm

For a list φs of 𝓕.FieldOp, Wick's theorem states that

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

where the sum is over all Wick contraction φsΛ.

The proof is via induction on φs.

• The base case φs = [] is handled by wickTerm_empty_nil.

The inductive step works as follows:

For the LHS:

1. timeOrder_eq_maxTimeField_mul_finset is used to write 𝓣(φ₀…φₙ) as 𝓢(φᵢ,φ₀…φᵢ₋₁) • φᵢ * 𝓣(φ₀…φᵢ₋₁φᵢ₊₁φₙ) where φᵢ is the maximal time field in φ₀…φₙ
2. The induction hypothesis is then used on 𝓣(φ₀…φᵢ₋₁φᵢ₊₁φₙ) to expand it as a sum over Wick contractions of φ₀…φᵢ₋₁φᵢ₊₁φₙ.
3. This gives terms of the form φᵢ * φsΛ.wickTerm on which mul_wickTerm_eq_sum is used where φsΛ is a Wick contraction of φ₀…φᵢ₋₁φᵢ₊₁φ, to rewrite terms as a sum over optional uncontracted elements of φsΛ

On the LHS we now have a sum over Wick contractions φsΛ of φ₀…φᵢ₋₁φᵢ₊₁φ (from 2) and optional uncontracted elements of φsΛ (from 3)

For the RHS:

1. The sum over Wick contractions of φ₀…φₙ on the RHS is split via insertLift_sum into a sum over Wick contractions φsΛ of φ₀…φᵢ₋₁φᵢ₊₁φ and sum over optional uncontracted elements of φsΛ.

Both sides are now sums over the same thing and their terms equate by the nature of the lemmas used.