PhysLean Documentation

PhysLean.QFT.PerturbationTheory.WickContraction.Sign.InsertNone

Sign on inserting and not contracting #

source
theorem WickContraction.signFinset_insertAndContract_none {๐“• : FieldSpecification} (ฯ† : ๐“•.FieldOp) (ฯ†s : List ๐“•.FieldOp) (ฯ†sฮ› : WickContraction ฯ†s.length) (i : Fin ฯ†s.length.succ) (i1 i2 : Fin ฯ†s.length) :
(insertAndContract ฯ† ฯ†sฮ› i none).signFinset ((finCongr โ‹ฏ) (i.succAbove i1)) ((finCongr โ‹ฏ) (i.succAbove i2)) = if i.succAbove i1 < i โˆง i < i.succAbove i2 then insert ((finCongr โ‹ฏ) i) (insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)) else insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)
source
def WickContraction.signInsertNone {๐“• : FieldSpecification} (ฯ† : ๐“•.FieldOp) (ฯ†s : List ๐“•.FieldOp) (ฯ†sฮ› : WickContraction ฯ†s.length) (i : Fin ฯ†s.length.succ) :
โ„‚

Given a Wick contraction ฯ†sฮ› associated with a list of states ฯ†s and an i : Fin ฯ†s.length.succ, the change in sign of the contraction associated with inserting ฯ† into ฯ†s at position i without contracting it.

For each contracted pair {a1, a2} in ฯ†sฮ› if a1 < a2 such that i is within the range a1 < i < a2 we pick up a sign equal to ๐“ข(ฯ†, ฯ†s[a2]).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem WickContraction.sign_insert_none_eq_signInsertNone_mul_sign {๐“• : FieldSpecification} (ฯ† : ๐“•.FieldOp) (ฯ†s : List ๐“•.FieldOp) (ฯ†sฮ› : WickContraction ฯ†s.length) (i : Fin ฯ†s.length.succ) :
    sign (List.insertIdx (โ†‘i) ฯ† ฯ†s) (insertAndContract ฯ† ฯ†sฮ› i none) = signInsertNone ฯ† ฯ†s ฯ†sฮ› i * sign ฯ†s ฯ†sฮ›
    source
    theorem WickContraction.signInsertNone_eq_mul_fst_snd {๐“• : FieldSpecification} (ฯ† : ๐“•.FieldOp) (ฯ†s : List ๐“•.FieldOp) (ฯ†sฮ› : WickContraction ฯ†s.length) (i : Fin ฯ†s.length.succ) :
    signInsertNone ฯ† ฯ†s ฯ†sฮ› i = โˆ a : { x : Finset (Fin ฯ†s.length) // x โˆˆ โ†‘ฯ†sฮ› }, (if i.succAbove (ฯ†sฮ›.fstFieldOfContract a) < i then (FieldStatistic.exchangeSign (๐“•.fieldOpStatistic ฯ†)) (๐“•.fieldOpStatistic ฯ†s[ฯ†sฮ›.sndFieldOfContract a]) else 1) * if i.succAbove (ฯ†sฮ›.sndFieldOfContract a) < i then (FieldStatistic.exchangeSign (๐“•.fieldOpStatistic ฯ†)) (๐“•.fieldOpStatistic ฯ†s[ฯ†sฮ›.sndFieldOfContract a]) else 1
    source
    theorem WickContraction.signInsertNone_eq_prod_prod {๐“• : FieldSpecification} (ฯ† : ๐“•.FieldOp) (ฯ†s : List ๐“•.FieldOp) (ฯ†sฮ› : WickContraction ฯ†s.length) (i : Fin ฯ†s.length.succ) (hG : GradingCompliant ฯ†s ฯ†sฮ›) :
    signInsertNone ฯ† ฯ†s ฯ†sฮ› i = โˆ a : { x : Finset (Fin ฯ†s.length) // x โˆˆ โ†‘ฯ†sฮ› }, โˆ x : { x : Fin ฯ†s.length // x โˆˆ โ†‘a }, if i.succAbove โ†‘x < i then (FieldStatistic.exchangeSign (๐“•.fieldOpStatistic ฯ†)) (๐“•.fieldOpStatistic ฯ†s[โ†‘x]) else 1
    source
    theorem WickContraction.signInsertNone_eq_prod_getDual?_Some {๐“• : FieldSpecification} (ฯ† : ๐“•.FieldOp) (ฯ†s : List ๐“•.FieldOp) (ฯ†sฮ› : WickContraction ฯ†s.length) (i : Fin ฯ†s.length.succ) (hG : GradingCompliant ฯ†s ฯ†sฮ›) :
    signInsertNone ฯ† ฯ†s ฯ†sฮ› i = โˆ x : Fin ฯ†s.length, if (ฯ†sฮ›.getDual? x).isSome = true then if i.succAbove x < i then (FieldStatistic.exchangeSign (๐“•.fieldOpStatistic ฯ†)) (๐“•.fieldOpStatistic ฯ†s[โ†‘x]) else 1 else 1
    source
    theorem WickContraction.signInsertNone_eq_filter_map {๐“• : FieldSpecification} (ฯ† : ๐“•.FieldOp) (ฯ†s : List ๐“•.FieldOp) (ฯ†sฮ› : WickContraction ฯ†s.length) (i : Fin ฯ†s.length.succ) (hG : GradingCompliant ฯ†s ฯ†sฮ›) :
    signInsertNone ฯ† ฯ†s ฯ†sฮ› i = (FieldStatistic.exchangeSign (๐“•.fieldOpStatistic ฯ†)) (FieldStatistic.ofList ๐“•.fieldOpStatistic (List.map ฯ†s.get (List.filter (fun (x : Fin ฯ†s.length) => decide ((ฯ†sฮ›.getDual? x).isSome = true โˆง i.succAbove x < i)) (List.finRange ฯ†s.length))))
    source
    theorem WickContraction.signInsertNone_eq_filterset {๐“• : FieldSpecification} (ฯ† : ๐“•.FieldOp) (ฯ†s : List ๐“•.FieldOp) (ฯ†sฮ› : WickContraction ฯ†s.length) (i : Fin ฯ†s.length.succ) (hG : GradingCompliant ฯ†s ฯ†sฮ›) :
    signInsertNone ฯ† ฯ†s ฯ†sฮ› i = (FieldStatistic.exchangeSign (๐“•.fieldOpStatistic ฯ†)) (FieldStatistic.ofFinset ๐“•.fieldOpStatistic ฯ†s.get (Finset.filter (fun (x : Fin ฯ†s.length) => (ฯ†sฮ›.getDual? x).isSome = true โˆง i.succAbove x < i) Finset.univ))

    The following signs for a grading compliant Wick contraction are equal:

    • The sign ฯ†sฮ›.signInsertNone ฯ† ฯ†s i which is given by the following: For each contracted pair {a1, a2} in ฯ†sฮ› if a1 < a2 such that i is within the range a1 < i < a2 we pick up a sign equal to ๐“ข(ฯ†, ฯ†s[a2]).
    • The sign got by moving ฯ† through ฯ†โ‚€โ€ฆฯ†แตขโ‚‹โ‚ and only picking up a sign when ฯ†แตข has a dual. These are equal since: Both ignore uncontracted fields, and for a contracted pair {a1, a2} with a1 < a2
    • if i < a1 < a2 then we don't pick up a sign from either ฯ†โ‚โ‚ or ฯ†โ‚โ‚‚.
    • if a1 < i < a2 then we pick up a sign from ฯ†โ‚โ‚ cases which is equal to ๐“ข(ฯ†, ฯ†s[a2]) (since ฯ†sฮ› is grading compliant).
    • if a1 < a2 < i then we pick up a sign from both ฯ†โ‚โ‚ and ฯ†โ‚โ‚‚ which cancel each other out.
    source
    theorem WickContraction.sign_insert_none {๐“• : FieldSpecification} (ฯ† : ๐“•.FieldOp) (ฯ†s : List ๐“•.FieldOp) (ฯ†sฮ› : WickContraction ฯ†s.length) (i : Fin ฯ†s.length.succ) (hG : GradingCompliant ฯ†s ฯ†sฮ›) :
    sign (List.insertIdx (โ†‘i) ฯ† ฯ†s) (insertAndContract ฯ† ฯ†sฮ› i none) = (FieldStatistic.exchangeSign (๐“•.fieldOpStatistic ฯ†)) (FieldStatistic.ofFinset ๐“•.fieldOpStatistic ฯ†s.get (Finset.filter (fun (x : Fin ฯ†s.length) => (ฯ†sฮ›.getDual? x).isSome = true โˆง i.succAbove x < i) Finset.univ)) * sign ฯ†s ฯ†sฮ›

    For a list ฯ†s = ฯ†โ‚€โ€ฆฯ†โ‚™ of ๐“•.FieldOp, a graded compliant Wick contraction ฯ†sฮ› of ฯ†s, an i โ‰ค ฯ†s.length, and a ฯ† in ๐“•.FieldOp, then (ฯ†sฮ› โ†ฉฮ› ฯ† i none).sign = s * ฯ†sฮ›.sign where s is the sign arrived at by moving ฯ† through the elements of ฯ†โ‚€โ€ฆฯ†แตขโ‚‹โ‚ which are contracted with some element.

    The proof of this result involves a careful consideration of the contributions of different FieldOps in ฯ†s to the sign of ฯ†sฮ› โ†ฉฮ› ฯ† i none.

    source
    theorem WickContraction.sign_insert_none_zero {๐“• : FieldSpecification} (ฯ† : ๐“•.FieldOp) (ฯ†s : List ๐“•.FieldOp) (ฯ†sฮ› : WickContraction ฯ†s.length) :
    sign (List.insertIdx (โ†‘0) ฯ† ฯ†s) (insertAndContract ฯ† ฯ†sฮ› 0 none) = sign ฯ†s ฯ†sฮ›

    For a list ฯ†s = ฯ†โ‚€โ€ฆฯ†โ‚™ of ๐“•.FieldOp, a graded compliant Wick contraction ฯ†sฮ› of ฯ†s, and a ฯ† in ๐“•.FieldOp, then (ฯ†sฮ› โ†ฉฮ› ฯ† 0 none).sign = ฯ†sฮ›.sign.

    This is a direct corollary of sign_insert_none.