PhysLean Documentation

PhysLean.QFT.PerturbationTheory.FieldOpAlgebra.NormalOrder.WickContractions

Normal ordering with relation to Wick contractions #

Normal order of uncontracted terms within proto-algebra. #

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

For a list ฯ†s = ฯ†โ‚€โ€ฆฯ†โ‚™ of ๐“•.FieldOp, a Wick contraction ฯ†sฮ› of ฯ†s, an element ฯ† of ๐“•.FieldOp, and a i โ‰ค ฯ†s.length, then the following relation holds:

๐“([ฯ†sฮ› โ†ฉฮ› ฯ† i none]แต˜แถœ) = s โ€ข ๐“(ฯ† :: [ฯ†sฮ›]แต˜แถœ)

where s is the exchange sign for ฯ† and the uncontracted fields in ฯ†โ‚€โ€ฆฯ†แตขโ‚‹โ‚.

The proof of this result ultimately is a consequence of normalOrder_superCommute_eq_zero.

source
theorem FieldSpecification.FieldOpAlgebra.normalOrder_uncontracted_some {๐“• : FieldSpecification} (ฯ† : ๐“•.FieldOp) (ฯ†s : List ๐“•.FieldOp) (i : Fin ฯ†s.length.succ) (ฯ†sฮ› : WickContraction ฯ†s.length) (k : { x : Fin ฯ†s.length // x โˆˆ ฯ†sฮ›.uncontracted }) :
normalOrder (ofFieldOpList (WickContraction.insertAndContract ฯ† ฯ†sฮ› i (some k)).uncontractedListGet) = normalOrder (ofFieldOpList (PhysLean.List.optionEraseZ ฯ†sฮ›.uncontractedListGet ฯ† ((WickContraction.uncontractedFieldOpEquiv ฯ†s ฯ†sฮ›) (some k))))

For a list ฯ†s = ฯ†โ‚€โ€ฆฯ†โ‚™ of ๐“•.FieldOp, a Wick contraction ฯ†sฮ› of ฯ†s, an element ฯ† of ๐“•.FieldOp, a i โ‰ค ฯ†s.length and a k in ฯ†sฮ›.uncontracted, then ๐“([ฯ†sฮ› โ†ฉฮ› ฯ† i (some k)]แต˜แถœ) is equal to the normal ordering of [ฯ†sฮ›]แต˜แถœ with the ๐“•.FieldOp corresponding to k removed.

The proof of this result ultimately is a consequence of definitions.