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.NormalOrder.WickContractions
public import Physlib.QFT.PerturbationTheory.WickContraction.Sign.InsertNone
public import Physlib.QFT.PerturbationTheory.WickContraction.Sign.InsertSome
public import Physlib.QFT.PerturbationTheory.WickContraction.StaticContractStatic Wick's terms
@[expose] public section
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.
def staticWickTerm {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : 𝓕.WickAlgebra :=
φsΛ.sign • φsΛ.staticContract * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ)
For the empty list [] of 𝓕.FieldOp, the staticWickTerm of the Wick contraction
corresponding to the empty set ∅ (the only Wick contraction of []) is 1.
𝓕:FieldSpecification⊢ sign [] empty • ↑empty.staticContract * normalOrder (ofFieldOpList (List.map [].get [])) = 1
All goals completed! 🐙
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.
lemma staticWickTerm_insert_zero_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
(φsΛ : WickContraction φs.length) :
(φsΛ ↩Λ φ 0 none).staticWickTerm =
φsΛ.sign • φsΛ.staticContract * 𝓝(ofFieldOpList (φ :: [φsΛ]ᵘᶜ)) := 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.length⊢ (φsΛ↩Λφ 0none).staticWickTerm = sign φs φsΛ • ↑φsΛ.staticContract * normalOrder (ofFieldOpList (φ :: [φsΛ]ᵘᶜ))
All goals completed! 🐙
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.
𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthk:↥φsΛ.uncontractedhn:¬(𝓕|>ₛφ) = 𝓕|>ₛφs[↑↑k]h0:GradingCompliant φs φsΛh1:contractStateAtIndex φ [φsΛ]ᵘᶜ ((uncontractedFieldOpEquiv φs φsΛ) (some k)) = 0⊢ sign φs φsΛ • (↑φsΛ.staticContract * contractStateAtIndex φ [φsΛ]ᵘᶜ ((uncontractedFieldOpEquiv φs φsΛ) (some k))) =
(sign (φs.insertIdx (↑0) φ) (φsΛ↩Λφ 0some k) *
(exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k}))) •
(contractStateAtIndex φ [φsΛ]ᵘᶜ ((uncontractedFieldOpEquiv φs φsΛ) (some k)) * ↑φsΛ.staticContract)
All goals completed! 🐙
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.
set_option backward.isDefEq.respectTransparency false inAll goals completed! 🐙