Time contractions

noncomputable def WickContraction.timeContract {𝓕 : FieldSpecification} {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : ↥(Subalgebra.center ℂ 𝓕.WickAlgebra)

For a list φs of 𝓕.FieldOp and a Wick contraction φsΛ the element of the center of 𝓕.WickAlgebra, φsΛ.timeContract is defined as the product of timeContract φs[j] φs[k] over contracted pairs {j, k} in φsΛ with j < k.

Equations

• φsΛ.timeContract = ∏ a : ↥↑φsΛ, ⟨FieldSpecification.WickAlgebra.timeContract (φs.get (φsΛ.fstFieldOfContract a)) (φs.get (φsΛ.sndFieldOfContract a)), ⋯⟩

@[simp]

theorem WickContraction.timeContract_insert_none {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) : (insertAndContract φ φsΛ i none).timeContract = φsΛ.timeContract

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp, and a i ≤ φs.length the following relation holds

(φsΛ ↩Λ φ i none).timeContract = φsΛ.timeContract

The proof of this result ultimately is a consequence of definitions.

theorem WickContraction.timeContract_insertAndContract_some {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : ↥φsΛ.uncontracted) : (insertAndContract φ φsΛ i (some j)).timeContract = (if i < i.succAbove ↑j then ⟨FieldSpecification.WickAlgebra.timeContract φ φs[↑j], ⋯⟩ else ⟨FieldSpecification.WickAlgebra.timeContract φs[↑j] φ, ⋯⟩) * φsΛ.timeContract

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp, a i ≤ φs.length and a k in φsΛ.uncontracted, then (φsΛ ↩Λ φ i (some k)).timeContract is equal to the product of

• timeContract φ φs[k] if i ≤ k or timeContract φs[k] φ if k < i
• φsΛ.timeContract.

The proof of this result ultimately is a consequence of definitions.

@[simp]

theorem WickContraction.timeContract_empty {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) : empty.timeContract = 1

theorem WickContraction.timeContract_insert_some_of_lt {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : ↥φsΛ.uncontracted) (ht : FieldSpecification.timeOrderRel φ φs[↑k]) (hik : i < i.succAbove ↑k) : ↑(insertAndContract φ φsΛ i (some k)).timeContract = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})) • (FieldSpecification.WickAlgebra.contractStateAtIndex φ φsΛ.uncontractedListGet ((uncontractedFieldOpEquiv φs φsΛ) (some k)) * ↑φsΛ.timeContract)

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp, a i ≤ φs.length and a k in φsΛ.uncontracted such that i ≤ k, with the condition that φ has greater or equal time to φs[k], then (φsΛ ↩Λ φ i (some k)).timeContract is equal to the product of

• [anPart φ, φs[k]]ₛ
• φsΛ.timeContract
• two copies of the exchange sign of φ with the uncontracted fields in φ₀…φₖ₋₁. These two exchange signs cancel each other out but are included for convenience.

The proof of this result ultimately is a consequence of definitions and timeContract_of_timeOrderRel.

theorem WickContraction.timeContract_insert_some_of_not_lt {𝓕 : FieldSpecification} (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : ↥φsΛ.uncontracted) (ht : ¬FieldSpecification.timeOrderRel φs[↑k] φ) (hik : ¬i < i.succAbove ↑k) : ↑(insertAndContract φ φsΛ i (some k)).timeContract = (FieldStatistic.exchangeSign (𝓕.fieldOpStatistic φ)) (FieldStatistic.ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x ≤ ↑k})) • (FieldSpecification.WickAlgebra.contractStateAtIndex φ φsΛ.uncontractedListGet ((uncontractedFieldOpEquiv φs φsΛ) (some k)) * ↑φsΛ.timeContract)

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp, a i ≤ φs.length and a k in φsΛ.uncontracted such that k < i, with the condition that φs[k] does not have time greater or equal to φ, then (φsΛ ↩Λ φ i (some k)).timeContract is equal to the product of

• [anPart φ, φs[k]]ₛ
• φsΛ.timeContract
• the exchange sign of φ with the uncontracted fields in φ₀…φₖ₋₁.
• the exchange sign of φ with the uncontracted fields in φ₀…φₖ.

The proof of this result ultimately is a consequence of definitions and timeContract_of_not_timeOrderRel_expand.

theorem WickContraction.timeContract_of_not_gradingCompliant {𝓕 : FieldSpecification} (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) (h : ¬GradingCompliant φs φsΛ) : φsΛ.timeContract = 0