PhysLean Documentation

PhysLean.QFT.PerturbationTheory.FieldOpAlgebra.WickTerm

Wick term #

source
def WickContraction.wickTerm {๐“• : 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ฮ›.wickTerm is defined as

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

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

Equations
Instances For
    source
    @[simp]
    theorem WickContraction.wickTerm_empty_nil {๐“• : FieldSpecification} :
    empty.wickTerm = 1

    For the empty list [] of ๐“•.FieldOp, the wickTerm of the Wick contraction corresponding to the empty set โˆ… (the only Wick contraction of []) is 1.

    source
    theorem WickContraction.wickTerm_insert_none {๐“• : FieldSpecification} (ฯ† : ๐“•.FieldOp) (ฯ†s : List ๐“•.FieldOp) (i : Fin ฯ†s.length.succ) (ฯ†sฮ› : WickContraction ฯ†s.length) :
    (insertAndContract ฯ† ฯ†sฮ› i none).wickTerm = (FieldStatistic.exchangeSign (๐“•.fieldOpStatistic ฯ†)) (FieldStatistic.ofFinset ๐“•.fieldOpStatistic ฯ†s.get (Finset.filter (fun (k : Fin ฯ†s.length) => i.succAbove k < i) Finset.univ)) โ€ข (sign ฯ†s ฯ†sฮ› โ€ข โ†‘ฯ†sฮ›.timeContract * FieldSpecification.FieldOpAlgebra.normalOrder (FieldSpecification.FieldOpAlgebra.ofFieldOpList (ฯ† :: ฯ†sฮ›.uncontractedListGet)))

    For a list ฯ†s = ฯ†โ‚€โ€ฆฯ†โ‚™ of ๐“•.FieldOp, a Wick contraction ฯ†sฮ› of ฯ†s, an element ฯ† of ๐“•.FieldOp, and i โ‰ค ฯ†s.length, then (ฯ†sฮ› โ†ฉฮ› ฯ† i none).wickTerm is equal to

    ๐“ข(ฯ†, ฯ†โ‚€โ€ฆฯ†แตขโ‚‹โ‚) ฯ†sฮ›.sign โ€ข ฯ†sฮ›.timeContract * ๐“(ฯ† :: [ฯ†sฮ›]แต˜แถœ)

    The proof of this result relies on

    • normalOrder_uncontracted_none to rewrite normal orderings.
    • timeContract_insert_none to rewrite the time contract.
    • sign_insert_none to rewrite the sign.
    source
    theorem WickContraction.wickTerm_insert_some {๐“• : FieldSpecification} (ฯ† : ๐“•.FieldOp) (ฯ†s : List ๐“•.FieldOp) (i : Fin ฯ†s.length.succ) (ฯ†sฮ› : WickContraction ฯ†s.length) (k : { x : Fin ฯ†s.length // x โˆˆ ฯ†sฮ›.uncontracted }) (hlt : โˆ€ (k : Fin ฯ†s.length), FieldSpecification.timeOrderRel ฯ† ฯ†s[k]) (hn : โˆ€ (k : Fin ฯ†s.length), i.succAbove k < i โ†’ ยฌFieldSpecification.timeOrderRel ฯ†s[k] ฯ†) :
    (insertAndContract ฯ† ฯ†sฮ› i (some k)).wickTerm = (FieldStatistic.exchangeSign (๐“•.fieldOpStatistic ฯ†)) (FieldStatistic.ofFinset ๐“•.fieldOpStatistic ฯ†s.get (Finset.filter (fun (x : Fin ฯ†s.length) => i.succAbove x < i) Finset.univ)) โ€ข (sign ฯ†s ฯ†sฮ› โ€ข (FieldSpecification.FieldOpAlgebra.contractStateAtIndex ฯ† ฯ†sฮ›.uncontractedListGet ((uncontractedFieldOpEquiv ฯ†s ฯ†sฮ›) (some k)) * โ†‘ฯ†sฮ›.timeContract) * 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, i โ‰ค ฯ†s.length and a k in ฯ†sฮ›.uncontracted, such that all ๐“•.FieldOp in ฯ†โ‚€โ€ฆฯ†แตขโ‚‹โ‚ have time strictly less than ฯ† and ฯ† has a time greater than or equal to all FieldOp in ฯ†โ‚€โ€ฆฯ†โ‚™, then (ฯ†sฮ› โ†ฉฮ› ฯ† i (some k)).staticWickTerm is equal to the product of

    • the sign ๐“ข(ฯ†, ฯ†โ‚€โ€ฆฯ†แตขโ‚‹โ‚)
    • the sign ฯ†sฮ›.sign
    • ฯ†sฮ›.timeContract
    • s โ€ข [anPart ฯ†, ofFieldOp ฯ†s[k]]โ‚› where s is the sign associated with moving ฯ† through uncontracted fields in ฯ†โ‚€โ€ฆฯ†โ‚–โ‚‹โ‚
    • the normal ordering [ฯ†sฮ›]แต˜แถœ with the field corresponding to k removed.

    The proof of this result relies on

    • timeContract_insert_some_of_not_lt and timeContract_insert_some_of_lt to rewrite time contractions.
    • normalOrder_uncontracted_some to rewrite normal orderings.
    • sign_insert_some_of_not_lt and sign_insert_some_of_lt to rewrite signs.
    source
    theorem WickContraction.mul_wickTerm_eq_sum {๐“• : FieldSpecification} (ฯ† : ๐“•.FieldOp) (ฯ†s : List ๐“•.FieldOp) (i : Fin ฯ†s.length.succ) (ฯ†sฮ› : WickContraction ฯ†s.length) (hlt : โˆ€ (k : Fin ฯ†s.length), FieldSpecification.timeOrderRel ฯ† ฯ†s[k]) (hn : โˆ€ (k : Fin ฯ†s.length), i.succAbove k < i โ†’ ยฌFieldSpecification.timeOrderRel ฯ†s[k] ฯ†) :
    FieldSpecification.FieldOpAlgebra.ofFieldOp ฯ† * ฯ†sฮ›.wickTerm = (FieldStatistic.exchangeSign (๐“•.fieldOpStatistic ฯ†)) (FieldStatistic.ofFinset ๐“•.fieldOpStatistic ฯ†s.get (Finset.filter (fun (x : Fin ฯ†s.length) => i.succAbove x < i) Finset.univ)) โ€ข โˆ‘ k : Option { x : Fin ฯ†s.length // x โˆˆ ฯ†sฮ›.uncontracted }, (insertAndContract ฯ† ฯ†sฮ› i k).wickTerm

    For a list ฯ†s = ฯ†โ‚€โ€ฆฯ†โ‚™ of ๐“•.FieldOp, a Wick contraction ฯ†sฮ› of ฯ†s, an element ฯ† of ๐“•.FieldOp, and i โ‰ค ฯ†s.length such that all ๐“•.FieldOp in ฯ†โ‚€โ€ฆฯ†แตขโ‚‹โ‚ have time strictly less than ฯ† and ฯ† has a time greater than or equal to all FieldOp in ฯ†โ‚€โ€ฆฯ†โ‚™, then

    ฯ† * ฯ†sฮ›.wickTerm = ๐“ข(ฯ†, ฯ†โ‚€โ€ฆฯ†แตขโ‚‹โ‚) โ€ข โˆ‘ k, (ฯ†sฮ› โ†ฉฮ› ฯ† i k).wickTerm

    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 wickTerm_insert_none and wickTerm_insert_some are used to equate terms.