/- 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.TimeContract import HepLean.Meta.Remark.Basic /-! # Wick's theorem This file contrains the time-dependent version of Wick's theorem for lists of fields containing both fermions and bosons. Wick's theorem is related to Isserlis' theorem in mathematics. -/ namespace FieldSpecification variable {𝓕 : FieldSpecification} {π“ž : 𝓕.ProtoOperatorAlgebra} open CrAnAlgebra open StateAlgebra open ProtoOperatorAlgebra open HepLean.List open WickContraction open FieldStatistic /-- Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`. We have (roughly) `N(c.insertList Ο† i none).uncontractedList = s β€’ N(Ο† * c.uncontractedList)` Where `s` is the exchange sign for `Ο†` and the uncontracted fields in `φ₀φ₁…φᡒ`. -/ lemma insertList_none_normalOrder (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) (i : Fin Ο†s.length.succ) (Ο†sΞ› : WickContraction Ο†s.length) : π“ž.crAnF (𝓝(ofStateList [Ο†sΞ›.insertList Ο† i none]ᡘᢜ)) = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› βŸ¨Ο†s.get, Ο†sΞ›.uncontracted.filter (fun x => i.succAbove x < i)⟩) β€’ π“ž.crAnF 𝓝(ofStateList (Ο† :: [Ο†sΞ›]ᡘᢜ)) := by simp only [Nat.succ_eq_add_one, instCommGroup.eq_1] rw [crAnF_ofState_normalOrder_insert Ο† [Ο†sΞ›]ᡘᢜ ⟨(Ο†sΞ›.uncontractedListOrderPos i), by simp [uncontractedListGet]⟩, smul_smul] trans (1 : β„‚) β€’ π“ž.crAnF (𝓝(ofStateList [Ο†sΞ›.insertList Ο† i none]ᡘᢜ)) Β· simp congr 1 simp only [instCommGroup.eq_1, uncontractedListGet] rw [← List.map_take, take_uncontractedListOrderPos_eq_filter] have h1 : (𝓕 |>β‚› List.map Ο†s.get (List.filter (fun x => decide (↑x < i.1)) Ο†sΞ›.uncontractedList)) = 𝓕 |>β‚› βŸ¨Ο†s.get, (Ο†sΞ›.uncontracted.filter (fun x => x.val < i.1))⟩ := by simp only [Nat.succ_eq_add_one, ofFinset] congr rw [uncontractedList_eq_sort] have hdup : (List.filter (fun x => decide (x.1 < i.1)) (Finset.sort (fun x1 x2 => x1 ≀ x2) Ο†sΞ›.uncontracted)).Nodup := by exact List.Nodup.filter _ (Finset.sort_nodup (fun x1 x2 => x1 ≀ x2) Ο†sΞ›.uncontracted) have hsort : (List.filter (fun x => decide (x.1 < i.1)) (Finset.sort (fun x1 x2 => x1 ≀ x2) Ο†sΞ›.uncontracted)).Sorted (Β· ≀ Β·) := by exact List.Sorted.filter _ (Finset.sort_sorted (fun x1 x2 => x1 ≀ x2) Ο†sΞ›.uncontracted) rw [← (List.toFinset_sort (Β· ≀ Β·) hdup).mpr hsort] congr ext a simp rw [h1] simp only [Nat.succ_eq_add_one] have h2 : (Finset.filter (fun x => x.1 < i.1) Ο†sΞ›.uncontracted) = (Finset.filter (fun x => i.succAbove x < i) Ο†sΞ›.uncontracted) := by ext a simp only [Nat.succ_eq_add_one, Finset.mem_filter, and_congr_right_iff] intro ha simp only [Fin.succAbove] split Β· apply Iff.intro Β· intro h omega Β· intro h rename_i h rw [Fin.lt_def] at h simp only [Fin.coe_castSucc] at h omega Β· apply Iff.intro Β· intro h rename_i h' rw [Fin.lt_def] simp only [Fin.val_succ] rw [Fin.lt_def] at h' simp only [Fin.coe_castSucc, not_lt] at h' omega Β· intro h rename_i h rw [Fin.lt_def] at h simp only [Fin.val_succ] at h omega rw [h2] simp only [exchangeSign_mul_self] congr simp only [Nat.succ_eq_add_one] rw [insertList_uncontractedList_none_map] /-- Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`. We have (roughly) `N(c.insertList Ο† i k).uncontractedList` is equal to `N((c.uncontractedList).eraseIdx k')` where `k'` is the position in `c.uncontractedList` corresponding to `k`. -/ lemma insertList_some_normalOrder (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) (i : Fin Ο†s.length.succ) (Ο†sΞ› : WickContraction Ο†s.length) (k : Ο†sΞ›.uncontracted) : π“ž.crAnF 𝓝(ofStateList [Ο†sΞ›.insertList Ο† i (some k)]ᡘᢜ) = π“ž.crAnF 𝓝(ofStateList (optionEraseZ [Ο†sΞ›]ᡘᢜ Ο† ((uncontractedStatesEquiv Ο†s Ο†sΞ›) k))) := by simp only [Nat.succ_eq_add_one, insertList, optionEraseZ, uncontractedStatesEquiv, Equiv.optionCongr_apply, Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, Fin.coe_cast, uncontractedListGet] congr rw [congr_uncontractedList] erw [uncontractedList_extractEquiv_symm_some] simp only [Fin.coe_succAboveEmb, List.map_eraseIdx, List.map_map] congr conv_rhs => rw [get_eq_insertIdx_succAbove Ο† Ο†s i] /-- Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`. This lemma states that `(c.sign β€’ c.timeContract π“ž) * N(c.uncontracted)` for `c` equal to `c.insertList Ο† i none` is equal to that for just `c` mulitiplied by the exchange sign of `Ο†` and `φ₀φ₁…φᡒ₋₁`. -/ lemma sign_timeContract_normalOrder_insertList_none (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) (i : Fin Ο†s.length.succ) (Ο†sΞ› : WickContraction Ο†s.length) : (Ο†sΞ›.insertList Ο† i none).sign β€’ (Ο†sΞ›.insertList Ο† i none).timeContract π“ž * π“ž.crAnF 𝓝(ofStateList [Ο†sΞ›.insertList Ο† i none]ᡘᢜ) = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› βŸ¨Ο†s.get, (Finset.univ.filter (fun k => i.succAbove k < i))⟩) β€’ (Ο†sΞ›.sign β€’ Ο†sΞ›.timeContract π“ž * π“ž.crAnF 𝓝(ofStateList (Ο† :: [Ο†sΞ›]ᡘᢜ))) := by by_cases hg : GradingCompliant Ο†s Ο†sΞ› Β· rw [insertList_none_normalOrder, sign_insert_none] simp only [Nat.succ_eq_add_one, timeContract_insertList_none, instCommGroup.eq_1, Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_smul] congr 1 rw [← mul_assoc] congr 1 rw [signInsertNone_eq_filterset _ _ _ _ hg, ← map_mul] congr rw [ofFinset_union] congr ext a simp only [Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_inter, not_and, not_lt, and_imp] apply Iff.intro Β· intro ha have ha1 := ha.1 rcases ha1 with ha1 | ha1 Β· exact ha1.2 Β· exact ha1.2 Β· intro ha simp only [uncontracted, Finset.mem_filter, Finset.mem_univ, true_and, ha, and_true, forall_const] have hx : Ο†sΞ›.getDual? a = none ↔ Β¬ (Ο†sΞ›.getDual? a).isSome := by simp rw [hx] simp only [Bool.not_eq_true, Bool.eq_false_or_eq_true_self, true_and] intro h1 h2 simp_all Β· simp only [Nat.succ_eq_add_one, timeContract_insertList_none, Algebra.smul_mul_assoc, instCommGroup.eq_1] rw [timeContract_of_not_gradingCompliant] simp only [ZeroMemClass.coe_zero, zero_mul, smul_zero] exact hg /-- Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`. This lemma states that `(c.sign β€’ c.timeContract π“ž) * N(c.uncontracted)` for `c` equal to `c.insertList Ο† i (some k)` is equal to that for just `c` mulitiplied by the exchange sign of `Ο†` and `φ₀φ₁…φᡒ₋₁`. -/ lemma sign_timeContract_normalOrder_insertList_some (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) (i : Fin Ο†s.length.succ) (Ο†sΞ› : WickContraction Ο†s.length) (k : Ο†sΞ›.uncontracted) (hlt : βˆ€ (k : Fin Ο†s.length), timeOrderRel Ο† Ο†s[k]) (hn : βˆ€ (k : Fin Ο†s.length), i.succAbove k < i β†’ Β¬ timeOrderRel Ο†s[k] Ο†) : (Ο†sΞ›.insertList Ο† i (some k)).sign β€’ (Ο†sΞ›.insertList Ο† i (some k)).timeContract π“ž * π“ž.crAnF 𝓝(ofStateList [Ο†sΞ›.insertList Ο† i (some k)]ᡘᢜ) = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› βŸ¨Ο†s.get, (Finset.univ.filter (fun x => i.succAbove x < i))⟩) β€’ (Ο†sΞ›.sign β€’ (π“ž.contractStateAtIndex Ο† [Ο†sΞ›]ᡘᢜ ((uncontractedStatesEquiv Ο†s Ο†sΞ›) (some k)) * Ο†sΞ›.timeContract π“ž) * π“ž.crAnF 𝓝(ofStateList (optionEraseZ [Ο†sΞ›]ᡘᢜ Ο† ((uncontractedStatesEquiv Ο†s Ο†sΞ›) k)))) := by by_cases hg : GradingCompliant Ο†s Ο†sΞ› ∧ (𝓕 |>β‚› Ο†) = (𝓕 |>β‚› Ο†s[k.1]) Β· by_cases hk : i.succAbove k < i Β· rw [WickContraction.timeConract_insertList_some_eq_mul_contractStateAtIndex_not_lt] swap Β· exact hn _ hk rw [insertList_some_normalOrder, sign_insert_some] simp only [instCommGroup.eq_1, smul_smul, Algebra.smul_mul_assoc] congr 1 rw [mul_assoc, mul_comm (sign Ο†s Ο†sΞ›), ← mul_assoc] congr 1 exact signInsertSome_mul_filter_contracted_of_lt Ο† Ο†s Ο†sΞ› i k hk hg Β· omega Β· have hik : i.succAbove ↑k β‰  i := Fin.succAbove_ne i ↑k rw [WickContraction.timeConract_insertList_some_eq_mul_contractStateAtIndex_lt] swap Β· exact hlt _ rw [insertList_some_normalOrder] rw [sign_insert_some] simp only [instCommGroup.eq_1, smul_smul, Algebra.smul_mul_assoc] congr 1 rw [mul_assoc, mul_comm (sign Ο†s Ο†sΞ›), ← mul_assoc] congr 1 exact signInsertSome_mul_filter_contracted_of_not_lt Ο† Ο†s Ο†sΞ› i k hk hg Β· omega Β· rw [timeConract_insertList_some] simp only [Fin.getElem_fin, not_and] at hg by_cases hg' : GradingCompliant Ο†s Ο†sΞ› Β· have hg := hg hg' simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul, Algebra.smul_mul_assoc, instCommGroup.eq_1, 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, uncontractedListGet] by_cases h1 : i < i.succAbove ↑k Β· simp only [h1, ↓reduceIte, MulMemClass.coe_mul] rw [timeContract_zero_of_diff_grade] simp only [zero_mul, smul_zero] rw [crAnF_superCommute_anPart_ofState_diff_grade_zero] simp only [zero_mul, smul_zero] exact hg exact hg Β· simp only [h1, ↓reduceIte, MulMemClass.coe_mul] rw [timeContract_zero_of_diff_grade] simp only [zero_mul, smul_zero] rw [crAnF_superCommute_anPart_ofState_diff_grade_zero] simp only [zero_mul, smul_zero] exact hg exact fun a => hg (id (Eq.symm a)) Β· rw [timeContract_of_not_gradingCompliant] simp only [Nat.succ_eq_add_one, Fin.getElem_fin, mul_zero, ZeroMemClass.coe_zero, smul_zero, zero_mul, instCommGroup.eq_1] exact hg' /-- Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`. This lemma states that `(c.sign β€’ c.timeContract π“ž) * N(c.uncontracted)` is equal to the sum of `(c'.sign β€’ c'.timeContract π“ž) * N(c'.uncontracted)` for all `c' = (c.insertList Ο† i k)` for `k : Option (c.uncontracted)`, multiplied by the exchange sign of `Ο†` and `φ₀φ₁…φᡒ₋₁`. -/ lemma mul_sum_contractions (Ο† : 𝓕.States) (Ο†s : List 𝓕.States) (i : Fin Ο†s.length.succ) (Ο†sΞ› : WickContraction Ο†s.length) (hlt : βˆ€ (k : Fin Ο†s.length), timeOrderRel Ο† Ο†s[k]) (hn : βˆ€ (k : Fin Ο†s.length), i.succAbove k < i β†’ Β¬timeOrderRel Ο†s[k] Ο†) : (Ο†sΞ›.sign β€’ Ο†sΞ›.timeContract π“ž) * π“ž.crAnF ((CrAnAlgebra.ofState Ο†) * 𝓝(ofStateList [Ο†sΞ›]ᡘᢜ)) = 𝓒(𝓕 |>β‚› Ο†, 𝓕 |>β‚› βŸ¨Ο†s.get, (Finset.univ.filter (fun x => i.succAbove x < i))⟩) β€’ βˆ‘ (k : Option Ο†sΞ›.uncontracted), ((Ο†sΞ›.insertList Ο† i k).sign β€’ (Ο†sΞ›.insertList Ο† i k).timeContract π“ž * π“ž.crAnF (𝓝(ofStateList [Ο†sΞ›.insertList Ο† i k]ᡘᢜ))) := by rw [crAnF_ofState_mul_normalOrder_ofStatesList_eq_sum, Finset.mul_sum, uncontractedStatesEquiv_list_sum, Finset.smul_sum] simp only [instCommGroup.eq_1, Nat.succ_eq_add_one] congr 1 funext n match n with | none => rw [sign_timeContract_normalOrder_insertList_none] simp only [contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply, Equiv.coe_trans, Option.map_none', one_mul, Algebra.smul_mul_assoc, instCommGroup.eq_1, smul_smul] congr 1 rw [← mul_assoc, exchangeSign_mul_self] simp | some n => rw [sign_timeContract_normalOrder_insertList_some _ _ _ _ _ (fun k => hlt k) (fun k a => hn k a)] simp only [uncontractedStatesEquiv, Equiv.optionCongr_apply, Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, Algebra.smul_mul_assoc, instCommGroup.eq_1, smul_smul] congr 1 Β· rw [← mul_assoc, exchangeSign_mul_self] rw [one_mul] Β· rw [← mul_assoc] congr 1 have ht := (WickContraction.timeContract π“ž Ο†sΞ›).prop rw [@Subalgebra.mem_center_iff] at ht rw [ht] lemma wicks_theorem_congr {Ο†s Ο†s' : List 𝓕.States} (h : Ο†s = Ο†s') : βˆ‘ (Ο†sΞ› : WickContraction Ο†s.length), (Ο†sΞ›.sign β€’ Ο†sΞ›.timeContract π“ž) * π“ž.crAnF 𝓝(ofStateList [Ο†sΞ›]ᡘᢜ) = βˆ‘ (Ο†s'Ξ› : WickContraction Ο†s'.length), (Ο†s'Ξ›.sign β€’ Ο†s'Ξ›.timeContract π“ž) * π“ž.crAnF 𝓝(ofStateList [Ο†s'Ξ›]ᡘᢜ) := by subst h simp /-! ## Wick's theorem -/ /-- Wick's theorem for the empty list. -/ lemma wicks_theorem_nil : π“ž.crAnF (ofStateAlgebra (timeOrder (ofList []))) = βˆ‘ (nilΞ› : WickContraction [].length), (nilΞ›.sign β€’ nilΞ›.timeContract π“ž) * π“ž.crAnF 𝓝(ofStateList [nilΞ›]ᡘᢜ) := by rw [timeOrder_ofList_nil] simp only [map_one, List.length_nil, Algebra.smul_mul_assoc] rw [sum_WickContraction_nil, uncontractedListGet, nil_zero_uncontractedList] simp only [List.map_nil] have h1 : ofStateList (𝓕 := 𝓕) [] = CrAnAlgebra.ofCrAnList [] := by simp rw [h1, normalOrder_ofCrAnList] simp [WickContraction.timeContract, empty, sign] remark wicks_theorem_context := " Wick's theorem is one of the most important results in perturbative quantum field theory. It expresses a time-ordered product of fields as a sum of terms consisting of time-contractions of pairs of fields multiplied by the normal-ordered product of the remaining fields. Wick's theorem is also the precursor to the diagrammatic approach to quantum field theory called Feynman diagrams." /-- Wick's theorem for time-ordered products of bosonic and fermionic fields. The time ordered product `T(φ₀φ₁…φₙ)` is equal to the sum of terms, for all possible Wick contractions `c` of the list of fields `Ο†s := φ₀φ₁…φₙ`, given by the multiple of: - The sign corresponding to the number of fermionic-fermionic exchanges one must do to put elements in contracted pairs of `c` next to each other. - The product of time-contractions of the contracted pairs of `c`. - The normal-ordering of the uncontracted fields in `c`. -/ theorem wicks_theorem : (Ο†s : List 𝓕.States) β†’ π“ž.crAnF (ofStateAlgebra (timeOrder (ofList Ο†s))) = βˆ‘ (Ο†sΞ› : WickContraction Ο†s.length), (Ο†sΞ›.sign β€’ Ο†sΞ›.timeContract π“ž) * π“ž.crAnF 𝓝(ofStateList [Ο†sΞ›]ᡘᢜ) | [] => wicks_theorem_nil | Ο† :: Ο†s => by have ih := wicks_theorem (eraseMaxTimeField Ο† Ο†s) rw [timeOrder_eq_maxTimeField_mul_finset, map_mul, map_mul, ih, Finset.mul_sum] have h1 : Ο† :: Ο†s = (eraseMaxTimeField Ο† Ο†s).insertIdx (maxTimeFieldPosFin Ο† Ο†s) (maxTimeField Ο† Ο†s) := by simp only [eraseMaxTimeField, insertionSortDropMinPos, List.length_cons, Nat.succ_eq_add_one, maxTimeField, insertionSortMin, List.get_eq_getElem] erw [insertIdx_eraseIdx_fin] rw [wicks_theorem_congr h1] conv_rhs => rw [insertLift_sum] congr funext c have ht := Subalgebra.mem_center_iff.mp (Subalgebra.smul_mem (Subalgebra.center β„‚ π“ž.A) (WickContraction.timeContract π“ž c).2 (sign (eraseMaxTimeField Ο† Ο†s) c)) rw [map_smul, map_smul, Algebra.smul_mul_assoc, ← mul_assoc, ht, mul_assoc, ← map_mul] rw [ofStateAlgebra_ofState, mul_sum_contractions (π“ž := π“ž) (maxTimeField Ο† Ο†s) (eraseMaxTimeField Ο† Ο†s) (maxTimeFieldPosFin Ο† Ο†s) c] trans (1 : β„‚) β€’ βˆ‘ k : Option { x // x ∈ c.uncontracted }, sign (List.insertIdx (↑(maxTimeFieldPosFin Ο† Ο†s)) (maxTimeField Ο† Ο†s) (eraseMaxTimeField Ο† Ο†s)) (insertList (maxTimeField Ο† Ο†s) c (maxTimeFieldPosFin Ο† Ο†s) k) β€’ ↑((c.insertList (maxTimeField Ο† Ο†s) (maxTimeFieldPosFin Ο† Ο†s) k).timeContract π“ž) * π“ž.crAnF 𝓝(ofStateList (List.map (List.insertIdx (↑(maxTimeFieldPosFin Ο† Ο†s)) (maxTimeField Ο† Ο†s) (eraseMaxTimeField Ο† Ο†s)).get (insertList (maxTimeField Ο† Ο†s) c (maxTimeFieldPosFin Ο† Ο†s) k).uncontractedList)) swap Β· simp [uncontractedListGet] rw [smul_smul] simp only [instCommGroup.eq_1, exchangeSign_mul_self, Nat.succ_eq_add_one, Algebra.smul_mul_assoc, Fintype.sum_option, timeContract_insertList_none, Finset.univ_eq_attach, smul_add, one_smul, uncontractedListGet] Β· exact fun k => timeOrder_maxTimeField _ _ k Β· exact fun k => lt_maxTimeFieldPosFin_not_timeOrder _ _ k termination_by Ο†s => Ο†s.length end FieldSpecification