Sign associated with joining two Wick contractions #
theorem
WickContraction.stat_signFinset_right
{𝓕 : FieldSpecification}
{φs : List 𝓕.FieldOp}
(φsΛ : WickContraction φs.length)
(φsucΛ : WickContraction φsΛ.uncontractedListGet.length)
(i j : Fin φsΛ.uncontractedListGet.length)
:
FieldStatistic.ofFinset 𝓕.fieldOpStatistic φsΛ.uncontractedListGet.get (φsucΛ.signFinset i j) = FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get (Finset.map uncontractedListEmd (φsucΛ.signFinset i j))
theorem
WickContraction.signFinset_right_map_uncontractedListEmd_eq_filter
{𝓕 : FieldSpecification}
{φs : List 𝓕.FieldOp}
(φsΛ : WickContraction φs.length)
(φsucΛ : WickContraction φsΛ.uncontractedListGet.length)
(i j : Fin φsΛ.uncontractedListGet.length)
:
Finset.map uncontractedListEmd (φsucΛ.signFinset i j) = Finset.filter (fun (c : Fin φs.length) => c ∈ φsΛ.uncontracted)
((φsΛ.join φsucΛ).signFinset (uncontractedListEmd i) (uncontractedListEmd j))
theorem
WickContraction.sign_right_eq_prod_mul_prod
{𝓕 : FieldSpecification}
{φs : List 𝓕.FieldOp}
(φsΛ : WickContraction φs.length)
(φsucΛ : WickContraction φsΛ.uncontractedListGet.length)
:
sign φsΛ.uncontractedListGet φsucΛ = (∏ a : { x : Finset (Fin φsΛ.uncontractedListGet.length) // x ∈ ↑φsucΛ },
(FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φsΛ.uncontractedListGet[φsucΛ.sndFieldOfContract a]))
(FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get
(Finset.filter (fun (c : Fin φs.length) => c ∉ φsΛ.uncontracted)
((φsΛ.join φsucΛ).signFinset (uncontractedListEmd (φsucΛ.fstFieldOfContract a))
(uncontractedListEmd (φsucΛ.sndFieldOfContract a)))))) * ∏ a : { x : Finset (Fin φsΛ.uncontractedListGet.length) // x ∈ ↑φsucΛ },
(FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φsΛ.uncontractedListGet[φsucΛ.sndFieldOfContract a]))
(FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get
((φsΛ.join φsucΛ).signFinset (uncontractedListEmd (φsucΛ.fstFieldOfContract a))
(uncontractedListEmd (φsucΛ.sndFieldOfContract a))))
theorem
WickContraction.join_singleton_signFinset_eq_filter
{𝓕 : FieldSpecification}
{φs : List 𝓕.FieldOp}
{i j : Fin φs.length}
(h : i < j)
(φsucΛ : WickContraction (singleton h).uncontractedListGet.length)
:
theorem
WickContraction.join_singleton_left_signFinset_eq_filter
{𝓕 : FieldSpecification}
{φs : List 𝓕.FieldOp}
{i j : Fin φs.length}
(h : i < j)
(φsucΛ : WickContraction (singleton h).uncontractedListGet.length)
:
FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get ((singleton h).signFinset i j) = FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get (((singleton h).join φsucΛ).signFinset i j) * FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get
(Finset.filter
(fun (c : Fin φs.length) =>
(((singleton h).join φsucΛ).getDual? c).isSome = true ∧ ∀ (h1 : (((singleton h).join φsucΛ).getDual? c).isSome = true),
(((singleton h).join φsucΛ).getDual? c).get h1 < i)
((singleton h).signFinset i j))
def
WickContraction.joinSignRightExtra
{𝓕 : FieldSpecification}
{φs : List 𝓕.FieldOp}
{i j : Fin φs.length}
(h : i < j)
(φsucΛ : WickContraction (singleton h).uncontractedListGet.length)
:
The difference in sign between φsucΛ.sign and the direct contribution of φsucΛ to
(join (singleton h) φsucΛ).
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
WickContraction.joinSignLeftExtra
{𝓕 : FieldSpecification}
{φs : List 𝓕.FieldOp}
{i j : Fin φs.length}
(h : i < j)
(φsucΛ : WickContraction (singleton h).uncontractedListGet.length)
:
The difference in sign between (singleton h).sign and the direct contribution of
(singleton h) to (join (singleton h) φsucΛ).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
WickContraction.join_singleton_sign_left
{𝓕 : FieldSpecification}
{φs : List 𝓕.FieldOp}
{i j : Fin φs.length}
(h : i < j)
(φsucΛ : WickContraction (singleton h).uncontractedListGet.length)
:
sign φs (singleton h) = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φs[j]))
(FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get (((singleton h).join φsucΛ).signFinset i j)) * joinSignLeftExtra h φsucΛ
theorem
WickContraction.join_singleton_sign_right
{𝓕 : FieldSpecification}
{φs : List 𝓕.FieldOp}
{i j : Fin φs.length}
(h : i < j)
(φsucΛ : WickContraction (singleton h).uncontractedListGet.length)
:
sign (singleton h).uncontractedListGet φsucΛ = joinSignRightExtra h φsucΛ * ∏ a : { x : Finset (Fin (singleton h).uncontractedListGet.length) // x ∈ ↑φsucΛ },
(FieldStatistic.exchangeSign (𝓕.fieldOpStatistic (singleton h).uncontractedListGet[φsucΛ.sndFieldOfContract a]))
(FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get
(((singleton h).join φsucΛ).signFinset (uncontractedListEmd (φsucΛ.fstFieldOfContract a))
(uncontractedListEmd (φsucΛ.sndFieldOfContract a))))
theorem
WickContraction.joinSignRightExtra_eq_i_j_finset_eq_if
{𝓕 : FieldSpecification}
{φs : List 𝓕.FieldOp}
{i j : Fin φs.length}
(h : i < j)
(φsucΛ : WickContraction (singleton h).uncontractedListGet.length)
:
joinSignRightExtra h φsucΛ = ∏ a : { x : Finset (Fin (singleton h).uncontractedListGet.length) // x ∈ ↑φsucΛ },
(FieldStatistic.exchangeSign (𝓕.fieldOpStatistic (singleton h).uncontractedListGet[φsucΛ.sndFieldOfContract a]))
(FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get
((if uncontractedListEmd (φsucΛ.fstFieldOfContract a) < j ∧ j < uncontractedListEmd (φsucΛ.sndFieldOfContract a) ∧ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < i then
{j}
else ∅) ∪ if uncontractedListEmd (φsucΛ.fstFieldOfContract a) < i ∧ i < uncontractedListEmd (φsucΛ.sndFieldOfContract a) then
{i}
else ∅))
theorem
WickContraction.joinSignLeftExtra_eq_joinSignRightExtra
{𝓕 : FieldSpecification}
{φs : List 𝓕.FieldOp}
{i j : Fin φs.length}
(h : i < j)
(hs : 𝓕.fieldOpStatistic φs[i] = 𝓕.fieldOpStatistic φs[j])
(φsucΛ : WickContraction (singleton h).uncontractedListGet.length)
:
theorem
WickContraction.join_sign_singleton
{𝓕 : FieldSpecification}
{φs : List 𝓕.FieldOp}
{i j : Fin φs.length}
(h : i < j)
(hs : 𝓕.fieldOpStatistic φs[i] = 𝓕.fieldOpStatistic φs[j])
(φsucΛ : WickContraction (singleton h).uncontractedListGet.length)
:
theorem
WickContraction.join_sign_induction
{𝓕 : FieldSpecification}
{φs : List 𝓕.FieldOp}
(φsΛ : WickContraction φs.length)
(φsucΛ : WickContraction φsΛ.uncontractedListGet.length)
(hc : GradingCompliant φs φsΛ)
(n : ℕ)
(hn : (↑φsΛ).card = n)
:
theorem
WickContraction.join_sign
{𝓕 : FieldSpecification}
{φs : List 𝓕.FieldOp}
(φsΛ : WickContraction φs.length)
(φsucΛ : WickContraction φsΛ.uncontractedListGet.length)
(hc : GradingCompliant φs φsΛ)
:
For a list φs of 𝓕.FieldOp, a grading compliant Wick contraction φsΛ of φs,
and a Wick contraction φsucΛ of [φsΛ]ᵘᶜ, the following relation holds
(join φsΛ φsucΛ).sign = φsΛ.sign * φsucΛ.sign.
In φsΛ.sign the sign is determined by starting with the contracted pair
whose first element occurs at the left-most position. This lemma manifests that this
choice does not matter, and that contracted pairs can be brought together in any order.
theorem
WickContraction.join_sign_timeContract
{𝓕 : FieldSpecification}
{φs : List 𝓕.FieldOp}
(φsΛ : WickContraction φs.length)
(φsucΛ : WickContraction φsΛ.uncontractedListGet.length)
:
sign φs (φsΛ.join φsucΛ) • ↑(φsΛ.join φsucΛ).timeContract = sign φs φsΛ • ↑φsΛ.timeContract * sign φsΛ.uncontractedListGet φsucΛ • ↑φsucΛ.timeContract
For a list φs of 𝓕.FieldOp, a Wick contraction φsΛ of φs,
and a Wick contraction φsucΛ of [φsΛ]ᵘᶜ,
(join φsΛ φsucΛ).sign • (join φsΛ φsucΛ).timeContract is equal to the product of
φsΛ.sign • φsΛ.timeContractandφsucΛ.sign • φsucΛ.timeContract.