Time contractions

def WickContraction.EqTimeOnly {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : Prop

The condition on a Wick contraction which is true iff and only if every contraction is between two fields of equal time.

Equations

• φsΛ.EqTimeOnly = ∀ (i j : Fin φs.length), {i, j} ∈ ↑φsΛ → FieldSpecification.timeOrderRel φs[i] φs[j]

instance WickContraction.instDecidableEqTimeOnly {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : Decidable φsΛ.EqTimeOnly

Equations

• φsΛ.instDecidableEqTimeOnly = inferInstanceAs (Decidable (∀ (i j : Fin φs.length), {i, j} ∈ ↑φsΛ → FieldSpecification.timeOrderRel φs[i] φs[j]))

theorem WickContraction.EqTimeOnly.timeOrderRel_of_eqTimeOnly_pair {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) {i j : Fin φs.length} (h : {i, j} ∈ ↑φsΛ) (hc : φsΛ.EqTimeOnly) : FieldSpecification.timeOrderRel φs[i] φs[j]

theorem WickContraction.EqTimeOnly.timeOrderRel_both_of_eqTimeOnly {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) {i j : Fin φs.length} (h : {i, j} ∈ ↑φsΛ) (hc : φsΛ.EqTimeOnly) : FieldSpecification.timeOrderRel φs[i] φs[j] ∧ FieldSpecification.timeOrderRel φs[j] φs[i]

theorem WickContraction.EqTimeOnly.eqTimeOnly_iff_forall_finset {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : φsΛ.EqTimeOnly ↔ ∀ (a : { x : Finset (Fin φs.length) // x ∈ ↑φsΛ }), FieldSpecification.timeOrderRel φs[φsΛ.fstFieldOfContract a] φs[φsΛ.sndFieldOfContract a] ∧ FieldSpecification.timeOrderRel φs[φsΛ.sndFieldOfContract a] φs[φsΛ.fstFieldOfContract a]

@[simp]

theorem WickContraction.EqTimeOnly.empty_mem {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} : empty.EqTimeOnly

theorem WickContraction.EqTimeOnly.staticContract_eq_timeContract_of_eqTimeOnly {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (h : φsΛ.EqTimeOnly) : φsΛ.staticContract = φsΛ.timeContract

Let φs be a list of 𝓕.FieldOp and φsΛ a WickContraction of φs within which every contraction involves two 𝓕.FieldOps that have the same time, then φsΛ.staticContract = φsΛ.timeContract.

theorem WickContraction.EqTimeOnly.eqTimeOnly_congr {𝓕 : FieldSpecification} {φs φs' : List 𝓕.FieldOp} (h : φs = φs') (φsΛ : WickContraction φs.length) : ((congr ⋯) φsΛ).EqTimeOnly ↔ φsΛ.EqTimeOnly

theorem WickContraction.EqTimeOnly.quotContraction_eqTimeOnly {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} (h : φsΛ.EqTimeOnly) (S : Finset (Finset (Fin φs.length))) (ha : S ⊆ ↑φsΛ) : (quotContraction S ha).EqTimeOnly

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

theorem WickContraction.EqTimeOnly.timeOrder_timeContract_mul_of_eqTimeOnly_mid_induction {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (hl : φsΛ.EqTimeOnly) (a b : 𝓕.FieldOpAlgebra) (n : ℕ) (hn : (↑φsΛ).card = n) : FieldSpecification.FieldOpAlgebra.timeOrder (a * ↑φsΛ.timeContract * b) = ↑φsΛ.timeContract * FieldSpecification.FieldOpAlgebra.timeOrder (a * b)

theorem WickContraction.EqTimeOnly.timeOrder_timeContract_mul_of_eqTimeOnly_mid {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (hl : φsΛ.EqTimeOnly) (a b : 𝓕.FieldOpAlgebra) : FieldSpecification.FieldOpAlgebra.timeOrder (a * ↑φsΛ.timeContract * b) = ↑φsΛ.timeContract * FieldSpecification.FieldOpAlgebra.timeOrder (a * b)

theorem WickContraction.EqTimeOnly.timeOrder_timeContract_mul_of_eqTimeOnly_left {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (hl : φsΛ.EqTimeOnly) (b : 𝓕.FieldOpAlgebra) : FieldSpecification.FieldOpAlgebra.timeOrder (↑φsΛ.timeContract * b) = ↑φsΛ.timeContract * FieldSpecification.FieldOpAlgebra.timeOrder b

Let φs be a list of 𝓕.FieldOp, φsΛ a WickContraction of φs within which every contraction involves two 𝓕.FieldOps that have the same time and b a general element in 𝓕.FieldOpAlgebra. Then 𝓣(φsΛ.timeContract.1 * b) = φsΛ.timeContract.1 * 𝓣(b).

This follows from properties of orderings and the ideal defining 𝓕.FieldOpAlgebra.

theorem WickContraction.EqTimeOnly.exists_join_singleton_of_not_eqTimeOnly {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (h1 : ¬φsΛ.EqTimeOnly) : ∃ (i : Fin φs.length) (j : Fin φs.length) (h : i < j) (φsucΛ : WickContraction (singleton h).uncontractedListGet.length), φsΛ = (singleton h).join φsucΛ ∧ (¬FieldSpecification.timeOrderRel φs[i] φs[j] ∨ ¬FieldSpecification.timeOrderRel φs[j] φs[i])

theorem WickContraction.EqTimeOnly.timeOrder_timeContract_of_not_eqTimeOnly {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (hl : ¬φsΛ.EqTimeOnly) : FieldSpecification.FieldOpAlgebra.timeOrder ↑φsΛ.timeContract = 0

theorem WickContraction.EqTimeOnly.timeOrder_staticContract_of_not_mem {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (hl : ¬φsΛ.EqTimeOnly) : FieldSpecification.FieldOpAlgebra.timeOrder ↑φsΛ.staticContract = 0

Let φs be a list of 𝓕.FieldOp and φsΛ a WickContraction with at least one contraction between 𝓕.FieldOp that do not have the same time. Then 𝓣(φsΛ.staticContract.1) = 0.

def WickContraction.HaveEqTime {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : Prop

The condition on a Wick contraction which is true if it has at least one contraction which is between two equal time fields.

Equations

• φsΛ.HaveEqTime = ∃ (i : Fin φs.length) (j : Fin φs.length) (_ : {i, j} ∈ ↑φsΛ), FieldSpecification.timeOrderRel φs[i] φs[j] ∧ FieldSpecification.timeOrderRel φs[j] φs[i]

noncomputable instance WickContraction.instDecidableHaveEqTime {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : Decidable φsΛ.HaveEqTime

Equations

• One or more equations did not get rendered due to their size.

theorem WickContraction.haveEqTime_iff_finset {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : φsΛ.HaveEqTime ↔ ∃ (a : Finset (Fin φs.length)) (h : a ∈ ↑φsΛ), FieldSpecification.timeOrderRel φs[φsΛ.fstFieldOfContract ⟨a, h⟩] φs[φsΛ.sndFieldOfContract ⟨a, h⟩] ∧ FieldSpecification.timeOrderRel φs[φsΛ.sndFieldOfContract ⟨a, h⟩] φs[φsΛ.fstFieldOfContract ⟨a, h⟩]

@[simp]

theorem WickContraction.empty_not_haveEqTime {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} : ¬empty.HaveEqTime

def WickContraction.eqTimeContractSet {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : Finset (Finset (Fin φs.length))

Given a Wick contraction the subset of contracted pairs between equal time fields.

Equations

• One or more equations did not get rendered due to their size.

theorem WickContraction.eqTimeContractSet_subset {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : φsΛ.eqTimeContractSet ⊆ ↑φsΛ

theorem WickContraction.mem_of_mem_eqTimeContractSet {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {a : Finset (Fin φs.length)} (h : a ∈ φsΛ.eqTimeContractSet) : a ∈ ↑φsΛ

theorem WickContraction.join_eqTimeContractSet {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) : (φsΛ.join φsucΛ).eqTimeContractSet = φsΛ.eqTimeContractSet ∪ Finset.map (Finset.mapEmbedding uncontractedListEmd).toEmbedding φsucΛ.eqTimeContractSet

theorem WickContraction.eqTimeContractSet_of_not_haveEqTime {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} (h : ¬φsΛ.HaveEqTime) : φsΛ.eqTimeContractSet = ∅

theorem WickContraction.eqTimeContractSet_of_mem_eqTimeOnly {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} (h : φsΛ.EqTimeOnly) : φsΛ.eqTimeContractSet = ↑φsΛ

theorem WickContraction.subContraction_eqTimeContractSet_eqTimeOnly {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : (subContraction φsΛ.eqTimeContractSet ⋯).EqTimeOnly

theorem WickContraction.pair_mem_eqTimeContractSet_iff {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (φsΛ : WickContraction φs.length) (h : {i, j} ∈ ↑φsΛ) : {i, j} ∈ φsΛ.eqTimeContractSet ↔ FieldSpecification.timeOrderRel φs[i] φs[j] ∧ FieldSpecification.timeOrderRel φs[j] φs[i]

theorem WickContraction.subContraction_eqTimeContractSet_not_empty_of_haveEqTime {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (h : φsΛ.HaveEqTime) : subContraction φsΛ.eqTimeContractSet ⋯ ≠ empty

theorem WickContraction.quotContraction_eqTimeContractSet_not_haveEqTime {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : ¬(quotContraction φsΛ.eqTimeContractSet ⋯).HaveEqTime

theorem WickContraction.join_haveEqTime_of_eqTimeOnly_nonEmpty {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (h1 : φsΛ.EqTimeOnly) (h2 : φsΛ ≠ empty) (φsucΛ : WickContraction φsΛ.uncontractedListGet.length) : (φsΛ.join φsucΛ).HaveEqTime

theorem WickContraction.hasEqTimeEquiv_ext_sigma {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} {x1 x2 : (φsΛ : { φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly ∧ φsΛ ≠ empty }) × { φssucΛ : WickContraction (↑φsΛ).uncontractedListGet.length // ¬φssucΛ.HaveEqTime }} (h1 : ↑x1.fst = ↑x2.fst) (h2 : ↑x1.snd = (congr ⋯) ↑x2.snd) : x1 = x2

def WickContraction.hasEqTimeEquiv {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) : { φsΛ : WickContraction φs.length // φsΛ.HaveEqTime } ≃ (φsΛ : { φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly ∧ φsΛ ≠ empty }) × { φssucΛ : WickContraction (↑φsΛ).uncontractedListGet.length // ¬φssucΛ.HaveEqTime }

The equivalence which separates a Wick contraction which has an equal time contraction into a non-empty contraction only between equal-time fields and a Wick contraction which does not have equal time contractions.

Equations

• One or more equations did not get rendered due to their size.

theorem WickContraction.sum_haveEqTime {𝓕 : FieldSpecification} {M : Type u_1} (φs : List 𝓕.FieldOp) (f : WickContraction φs.length → M) [AddCommMonoid M] : ∑ φsΛ : { φsΛ : WickContraction φs.length // φsΛ.HaveEqTime }, f ↑φsΛ = ∑ φsΛ : { φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly ∧ φsΛ ≠ empty }, ∑ φssucΛ : { φssucΛ : WickContraction (↑φsΛ).uncontractedListGet.length // ¬φssucΛ.HaveEqTime }, f ((↑φsΛ).join ↑φssucΛ)