1. Physlib
  2. QFT
  3. PerturbationTheory
  4. WickContraction
  5. TimeContract
Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.QFT.PerturbationTheory.WickAlgebra.TimeContraction public import Physlib.QFT.PerturbationTheory.WickContraction.InsertAndContract

Time contractions

@[expose] public section

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.

𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succ⊢ ∏ a, ⟨WickAlgebra.timeContract ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i none).fstFieldOfContract (congrLift ⋯ (insertLift i none a)))) ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i none).sndFieldOfContract (congrLift ⋯ (insertLift i none a)))), ⋯⟩ = φsΛ.timeContract 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succ⊢ (fun a => ⟨WickAlgebra.timeContract ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i none).fstFieldOfContract (congrLift ⋯ (insertLift i none a)))) ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i none).sndFieldOfContract (congrLift ⋯ (insertLift i none a)))), ⋯⟩) = fun a => ⟨WickAlgebra.timeContract (φs.get (φsΛ.fstFieldOfContract a)) (φs.get (φsΛ.sndFieldOfContract a)), ⋯⟩ 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succa:↥↑φsΛ⊢ ↑⟨WickAlgebra.timeContract ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i none).fstFieldOfContract (congrLift ⋯ (insertLift i none a)))) ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i none).sndFieldOfContract (congrLift ⋯ (insertLift i none a)))), ⋯⟩ = ↑⟨WickAlgebra.timeContract (φs.get (φsΛ.fstFieldOfContract a)) (φs.get (φsΛ.sndFieldOfContract a)), ⋯⟩ All goals completed! 🐙

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.

𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontracted⊢ ⟨WickAlgebra.timeContract ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).fstFieldOfContract (congrLift ⋯ ⟨{i, i.succAbove ↑j}, ⋯⟩))) ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).sndFieldOfContract (congrLift ⋯ ⟨{i, i.succAbove ↑j}, ⋯⟩))), ⋯⟩ * ∏ a, ⟨WickAlgebra.timeContract ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).fstFieldOfContract (congrLift ⋯ (insertLift i (some j) a)))) ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).sndFieldOfContract (congrLift ⋯ (insertLift i (some j) a)))), ⋯⟩ = (if i < i.succAbove ↑j then ⟨WickAlgebra.timeContract φ φs[↑j], ⋯⟩ else ⟨WickAlgebra.timeContract φs[↑j] φ, ⋯⟩) * φsΛ.timeContract 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontracted⊢ ⟨WickAlgebra.timeContract ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).fstFieldOfContract (congrLift ⋯ ⟨{i, i.succAbove ↑j}, ⋯⟩))) ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).sndFieldOfContract (congrLift ⋯ ⟨{i, i.succAbove ↑j}, ⋯⟩))), ⋯⟩ = if i < i.succAbove ↑j then ⟨WickAlgebra.timeContract φ φs[↑j], ⋯⟩ else ⟨WickAlgebra.timeContract φs[↑j] φ, ⋯⟩𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontracted⊢ ∏ a, ⟨WickAlgebra.timeContract ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).fstFieldOfContract (congrLift ⋯ (insertLift i (some j) a)))) ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).sndFieldOfContract (congrLift ⋯ (insertLift i (some j) a)))), ⋯⟩ = φsΛ.timeContract 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontracted⊢ ⟨WickAlgebra.timeContract ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).fstFieldOfContract (congrLift ⋯ ⟨{i, i.succAbove ↑j}, ⋯⟩))) ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).sndFieldOfContract (congrLift ⋯ ⟨{i, i.succAbove ↑j}, ⋯⟩))), ⋯⟩ = if i < i.succAbove ↑j then ⟨WickAlgebra.timeContract φ φs[↑j], ⋯⟩ else ⟨WickAlgebra.timeContract φs[↑j] φ, ⋯⟩ 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontracted⊢ ⟨WickAlgebra.timeContract (φs.insertIdx (↑i) φ)[↑(if i < i.succAbove ↑j then Fin.cast ⋯ i else Fin.cast ⋯ (i.succAbove ↑j))] (φs.insertIdx (↑i) φ)[↑(if i < i.succAbove ↑j then Fin.cast ⋯ (i.succAbove ↑j) else Fin.cast ⋯ i)], ⋯⟩ = if i < i.succAbove ↑j then ⟨WickAlgebra.timeContract φ φs[↑↑j], ⋯⟩ else ⟨WickAlgebra.timeContract φs[↑↑j] φ, ⋯⟩ 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontractedh✝:i < i.succAbove ↑j⊢ ⟨WickAlgebra.timeContract (φs.insertIdx (↑i) φ)[↑(Fin.cast ⋯ i)] (φs.insertIdx (↑i) φ)[↑(Fin.cast ⋯ (i.succAbove ↑j))], ⋯⟩ = ⟨WickAlgebra.timeContract φ φs[↑↑j], ⋯⟩𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontractedh✝:¬i < i.succAbove ↑j⊢ ⟨WickAlgebra.timeContract (φs.insertIdx (↑i) φ)[↑(Fin.cast ⋯ (i.succAbove ↑j))] (φs.insertIdx (↑i) φ)[↑(Fin.cast ⋯ i)], ⋯⟩ = ⟨WickAlgebra.timeContract φs[↑↑j] φ, ⋯⟩ 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontractedh✝:i < i.succAbove ↑j⊢ ⟨WickAlgebra.timeContract (φs.insertIdx (↑i) φ)[↑(Fin.cast ⋯ i)] (φs.insertIdx (↑i) φ)[↑(Fin.cast ⋯ (i.succAbove ↑j))], ⋯⟩ = ⟨WickAlgebra.timeContract φ φs[↑↑j], ⋯⟩ All goals completed! 🐙 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontractedh✝:¬i < i.succAbove ↑j⊢ ⟨WickAlgebra.timeContract (φs.insertIdx (↑i) φ)[↑(Fin.cast ⋯ (i.succAbove ↑j))] (φs.insertIdx (↑i) φ)[↑(Fin.cast ⋯ i)], ⋯⟩ = ⟨WickAlgebra.timeContract φs[↑↑j] φ, ⋯⟩ All goals completed! 🐙 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontracted⊢ ∏ a, ⟨WickAlgebra.timeContract ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).fstFieldOfContract (congrLift ⋯ (insertLift i (some j) a)))) ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).sndFieldOfContract (congrLift ⋯ (insertLift i (some j) a)))), ⋯⟩ = φsΛ.timeContract 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontracted⊢ (fun a => ⟨WickAlgebra.timeContract ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).fstFieldOfContract (congrLift ⋯ (insertLift i (some j) a)))) ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).sndFieldOfContract (congrLift ⋯ (insertLift i (some j) a)))), ⋯⟩) = fun a => ⟨WickAlgebra.timeContract (φs.get (φsΛ.fstFieldOfContract a)) (φs.get (φsΛ.sndFieldOfContract a)), ⋯⟩ 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succj:↥φsΛ.uncontracteda:↥↑φsΛ⊢ ↑⟨WickAlgebra.timeContract ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).fstFieldOfContract (congrLift ⋯ (insertLift i (some j) a)))) ((φs.insertIdx (↑i) φ).get ((φsΛ↩Λφ i some j).sndFieldOfContract (congrLift ⋯ (insertLift i (some j) a)))), ⋯⟩ = ↑⟨WickAlgebra.timeContract (φs.get (φsΛ.fstFieldOfContract a)) (φs.get (φsΛ.sndFieldOfContract a)), ⋯⟩ All goals completed! 🐙
𝓕:FieldSpecificationφs:List 𝓕.FieldOp⊢ ∏ a, ⟨WickAlgebra.timeContract (φs.get (fstFieldOfContract ⟨∅, ⋯⟩ a)) (φs.get (sndFieldOfContract ⟨∅, ⋯⟩ a)), ⋯⟩ = 1 All goals completed! 🐙

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.

set_option backward.isDefEq.respectTransparency false in𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedht:timeOrderRel φ φs[↑k]hik:i < i.succAbove ↑kh1:ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList)) = ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})⊢ 1 = (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})) * (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k}))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedht:timeOrderRel φ φs[↑k]hik:i < i.succAbove ↑k⊢ timeOrderRel φ φs[↑↑k] 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedht:timeOrderRel φ φs[↑k]hik:i < i.succAbove ↑k⊢ timeOrderRel φ φs[↑↑k] 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedht:timeOrderRel φ φs[↑k]hik:i < i.succAbove ↑k⊢ timeOrderRel φ φs[↑↑k] All goals completed! 🐙

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.

set_option backward.isDefEq.respectTransparency false in𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedht:¬timeOrderRel φs[↑k] φhik:¬i < i.succAbove ↑kh1✝:ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k)) (List.map φs.get φsΛ.uncontractedList)) = ofFinset 𝓕.fieldOpStatistic φs.get ({x ∈ φsΛ.uncontracted | x < ↑k})a:Fin φs.lengthh:(a ∈ φsΛ.uncontracted ∧ a ≤ ↑k ∨ a ∈ φsΛ.uncontracted ∧ a < ↑k) ∧ (a ∈ φsΛ.uncontracted → a ≤ ↑k → a ∈ φsΛ.uncontracted → ↑k ≤ a)h1:a ∈ φsΛ.uncontracted ∧ a < ↑kh2':↑k ≤ a⊢ a = ↑k All goals completed! 🐙 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedht✝:¬timeOrderRel φs[↑k] φhik:¬i < i.succAbove ↑kht:timeOrderRel φs[↑k] φ ∨ timeOrderRel φ φs[↑k]⊢ timeOrderRel φ φs[↑↑k]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedht:¬timeOrderRel φs[↑k] φhik:¬i < i.succAbove ↑k⊢ ¬timeOrderRel φs[↑↑k] φ 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.length.succk:↥φsΛ.uncontractedht:¬timeOrderRel φs[↑k] φhik:¬i < i.succAbove ↑k⊢ ¬timeOrderRel φs[↑↑k] φ All goals completed! 🐙
𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin φs.length)ha:a ∈ ↑φsΛha2:¬(𝓕|>ₛφs[↑(φsΛ.fstFieldOfContract ⟨a, ha⟩)]) = 𝓕|>ₛφs[↑(φsΛ.sndFieldOfContract ⟨a, ha⟩)]⊢ (𝓕|>ₛφs[↑(φsΛ.fstFieldOfContract ⟨a, ha⟩)]) ≠ 𝓕|>ₛφs[↑(φsΛ.sndFieldOfContract ⟨a, ha⟩)] All goals completed! 🐙