PhysLean Documentation

PhysLean.QFT.PerturbationTheory.WickContraction.TimeContract

Time contractions #

source
noncomputable def WickContraction.timeContract {š“• : FieldSpecification} {Ļ†s : List š“•.FieldOp} (Ļ†sĪ› : WickContraction Ļ†s.length) :
ā†„(Subalgebra.center ā„‚ š“•.FieldOpAlgebra)

For a list Ļ†s of š“•.FieldOp and a Wick contraction Ļ†sĪ› the element of the center of š“•.FieldOpAlgebra, Ļ†sĪ›.timeContract is defined as the product of timeContract Ļ†s[j] Ļ†s[k] over contracted pairs {j, k} in Ļ†sĪ› with j < k.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem WickContraction.timeContract_insert_none {š“• : FieldSpecification} (Ļ† : š“•.FieldOp) (Ļ†s : List š“•.FieldOp) (Ļ†sĪ› : WickContraction Ļ†s.length) (i : Fin Ļ†s.length.succ) :
    (insertAndContract Ļ† Ļ†sĪ› i none).timeContract = Ļ†sĪ›.timeContract

    For a list Ļ†s = Ļ†ā‚€ā€¦Ļ†ā‚™ of š“•.FieldOp, a Wick contraction Ļ†sĪ› of Ļ†s, an element Ļ† of š“•.FieldOp, and a i ā‰¤ Ļ†s.length the following relation holds

    (Ļ†sĪ› ā†©Ī› Ļ† i none).timeContract = Ļ†sĪ›.timeContract

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

    source
    theorem WickContraction.timeContract_insertAndContract_some {š“• : FieldSpecification} (Ļ† : š“•.FieldOp) (Ļ†s : List š“•.FieldOp) (Ļ†sĪ› : WickContraction Ļ†s.length) (i : Fin Ļ†s.length.succ) (j : { x : Fin Ļ†s.length // x āˆˆ Ļ†sĪ›.uncontracted }) :
    (insertAndContract Ļ† Ļ†sĪ› i (some j)).timeContract = (if i < i.succAbove ā†‘j then āŸØFieldSpecification.FieldOpAlgebra.timeContract Ļ† Ļ†s[ā†‘j], ā‹ÆāŸ© else āŸØFieldSpecification.FieldOpAlgebra.timeContract Ļ†s[ā†‘j] Ļ†, ā‹ÆāŸ©) * Ļ†sĪ›.timeContract

    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)).timeContract is equal to the product of

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

    source
    @[simp]
    theorem WickContraction.timeContract_empty {š“• : FieldSpecification} (Ļ†s : List š“•.FieldOp) :
    empty.timeContract = 1
    source
    theorem WickContraction.timeContract_insert_some_of_lt {š“• : FieldSpecification} (Ļ† : š“•.FieldOp) (Ļ†s : List š“•.FieldOp) (Ļ†sĪ› : WickContraction Ļ†s.length) (i : Fin Ļ†s.length.succ) (k : { x : Fin Ļ†s.length // x āˆˆ Ļ†sĪ›.uncontracted }) (ht : FieldSpecification.timeOrderRel Ļ† Ļ†s[ā†‘k]) (hik : i < i.succAbove ā†‘k) :
    ā†‘(insertAndContract Ļ† Ļ†sĪ› i (some k)).timeContract = (FieldStatistic.exchangeSign (š“•.fieldOpStatistic Ļ†)) (FieldStatistic.ofFinset š“•.fieldOpStatistic Ļ†s.get (Finset.filter (fun (x : Fin Ļ†s.length) => x < ā†‘k) Ļ†sĪ›.uncontracted)) ā€¢ (FieldSpecification.FieldOpAlgebra.contractStateAtIndex Ļ† Ļ†sĪ›.uncontractedListGet ((uncontractedFieldOpEquiv Ļ†s Ļ†sĪ›) (some k)) * ā†‘Ļ†sĪ›.timeContract)

    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 such that i ā‰¤ k, with the condition that Ļ† has greater or equal time to Ļ†s[k], then (Ļ†sĪ› ā†©Ī› Ļ† i (some k)).timeContract is equal to the product of

    • [anPart Ļ†, Ļ†s[k]]ā‚›
    • Ļ†sĪ›.timeContract
    • two copies of the exchange sign of Ļ† with the uncontracted fields in Ļ†ā‚€ā€¦Ļ†ā‚–ā‚‹ā‚. These two exchange signs cancel each other out but are included for convenience.

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

    source
    theorem WickContraction.timeContract_insert_some_of_not_lt {š“• : FieldSpecification} (Ļ† : š“•.FieldOp) (Ļ†s : List š“•.FieldOp) (Ļ†sĪ› : WickContraction Ļ†s.length) (i : Fin Ļ†s.length.succ) (k : { x : Fin Ļ†s.length // x āˆˆ Ļ†sĪ›.uncontracted }) (ht : Ā¬FieldSpecification.timeOrderRel Ļ†s[ā†‘k] Ļ†) (hik : Ā¬i < i.succAbove ā†‘k) :
    ā†‘(insertAndContract Ļ† Ļ†sĪ› i (some k)).timeContract = (FieldStatistic.exchangeSign (š“•.fieldOpStatistic Ļ†)) (FieldStatistic.ofFinset š“•.fieldOpStatistic Ļ†s.get (Finset.filter (fun (x : Fin Ļ†s.length) => x ā‰¤ ā†‘k) Ļ†sĪ›.uncontracted)) ā€¢ (FieldSpecification.FieldOpAlgebra.contractStateAtIndex Ļ† Ļ†sĪ›.uncontractedListGet ((uncontractedFieldOpEquiv Ļ†s Ļ†sĪ›) (some k)) * ā†‘Ļ†sĪ›.timeContract)

    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 such that k < i, with the condition that Ļ†s[k] does not have time greater or equal to Ļ†, then (Ļ†sĪ› ā†©Ī› Ļ† i (some k)).timeContract is equal to the product of

    • [anPart Ļ†, Ļ†s[k]]ā‚›
    • Ļ†sĪ›.timeContract
    • the exchange sign of Ļ† with the uncontracted fields in Ļ†ā‚€ā€¦Ļ†ā‚–ā‚‹ā‚.
    • the exchange sign of Ļ† with the uncontracted fields in Ļ†ā‚€ā€¦Ļ†ā‚–.

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

    source
    theorem WickContraction.timeContract_of_not_gradingCompliant {š“• : FieldSpecification} (Ļ†s : List š“•.FieldOp) (Ļ†sĪ› : WickContraction Ļ†s.length) (h : Ā¬GradingCompliant Ļ†s Ļ†sĪ›) :
    Ļ†sĪ›.timeContract = 0