/- 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 -/ import HepLean.PerturbationTheory.WickContraction.Sign import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.TimeContraction /-! # Time contractions -/ open FieldSpecification variable {𝓕 : FieldSpecification} namespace WickContraction variable {n : β„•} (c : WickContraction n) open HepLean.List /-- Given a Wick contraction `Ο†sΞ›` associated with a list `Ο†s`, the product of all time-contractions of pairs of contracted elements in `Ο†s`, as a member of the center of `π“ž.A`. -/ noncomputable def timeContract (π“ž : 𝓕.ProtoOperatorAlgebra) {Ο†s : List 𝓕.States} (Ο†sΞ› : WickContraction Ο†s.length) : Subalgebra.center β„‚ π“ž.A := ∏ (a : Ο†sΞ›.1), βŸ¨π“ž.timeContract (Ο†s.get (Ο†sΞ›.fstFieldOfContract a)) (Ο†s.get (Ο†sΞ›.sndFieldOfContract a)), π“ž.timeContract_mem_center _ _⟩ /-- For `Ο†sΞ›` a Wick contraction for `Ο†s`, the time contraction `(Ο†sΞ› ↩Λ Ο† i none).timeContract π“ž` is equal to `Ο†sΞ›.timeContract π“ž`. This result follows from the fact that `timeContract` only depends on contracted pairs, and `(Ο†sΞ› ↩Λ Ο† i none)` has the 'same' contracted pairs as `Ο†sΞ›`. -/ @[simp] lemma timeContract_insertAndContract_none (π“ž : 𝓕.ProtoOperatorAlgebra) (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) (Ο†sΞ› : WickContraction Ο†s.length) (i : Fin Ο†s.length.succ) : (Ο†sΞ› ↩Λ Ο† i none).timeContract π“ž = Ο†sΞ›.timeContract π“ž := by rw [timeContract, insertAndContract_none_prod_contractions] congr ext a simp /-- For `Ο†sΞ›` a Wick contraction for `Ο†s = φ₀…φₙ`, the time contraction `(Ο†sΞ› ↩Λ Ο† i (some j)).timeContract π“ž` is equal to the multiple of - the time contraction of `Ο†` with `Ο†β±Ό` if `i < i.succAbove j` else `Ο†β±Ό` with `Ο†`. - `Ο†sΞ›.timeContract π“ž`. This follows from the fact that `(Ο†sΞ› ↩Λ Ο† i (some j))` has one more contracted pair than `Ο†sΞ›`, corresponding to `Ο†` contracted with `Ο†β±Ό`. The order depends on whether we insert `Ο†` before or after `Ο†β±Ό`. -/ lemma timeConract_insertAndContract_some (π“ž : 𝓕.ProtoOperatorAlgebra) (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) (Ο†sΞ› : WickContraction Ο†s.length) (i : Fin Ο†s.length.succ) (j : Ο†sΞ›.uncontracted) : (Ο†sΞ› ↩Λ Ο† i (some j)).timeContract π“ž = (if i < i.succAbove j then βŸ¨π“ž.timeContract Ο† Ο†s[j.1], π“ž.timeContract_mem_center _ _⟩ else βŸ¨π“ž.timeContract Ο†s[j.1] Ο†, π“ž.timeContract_mem_center _ _⟩) * Ο†sΞ›.timeContract π“ž := by rw [timeContract, insertAndContract_some_prod_contractions] congr 1 Β· simp only [Nat.succ_eq_add_one, insertAndContract_fstFieldOfContract_some_incl, finCongr_apply, List.get_eq_getElem, insertAndContract_sndFieldOfContract_some_incl, Fin.getElem_fin] split Β· simp Β· simp Β· congr ext a simp open FieldStatistic lemma timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_lt (π“ž : 𝓕.ProtoOperatorAlgebra) (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) (Ο†sΞ› : WickContraction Ο†s.length) (i : Fin Ο†s.length.succ) (k : Ο†sΞ›.uncontracted) (ht : 𝓕.timeOrderRel Ο† Ο†s[k.1]) (hik : i < i.succAbove k) : (Ο†sΞ› ↩Λ Ο† i (some k)).timeContract π“ž = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› βŸ¨Ο†s.get, (Ο†sΞ›.uncontracted.filter (fun x => x < k))⟩) β€’ (π“ž.contractStateAtIndex Ο† [Ο†sΞ›]ᡘᢜ ((uncontractedStatesEquiv Ο†s Ο†sΞ›) (some k)) * Ο†sΞ›.timeContract π“ž) := by rw [timeConract_insertAndContract_some] simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul, instCommGroup.eq_1, ProtoOperatorAlgebra.contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply, Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, Fin.coe_cast, List.getElem_map, uncontractedList_getElem_uncontractedIndexEquiv_symm, List.get_eq_getElem, Algebra.smul_mul_assoc, uncontractedListGet] Β· simp only [hik, ↓reduceIte, MulMemClass.coe_mul] rw [π“ž.timeContract_of_timeOrderRel] trans (1 : β„‚) β€’ (π“ž.crAnF ((CrAnAlgebra.superCommute (CrAnAlgebra.anPart (StateAlgebra.ofState Ο†))) (CrAnAlgebra.ofState Ο†s[k.1])) * ↑(timeContract π“ž Ο†sΞ›)) Β· simp simp only [smul_smul] congr have h1 : ofList 𝓕.statesStatistic (List.take (↑(Ο†sΞ›.uncontractedIndexEquiv.symm k)) (List.map Ο†s.get Ο†sΞ›.uncontractedList)) = (𝓕 |>β‚› βŸ¨Ο†s.get, (Finset.filter (fun x => x < k) Ο†sΞ›.uncontracted)⟩) := by simp only [ofFinset] congr rw [← List.map_take] congr rw [take_uncontractedIndexEquiv_symm] rw [filter_uncontractedList] rw [h1] simp only [exchangeSign_mul_self] Β· exact ht lemma timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_not_lt (π“ž : 𝓕.ProtoOperatorAlgebra) (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) (Ο†sΞ› : WickContraction Ο†s.length) (i : Fin Ο†s.length.succ) (k : Ο†sΞ›.uncontracted) (ht : Β¬ 𝓕.timeOrderRel Ο†s[k.1] Ο†) (hik : Β¬ i < i.succAbove k) : (Ο†sΞ› ↩Λ Ο† i (some k)).timeContract π“ž = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› βŸ¨Ο†s.get, (Ο†sΞ›.uncontracted.filter (fun x => x ≀ k))⟩) β€’ (π“ž.contractStateAtIndex Ο† [Ο†sΞ›]ᡘᢜ ((uncontractedStatesEquiv Ο†s Ο†sΞ›) (some k)) * Ο†sΞ›.timeContract π“ž) := by rw [timeConract_insertAndContract_some] simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul, instCommGroup.eq_1, ProtoOperatorAlgebra.contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply, Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, Fin.coe_cast, List.getElem_map, uncontractedList_getElem_uncontractedIndexEquiv_symm, List.get_eq_getElem, Algebra.smul_mul_assoc, uncontractedListGet] simp only [hik, ↓reduceIte, MulMemClass.coe_mul] rw [π“ž.timeContract_of_not_timeOrderRel, π“ž.timeContract_of_timeOrderRel] simp only [instCommGroup.eq_1, Algebra.smul_mul_assoc, smul_smul] congr have h1 : ofList 𝓕.statesStatistic (List.take (↑(Ο†sΞ›.uncontractedIndexEquiv.symm k)) (List.map Ο†s.get Ο†sΞ›.uncontractedList)) = (𝓕 |>β‚› βŸ¨Ο†s.get, (Finset.filter (fun x => x < k) Ο†sΞ›.uncontracted)⟩) := by simp only [ofFinset] congr rw [← List.map_take] congr rw [take_uncontractedIndexEquiv_symm, filter_uncontractedList] rw [h1] trans 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› βŸ¨Ο†s.get, {k.1}⟩) Β· rw [exchangeSign_symm, ofFinset_singleton] simp rw [← map_mul] congr rw [ofFinset_union] congr ext a simp only [Finset.mem_singleton, Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_inter, not_and, not_lt, and_imp] apply Iff.intro Β· intro h subst h simp Β· intro h have h1 := h.1 rcases h1 with h1 | h1 Β· have h2' := h.2 h1.1 h1.2 h1.1 omega Β· have h2' := h.2 h1.1 (by omega) h1.1 omega have ht := IsTotal.total (r := timeOrderRel) Ο†s[k.1] Ο† simp_all only [Fin.getElem_fin, Nat.succ_eq_add_one, not_lt, false_or] exact ht lemma timeContract_of_not_gradingCompliant (π“ž : 𝓕.ProtoOperatorAlgebra) (Ο†s : List 𝓕.States) (Ο†sΞ› : WickContraction Ο†s.length) (h : Β¬ GradingCompliant Ο†s Ο†sΞ›) : Ο†sΞ›.timeContract π“ž = 0 := by rw [timeContract] simp only [GradingCompliant, Fin.getElem_fin, Subtype.forall, not_forall] at h obtain ⟨a, ha⟩ := h obtain ⟨ha, ha2⟩ := ha apply Finset.prod_eq_zero (i := ⟨a, ha⟩) simp only [Finset.univ_eq_attach, Finset.mem_attach] apply Subtype.eq simp only [List.get_eq_getElem, ZeroMemClass.coe_zero] rw [ProtoOperatorAlgebra.timeContract_zero_of_diff_grade] simp [ha2] end WickContraction