PhysLean Documentation

PhysLean.QFT.PerturbationTheory.WickContraction.SubContraction

Sub contractions #

source
def WickContraction.subContraction {๐“• : FieldSpecification} {ฯ†s : List ๐“•.FieldOp} {ฯ†sฮ› : WickContraction ฯ†s.length} (S : Finset (Finset (Fin ฯ†s.length))) (ha : S โŠ† โ†‘ฯ†sฮ›) :
WickContraction ฯ†s.length

Given a Wick contraction ฯ†sฮ›, and a subset of ฯ†sฮ›.1, the Wick contraction consisting of contracted pairs within that subset.

Equations
Instances For
    source
    theorem WickContraction.mem_of_mem_subContraction {๐“• : FieldSpecification} {ฯ†s : List ๐“•.FieldOp} {ฯ†sฮ› : WickContraction ฯ†s.length} {S : Finset (Finset (Fin ฯ†s.length))} {hs : S โŠ† โ†‘ฯ†sฮ›} {a : Finset (Fin ฯ†s.length)} (ha : a โˆˆ โ†‘(subContraction S hs)) :
    a โˆˆ โ†‘ฯ†sฮ›
    source
    def WickContraction.quotContraction {๐“• : FieldSpecification} {ฯ†s : List ๐“•.FieldOp} {ฯ†sฮ› : WickContraction ฯ†s.length} (S : Finset (Finset (Fin ฯ†s.length))) (ha : S โŠ† โ†‘ฯ†sฮ›) :
    WickContraction (subContraction S ha).uncontractedListGet.length

    Given a Wick contraction ฯ†sฮ›, and a subset S of ฯ†sฮ›.1, the Wick contraction on the uncontracted list [ฯ†sฮ›.subContraction S ha]แต˜แถœ consisting of the remaining contracted pairs of ฯ†sฮ› not in S.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem WickContraction.mem_of_mem_quotContraction {๐“• : FieldSpecification} {ฯ†s : List ๐“•.FieldOp} {ฯ†sฮ› : WickContraction ฯ†s.length} {S : Finset (Finset (Fin ฯ†s.length))} {hs : S โŠ† โ†‘ฯ†sฮ›} {a : Finset (Fin (subContraction S hs).uncontractedListGet.length)} (ha : a โˆˆ โ†‘(quotContraction S hs)) :
      Finset.map uncontractedListEmd a โˆˆ โ†‘ฯ†sฮ›
      source
      theorem WickContraction.mem_subContraction_or_quotContraction {๐“• : FieldSpecification} {ฯ†s : List ๐“•.FieldOp} {ฯ†sฮ› : WickContraction ฯ†s.length} {S : Finset (Finset (Fin ฯ†s.length))} {hs : S โŠ† โ†‘ฯ†sฮ›} {a : Finset (Fin ฯ†s.length)} (ha : a โˆˆ โ†‘ฯ†sฮ›) :
      a โˆˆ โ†‘(subContraction S hs) โˆจ โˆƒ (a' : Finset (Fin (subContraction S hs).uncontractedListGet.length)), Finset.map uncontractedListEmd a' = a โˆง a' โˆˆ โ†‘(quotContraction S hs)
      source
      @[simp]
      theorem WickContraction.subContraction_uncontractedList_get {๐“• : FieldSpecification} {ฯ†s : List ๐“•.FieldOp} {ฯ†sฮ› : WickContraction ฯ†s.length} {S : Finset (Finset (Fin ฯ†s.length))} {hs : S โŠ† โ†‘ฯ†sฮ›} {a : Fin (subContraction S hs).uncontractedListGet.length} :
      (subContraction S hs).uncontractedListGet[a] = ฯ†s[uncontractedListEmd a]
      source
      @[simp]
      theorem WickContraction.subContraction_fstFieldOfContract {๐“• : FieldSpecification} {ฯ†s : List ๐“•.FieldOp} {ฯ†sฮ› : WickContraction ฯ†s.length} {S : Finset (Finset (Fin ฯ†s.length))} {hs : S โŠ† โ†‘ฯ†sฮ›} (a : { x : Finset (Fin ฯ†s.length) // x โˆˆ โ†‘(subContraction S hs) }) :
      (subContraction S hs).fstFieldOfContract a = ฯ†sฮ›.fstFieldOfContract โŸจโ†‘a, โ‹ฏโŸฉ
      source
      @[simp]
      theorem WickContraction.subContraction_sndFieldOfContract {๐“• : FieldSpecification} {ฯ†s : List ๐“•.FieldOp} {ฯ†sฮ› : WickContraction ฯ†s.length} {S : Finset (Finset (Fin ฯ†s.length))} {hs : S โŠ† โ†‘ฯ†sฮ›} (a : { x : Finset (Fin ฯ†s.length) // x โˆˆ โ†‘(subContraction S hs) }) :
      (subContraction S hs).sndFieldOfContract a = ฯ†sฮ›.sndFieldOfContract โŸจโ†‘a, โ‹ฏโŸฉ
      source
      @[simp]
      theorem WickContraction.quotContraction_fstFieldOfContract_uncontractedListEmd {๐“• : FieldSpecification} {ฯ†s : List ๐“•.FieldOp} {ฯ†sฮ› : WickContraction ฯ†s.length} {S : Finset (Finset (Fin ฯ†s.length))} {hs : S โŠ† โ†‘ฯ†sฮ›} (a : { x : Finset (Fin (subContraction S hs).uncontractedListGet.length) // x โˆˆ โ†‘(quotContraction S hs) }) :
      uncontractedListEmd ((quotContraction S hs).fstFieldOfContract a) = ฯ†sฮ›.fstFieldOfContract โŸจFinset.map uncontractedListEmd โ†‘a, โ‹ฏโŸฉ
      source
      @[simp]
      theorem WickContraction.quotContraction_sndFieldOfContract_uncontractedListEmd {๐“• : FieldSpecification} {ฯ†s : List ๐“•.FieldOp} {ฯ†sฮ› : WickContraction ฯ†s.length} {S : Finset (Finset (Fin ฯ†s.length))} {hs : S โŠ† โ†‘ฯ†sฮ›} (a : { x : Finset (Fin (subContraction S hs).uncontractedListGet.length) // x โˆˆ โ†‘(quotContraction S hs) }) :
      uncontractedListEmd ((quotContraction S hs).sndFieldOfContract a) = ฯ†sฮ›.sndFieldOfContract โŸจFinset.map uncontractedListEmd โ†‘a, โ‹ฏโŸฉ
      source
      theorem WickContraction.quotContraction_gradingCompliant {๐“• : FieldSpecification} {ฯ†s : List ๐“•.FieldOp} {ฯ†sฮ› : WickContraction ฯ†s.length} {S : Finset (Finset (Fin ฯ†s.length))} {hs : S โŠ† โ†‘ฯ†sฮ›} (hsฮ› : GradingCompliant ฯ†s ฯ†sฮ›) :
      GradingCompliant (subContraction S hs).uncontractedListGet (quotContraction S hs)
      source
      theorem WickContraction.mem_quotContraction_iff {๐“• : FieldSpecification} {ฯ†s : List ๐“•.FieldOp} {ฯ†sฮ› : WickContraction ฯ†s.length} {S : Finset (Finset (Fin ฯ†s.length))} {hs : S โŠ† โ†‘ฯ†sฮ›} {a : Finset (Fin (subContraction S hs).uncontractedListGet.length)} :
      a โˆˆ โ†‘(quotContraction S hs) โ†” Finset.map uncontractedListEmd a โˆˆ โ†‘ฯ†sฮ› โˆง Finset.map uncontractedListEmd a โˆ‰ โ†‘(subContraction S hs)