PhysLean Documentation

PhysLean.QFT.PerturbationTheory.FieldOpAlgebra.StaticWickTerm

Static Wick's terms #

source
def WickContraction.staticWickTerm {๐“• : FieldSpecification} {ฯ†s : List ๐“•.FieldOp} (ฯ†sฮ› : WickContraction ฯ†s.length) :
๐“•.FieldOpAlgebra

For a list ฯ†s of ๐“•.FieldOp, and a Wick contraction ฯ†sฮ› of ฯ†s, the element of ๐“•.FieldOpAlgebra, ฯ†sฮ›.staticWickTerm is defined as

ฯ†sฮ›.sign โ€ข ฯ†sฮ›.staticContract * ๐“([ฯ†sฮ›]แต˜แถœ).

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[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.

    source
    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.FieldOpAlgebra.normalOrder (FieldSpecification.FieldOpAlgebra.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.
    source
    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.FieldOpAlgebra.contractStateAtIndex ฯ† ฯ†sฮ›.uncontractedListGet ((uncontractedFieldOpEquiv ฯ†s ฯ†sฮ›) (some k)) * FieldSpecification.FieldOpAlgebra.normalOrder (FieldSpecification.FieldOpAlgebra.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.
    source
    theorem WickContraction.mul_staticWickTerm_eq_sum {๐“• : FieldSpecification} (ฯ† : ๐“•.FieldOp) (ฯ†s : List ๐“•.FieldOp) (ฯ†sฮ› : WickContraction ฯ†s.length) :
    FieldSpecification.FieldOpAlgebra.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: