Join of contractions

def WickContraction.join {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) : WickContraction φs.length

Given a list φs of 𝓕.FieldOp, a Wick contraction φsΛ of φs and a Wick contraction φsucΛ of [φsΛ]ᵘᶜ, join φsΛ φsucΛ is defined as the Wick contraction of φs consisting of the contractions in φsΛ and those in φsucΛ.

As an example, for φs = [φ1, φ2, φ3, φ4], φsΛ = {{0, 1}} corresponding to the contraction of φ1 and φ2 in φs and φsucΛ = {{0, 1}} corresponding to the contraction of φ3 and φ4 in [φsΛ]ᵘᶜ = [φ3, φ4], then join φsΛ φsucΛ is the contraction {{0, 1}, {2, 3}} of φs.

Equations

• φsΛ.join φsucΛ = ⟨↑φsΛ ∪ Finset.map (Finset.mapEmbedding WickContraction.uncontractedListEmd).toEmbedding ↑φsucΛ, ⋯⟩

theorem WickContraction.join_congr {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction φsΛ.uncontractedListGet.length} {φsΛ' : WickContraction φs.length} (h1 : φsΛ = φsΛ') : φsΛ.join φsucΛ = φsΛ'.join ((congr ⋯) φsucΛ)

def WickContraction.joinLiftLeft {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction φsΛ.uncontractedListGet.length} : { x : Finset (Fin φs.length) // x ∈ ↑φsΛ } → { x : Finset (Fin φs.length) // x ∈ ↑(φsΛ.join φsucΛ) }

Given a contracting pair within φsΛ the corresponding contracting pair within (join φsΛ φsucΛ).

Equations

• WickContraction.joinLiftLeft a = ⟨↑a, ⋯⟩

theorem WickContraction.jointLiftLeft_injective {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction φsΛ.uncontractedListGet.length} : Function.Injective joinLiftLeft

def WickContraction.joinLiftRight {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction φsΛ.uncontractedListGet.length} : { x : Finset (Fin φsΛ.uncontractedListGet.length) // x ∈ ↑φsucΛ } → { x : Finset (Fin φs.length) // x ∈ ↑(φsΛ.join φsucΛ) }

Given a contracting pair within φsucΛ the corresponding contracting pair within (join φsΛ φsucΛ).

Equations

• WickContraction.joinLiftRight a = ⟨Finset.map WickContraction.uncontractedListEmd ↑a, ⋯⟩

theorem WickContraction.joinLiftRight_injective {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction φsΛ.uncontractedListGet.length} : Function.Injective joinLiftRight

theorem WickContraction.jointLiftLeft_disjoint_joinLiftRight {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction φsΛ.uncontractedListGet.length} (a : { x : Finset (Fin φs.length) // x ∈ ↑φsΛ }) (b : { x : Finset (Fin φsΛ.uncontractedListGet.length) // x ∈ ↑φsucΛ }) : Disjoint ↑(joinLiftLeft a) ↑(joinLiftRight b)

theorem WickContraction.jointLiftLeft_neq_joinLiftRight {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction φsΛ.uncontractedListGet.length} (a : { x : Finset (Fin φs.length) // x ∈ ↑φsΛ }) (b : { x : Finset (Fin φsΛ.uncontractedListGet.length) // x ∈ ↑φsucΛ }) : joinLiftLeft a ≠ joinLiftRight b

def WickContraction.joinLift {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction φsΛ.uncontractedListGet.length} : { x : Finset (Fin φs.length) // x ∈ ↑φsΛ } ⊕ { x : Finset (Fin φsΛ.uncontractedListGet.length) // x ∈ ↑φsucΛ } → { x : Finset (Fin φs.length) // x ∈ ↑(φsΛ.join φsucΛ) }

The map from contracted pairs of φsΛ and φsucΛ to contracted pairs in (join φsΛ φsucΛ).

Equations

• WickContraction.joinLift (Sum.inl a_2) = WickContraction.joinLiftLeft a_2
• WickContraction.joinLift (Sum.inr a_2) = WickContraction.joinLiftRight a_2

theorem WickContraction.joinLift_injective {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction φsΛ.uncontractedListGet.length} : Function.Injective joinLift

theorem WickContraction.joinLift_surjective {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction φsΛ.uncontractedListGet.length} : Function.Surjective joinLift

theorem WickContraction.joinLift_bijective {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction φsΛ.uncontractedListGet.length} : Function.Bijective joinLift

theorem WickContraction.prod_join {𝓕 : FieldSpecification} {M : Type u_1} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) (f : { x : Finset (Fin φs.length) // x ∈ ↑(φsΛ.join φsucΛ) } → M) [CommMonoid M] : ∏ a : { x : Finset (Fin φs.length) // x ∈ ↑(φsΛ.join φsucΛ) }, f a = (∏ a : { x : Finset (Fin φs.length) // x ∈ ↑φsΛ }, f (joinLiftLeft a)) * ∏ a : { x : Finset (Fin φsΛ.uncontractedListGet.length) // x ∈ ↑φsucΛ }, f (joinLiftRight a)

theorem WickContraction.joinLiftLeft_or_joinLiftRight_of_mem_join {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) {a : Finset (Fin φs.length)} (ha : a ∈ ↑(φsΛ.join φsucΛ)) : (∃ (b : { x : Finset (Fin φs.length) // x ∈ ↑φsΛ }), a = ↑(joinLiftLeft b)) ∨ ∃ (b : { x : Finset (Fin φsΛ.uncontractedListGet.length) // x ∈ ↑φsucΛ }), a = ↑(joinLiftRight b)

@[simp]

theorem WickContraction.join_fstFieldOfContract_joinLiftRight {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) (a : { x : Finset (Fin φsΛ.uncontractedListGet.length) // x ∈ ↑φsucΛ }) : (φsΛ.join φsucΛ).fstFieldOfContract (joinLiftRight a) = uncontractedListEmd (φsucΛ.fstFieldOfContract a)

@[simp]

theorem WickContraction.join_sndFieldOfContract_joinLiftRight {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) (a : { x : Finset (Fin φsΛ.uncontractedListGet.length) // x ∈ ↑φsucΛ }) : (φsΛ.join φsucΛ).sndFieldOfContract (joinLiftRight a) = uncontractedListEmd (φsucΛ.sndFieldOfContract a)

@[simp]

theorem WickContraction.join_fstFieldOfContract_joinLiftLeft {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) (a : { x : Finset (Fin φs.length) // x ∈ ↑φsΛ }) : (φsΛ.join φsucΛ).fstFieldOfContract (joinLiftLeft a) = φsΛ.fstFieldOfContract a

@[simp]

theorem WickContraction.join_sndFieldOfContract_joinLift {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) (a : { x : Finset (Fin φs.length) // x ∈ ↑φsΛ }) : (φsΛ.join φsucΛ).sndFieldOfContract (joinLiftLeft a) = φsΛ.sndFieldOfContract a

theorem WickContraction.mem_join_right_iff {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) (a : Finset (Fin φsΛ.uncontractedListGet.length)) : a ∈ ↑φsucΛ ↔ Finset.map uncontractedListEmd a ∈ ↑(φsΛ.join φsucΛ)

theorem WickContraction.join_card {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction φsΛ.uncontractedListGet.length} : (↑(φsΛ.join φsucΛ)).card = (↑φsΛ).card + (↑φsucΛ).card

@[simp]

theorem WickContraction.empty_join {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction empty.uncontractedListGet.length) : empty.join φsΛ = (congr ⋯) φsΛ

@[simp]

theorem WickContraction.join_empty {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : φsΛ.join empty = φsΛ

theorem WickContraction.join_timeContract {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) : (φsΛ.join φsucΛ).timeContract = φsΛ.timeContract * φsucΛ.timeContract

theorem WickContraction.join_staticContract {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) : (φsΛ.join φsucΛ).staticContract = φsΛ.staticContract * φsucΛ.staticContract

theorem WickContraction.mem_join_uncontracted_of_mem_right_uncontracted {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) (i : Fin φsΛ.uncontractedListGet.length) (ha : i ∈ φsucΛ.uncontracted) : uncontractedListEmd i ∈ (φsΛ.join φsucΛ).uncontracted

theorem WickContraction.exists_mem_left_uncontracted_of_mem_join_uncontracted {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) (i : Fin φs.length) (ha : i ∈ (φsΛ.join φsucΛ).uncontracted) : i ∈ φsΛ.uncontracted

theorem WickContraction.exists_mem_right_uncontracted_of_mem_join_uncontracted {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) (i : Fin φs.length) (hi : i ∈ (φsΛ.join φsucΛ).uncontracted) : ∃ (a : Fin φsΛ.uncontractedListGet.length), uncontractedListEmd a = i ∧ a ∈ φsucΛ.uncontracted

theorem WickContraction.join_uncontractedList {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) : (φsΛ.join φsucΛ).uncontractedList = List.map (⇑uncontractedListEmd) φsucΛ.uncontractedList

theorem WickContraction.join_uncontractedList_get {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) : (φsΛ.join φsucΛ).uncontractedList.get = ⇑uncontractedListEmd ∘ φsucΛ.uncontractedList.get ∘ Fin.cast ⋯

theorem WickContraction.join_uncontractedListGet {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) : (φsΛ.join φsucΛ).uncontractedListGet = φsucΛ.uncontractedListGet

theorem WickContraction.join_uncontractedListEmb {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) : uncontractedListEmd = ((finCongr ⋯).toEmbedding.trans uncontractedListEmd).trans uncontractedListEmd

theorem WickContraction.join_assoc {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) (φsucΛ' : WickContraction (φsΛ.join φsucΛ).uncontractedListGet.length) : (φsΛ.join φsucΛ).join φsucΛ' = φsΛ.join (φsucΛ.join ((congr ⋯) φsucΛ'))

theorem WickContraction.join_getDual?_apply_uncontractedListEmb_eq_none_iff {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) (i : Fin φsΛ.uncontractedListGet.length) : (φsΛ.join φsucΛ).getDual? (uncontractedListEmd i) = none ↔ φsucΛ.getDual? i = none

theorem WickContraction.join_getDual?_apply_uncontractedListEmb_isSome_iff {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) (i : Fin φsΛ.uncontractedListGet.length) : ((φsΛ.join φsucΛ).getDual? (uncontractedListEmd i)).isSome = true ↔ (φsucΛ.getDual? i).isSome = true

theorem WickContraction.join_getDual?_apply_uncontractedListEmb_some {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) (i : Fin φsΛ.uncontractedListGet.length) (hi : ((φsΛ.join φsucΛ).getDual? (uncontractedListEmd i)).isSome = true) : (φsΛ.join φsucΛ).getDual? (uncontractedListEmd i) = some (uncontractedListEmd ((φsucΛ.getDual? i).get ⋯))

@[simp]

theorem WickContraction.join_getDual?_apply_uncontractedListEmb {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) (i : Fin φsΛ.uncontractedListGet.length) : (φsΛ.join φsucΛ).getDual? (uncontractedListEmd i) = Option.map (⇑uncontractedListEmd) (φsucΛ.getDual? i)

Subcontractions and quotient contractions

theorem WickContraction.join_sub_quot {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (S : Finset (Finset (Fin φs.length))) (ha : S ⊆ ↑φsΛ) : (subContraction S ha).join (quotContraction S ha) = φsΛ

theorem WickContraction.subContraction_card_plus_quotContraction_card_eq {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (S : Finset (Finset (Fin φs.length))) (ha : S ⊆ ↑φsΛ) : (↑(subContraction S ha)).card + (↑(quotContraction S ha)).card = (↑φsΛ).card

@[simp]

theorem WickContraction.join_singleton_getDual?_left {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (h : i < j) (φsucΛ : WickContraction (singleton h).uncontractedListGet.length) : ((singleton h).join φsucΛ).getDual? i = some j

@[simp]

theorem WickContraction.join_singleton_getDual?_right {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (h : i < j) (φsucΛ : WickContraction (singleton h).uncontractedListGet.length) : ((singleton h).join φsucΛ).getDual? j = some i

theorem WickContraction.exists_contraction_pair_of_card_ge_zero {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (h : 0 < (↑φsΛ).card) : ∃ (a : Finset (Fin φs.length)), a ∈ ↑φsΛ

theorem WickContraction.exists_join_singleton_of_card_ge_zero {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (h : 0 < (↑φsΛ).card) (hc : GradingCompliant φs φsΛ) : ∃ (i : Fin φs.length) (j : Fin φs.length) (h : i < j) (φsucΛ : WickContraction (singleton h).uncontractedListGet.length), φsΛ = (singleton h).join φsucΛ ∧ 𝓕.fieldOpStatistic φs[i] = 𝓕.fieldOpStatistic φs[j] ∧ GradingCompliant (singleton h).uncontractedListGet φsucΛ ∧ (↑φsucΛ).card + 1 = (↑φsΛ).card

theorem WickContraction.join_not_gradingCompliant_of_left_not_gradingCompliant {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) (hc : ¬GradingCompliant φs φsΛ) : ¬GradingCompliant φs (φsΛ.join φsucΛ)