PhysLean Documentation

PhysLean.QFT.PerturbationTheory.FieldOpAlgebra.StaticWickTheorem

Static Wick's theorem #

source
theorem FieldSpecification.FieldOpAlgebra.static_wick_theorem {š“• : FieldSpecification} (Ļ†s : List š“•.FieldOp) :
ofFieldOpList Ļ†s = āˆ‘ Ļ†sĪ› : WickContraction Ļ†s.length, Ļ†sĪ›.staticWickTerm

For a list Ļ†s of š“•.FieldOp, the static version of Wick's theorem states that

Ļ†s = āˆ‘ Ļ†sĪ›, Ļ†sĪ›.staticWickTerm

where the sum is over all Wick contraction Ļ†sĪ›.

The proof is via induction on Ļ†s.

  • The base case Ļ†s = [] is handled by staticWickTerm_empty_nil.

The inductive step works as follows:

For the LHS:

  1. The proof considers Ļ†ā‚€ā€¦Ļ†ā‚™ as Ļ†ā‚€(Ļ†ā‚ā€¦Ļ†ā‚™) and uses the induction hypothesis on Ļ†ā‚ā€¦Ļ†ā‚™.
  2. This gives terms of the form Ļ† * Ļ†sĪ›.staticWickTerm on which mul_staticWickTerm_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 1) and optional uncontracted elements of Ļ†sĪ› (from 2)

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.