feat: Wick's theorem for normal ordered lists

HepLean.lean

@@ -133,6 +133,7 @@ import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.StaticWickTheorem
 import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.SuperCommute
 import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction
 import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeOrder
+import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.WicksTheoremNormal
 import HepLean.PerturbationTheory.CreateAnnihilate
 import HepLean.PerturbationTheory.FeynmanDiagrams.Basic
 import HepLean.PerturbationTheory.FeynmanDiagrams.Instances.ComplexScalar
@@ -157,8 +158,12 @@ import HepLean.PerturbationTheory.WickContraction.InsertAndContract
 import HepLean.PerturbationTheory.WickContraction.InsertAndContractNat
 import HepLean.PerturbationTheory.WickContraction.Involutions
 import HepLean.PerturbationTheory.WickContraction.IsFull
+import HepLean.PerturbationTheory.WickContraction.Join
 import HepLean.PerturbationTheory.WickContraction.Sign
+import HepLean.PerturbationTheory.WickContraction.Singleton
 import HepLean.PerturbationTheory.WickContraction.StaticContract
+import HepLean.PerturbationTheory.WickContraction.SubContraction
+import HepLean.PerturbationTheory.WickContraction.TimeCond
 import HepLean.PerturbationTheory.WickContraction.TimeContract
 import HepLean.PerturbationTheory.WickContraction.Uncontracted
 import HepLean.PerturbationTheory.WickContraction.UncontractedList

HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean

@@ -52,6 +52,67 @@ lemma normalOrderF_one : normalOrderF (𝓕 := 𝓕) 1 = 1 := by
   rw [← ofCrAnList_nil, normalOrderF_ofCrAnList, normalOrderSign_nil, normalOrderList_nil,
     ofCrAnList_nil, one_smul]
 
+lemma normalOrderF_normalOrderF_mid (a b c : 𝓕.CrAnAlgebra) :
+    𝓝ᶠ(a * b * c) = 𝓝ᶠ(a * 𝓝ᶠ(b) * c) := by
+  let pc (c : 𝓕.CrAnAlgebra) (hc : c ∈ Submodule.span ℂ (Set.range ofCrAnListBasis)) :
+    Prop := 𝓝ᶠ(a * b * c) = 𝓝ᶠ(a * 𝓝ᶠ(b) * c)
+  change pc c (Basis.mem_span _ c)
+  apply Submodule.span_induction
+  · intro x hx
+    obtain ⟨φs, rfl⟩ := hx
+    simp only [ofListBasis_eq_ofList, pc]
+    let pb (b : 𝓕.CrAnAlgebra) (hb : b ∈ Submodule.span ℂ (Set.range ofCrAnListBasis)) :
+      Prop := 𝓝ᶠ(a * b * ofCrAnList φs) = 𝓝ᶠ(a * 𝓝ᶠ(b) * ofCrAnList φs)
+    change pb b (Basis.mem_span _ b)
+    apply Submodule.span_induction
+    · intro x hx
+      obtain ⟨φs', rfl⟩ := hx
+      simp only [ofListBasis_eq_ofList, pb]
+      let pa (a : 𝓕.CrAnAlgebra) (ha : a ∈ Submodule.span ℂ (Set.range ofCrAnListBasis)) :
+        Prop := 𝓝ᶠ(a * ofCrAnList φs' * ofCrAnList φs) = 𝓝ᶠ(a * 𝓝ᶠ(ofCrAnList φs') * ofCrAnList φs)
+      change pa a (Basis.mem_span _ a)
+      apply Submodule.span_induction
+      · intro x hx
+        obtain ⟨φs'', rfl⟩ := hx
+        simp only [ofListBasis_eq_ofList, pa]
+        rw [normalOrderF_ofCrAnList]
+        simp only [← ofCrAnList_append, Algebra.mul_smul_comm,
+          Algebra.smul_mul_assoc, map_smul]
+        rw [normalOrderF_ofCrAnList, normalOrderF_ofCrAnList, smul_smul]
+        congr 1
+        · simp only [normalOrderSign, normalOrderList]
+          rw [Wick.koszulSign_of_append_eq_insertionSort, mul_comm]
+        · congr 1
+          simp only [normalOrderList]
+          rw [HepLean.List.insertionSort_append_insertionSort_append]
+      · simp [pa]
+      · intro x y hx hy h1 h2
+        simp_all [pa, add_mul]
+      · intro x hx h
+        simp_all [pa]
+    · simp [pb]
+    · intro x y hx hy h1 h2
+      simp_all [pb, mul_add, add_mul]
+    · intro x hx h
+      simp_all [pb]
+  · simp [pc]
+  · intro x y hx hy h1 h2
+    simp_all [pc, mul_add]
+  · intro x hx h hp
+    simp_all [pc]
+
+lemma normalOrderF_normalOrderF_right (a b : 𝓕.CrAnAlgebra) : 𝓝ᶠ(a * b) = 𝓝ᶠ(a * 𝓝ᶠ(b)) := by
+  trans 𝓝ᶠ(a * b * 1)
+  · simp
+  · rw [normalOrderF_normalOrderF_mid]
+    simp
+
+lemma normalOrderF_normalOrderF_left (a b : 𝓕.CrAnAlgebra) : 𝓝ᶠ(a * b) = 𝓝ᶠ(𝓝ᶠ(a) * b) := by
+  trans 𝓝ᶠ(1 * a * b)
+  · simp
+  · rw [normalOrderF_normalOrderF_mid]
+    simp
+
 /-!
 
 ## Normal ordering with a creation operator on the left or annihilation on the right

HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean

@@ -261,6 +261,43 @@ lemma ofCrAnFieldOpList_eq_normalOrder (φs : List 𝓕.CrAnStates) :
   rw [normalOrder_ofCrAnFieldOpList, smul_smul, normalOrderSign, Wick.koszulSign_mul_self,
     one_smul]
 
+lemma normalOrder_normalOrder_mid (a b c : 𝓕.FieldOpAlgebra) :
+    𝓝(a * b * c) = 𝓝(a * 𝓝(b) * c) := by
+  obtain ⟨a, rfl⟩ := ι_surjective a
+  obtain ⟨b, rfl⟩ := ι_surjective b
+  obtain ⟨c, rfl⟩ := ι_surjective c
+  rw [normalOrder_eq_ι_normalOrderF]
+  simp only [← map_mul]
+  rw [normalOrder_eq_ι_normalOrderF]
+  rw [normalOrderF_normalOrderF_mid]
+  rfl
+
+lemma normalOrder_normalOrder_left (a b : 𝓕.FieldOpAlgebra) :
+    𝓝(a * b) = 𝓝(𝓝(a) * b) := by
+  obtain ⟨a, rfl⟩ := ι_surjective a
+  obtain ⟨b, rfl⟩ := ι_surjective b
+  rw [normalOrder_eq_ι_normalOrderF]
+  simp only [← map_mul]
+  rw [normalOrder_eq_ι_normalOrderF]
+  rw [normalOrderF_normalOrderF_left]
+  rfl
+
+lemma normalOrder_normalOrder_right (a b : 𝓕.FieldOpAlgebra) :
+    𝓝(a * b) = 𝓝(a * 𝓝(b)) := by
+  obtain ⟨a, rfl⟩ := ι_surjective a
+  obtain ⟨b, rfl⟩ := ι_surjective b
+  rw [normalOrder_eq_ι_normalOrderF]
+  simp only [← map_mul]
+  rw [normalOrder_eq_ι_normalOrderF]
+  rw [normalOrderF_normalOrderF_right]
+  rfl
+
+lemma normalOrder_normalOrder (a : 𝓕.FieldOpAlgebra) : 𝓝(𝓝(a)) = 𝓝(a) := by
+  trans 𝓝(𝓝(a) * 1)
+  · simp
+  · rw [← normalOrder_normalOrder_left]
+    simp
+
 /-!
 
 ## mul anpart and crpart
@@ -466,7 +503,7 @@ lemma anPart_mul_normalOrder_ofFieldOpList_eq_superCommute_reorder (φ : 𝓕.St
     (φs : List 𝓕.States) : anPart φ * 𝓝(ofFieldOpList φs) =
     𝓝(anPart φ * ofFieldOpList φs) + [anPart φ, 𝓝(ofFieldOpList φs)]ₛ := by
   rw [anPart_mul_normalOrder_ofFieldOpList_eq_superCommute]
-  simp [instCommGroup.eq_1, map_add, map_smul]
+  simp only [instCommGroup.eq_1, add_left_inj]
   rw [normalOrder_anPart_ofFieldOpList_swap]
 
 /--
@@ -525,8 +562,8 @@ lemma ofFieldOpList_normalOrder_insert (φ : 𝓕.States) (φs : List 𝓕.State
   rw [hl]
   rw [ofFieldOpList_append, ofFieldOpList_append]
   rw [ofFieldOpList_mul_ofFieldOpList_eq_superCommute, add_mul]
-  simp [instCommGroup.eq_1, Nat.succ_eq_add_one, ofList_singleton, Algebra.smul_mul_assoc,
-    map_add, map_smul, add_zero, smul_smul,
+  simp only [instCommGroup.eq_1, Nat.succ_eq_add_one, ofList_singleton, Algebra.smul_mul_assoc,
+    map_add, map_smul, normalOrder_superCommute_left_eq_zero, add_zero, smul_smul,
     exchangeSign_mul_self_swap, one_smul]
   rw [← ofFieldOpList_append, ← ofFieldOpList_append]
   simp

HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/StaticWickTheorem.lean

@@ -34,15 +34,15 @@ theorem static_wick_theorem : (φs : List 𝓕.States) →
   | φ :: φs => by
     rw [ofFieldOpList_cons]
     rw [static_wick_theorem φs]
-    rw [show  (φ :: φs) = φs.insertIdx (⟨0, Nat.zero_lt_succ φs.length⟩ : Fin φs.length.succ) φ
+    rw [show (φ :: φs) = φs.insertIdx (⟨0, Nat.zero_lt_succ φs.length⟩ : Fin φs.length.succ) φ
       from rfl]
-    conv_rhs => rw [insertLift_sum ]
+    conv_rhs => rw [insertLift_sum]
     rw [Finset.mul_sum]
     apply Finset.sum_congr rfl
     intro c _
-    trans  (sign φs c • ↑c.staticContract * (ofFieldOp φ * normalOrder (ofFieldOpList [c]ᵘᶜ)))
+    trans (sign φs c • ↑c.staticContract * (ofFieldOp φ * normalOrder (ofFieldOpList [c]ᵘᶜ)))
     · have ht := Subalgebra.mem_center_iff.mp (Subalgebra.smul_mem (Subalgebra.center ℂ _)
-        (c.staticContract).2 c.sign )
+        (c.staticContract).2 c.sign)
       conv_rhs => rw [← mul_assoc, ← ht]
       simp [mul_assoc]
     rw [ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum]
@@ -61,15 +61,15 @@ theorem static_wick_theorem : (φs : List 𝓕.States) →
       simp only [Algebra.smul_mul_assoc, Nat.succ_eq_add_one, Fin.zero_eta, Fin.val_zero,
         List.insertIdx_zero]
       rw [normalOrder_uncontracted_some]
-      simp [← mul_assoc]
+      simp only [← mul_assoc]
       rw [← smul_mul_assoc]
       conv_rhs => rw [← smul_mul_assoc]
       congr 1
       rw [staticConract_insertAndContract_some_eq_mul_contractStateAtIndex_lt]
       swap
       · simp
       rw [smul_smul]
-      by_cases hn :  GradingCompliant φs c ∧ (𝓕|>ₛφ) = (𝓕|>ₛ φs[n.1])
+      by_cases hn : GradingCompliant φs c ∧ (𝓕|>ₛφ) = (𝓕|>ₛ φs[n.1])
       · congr 1
         swap
         · have h1 := c.staticContract.2
@@ -82,19 +82,20 @@ theorem static_wick_theorem : (φs : List 𝓕.States) →
           ofFinset_empty, map_one, one_mul]
         simp only [Fin.zero_succAbove, Fin.not_lt_zero, not_false_eq_true]
         exact hn
-      · simp at hn
+      · simp only [Fin.getElem_fin, not_and] at hn
         by_cases h0 : ¬ GradingCompliant φs c
         · rw [staticContract_of_not_gradingCompliant]
           simp only [ZeroMemClass.coe_zero, zero_mul, smul_zero, instCommGroup.eq_1, mul_zero]
           exact h0
-        · simp_all
-          have h1 :  contractStateAtIndex φ [c]ᵘᶜ
+        · simp_all only [Finset.mem_univ, not_not, instCommGroup.eq_1, forall_const]
+          have h1 : contractStateAtIndex φ [c]ᵘᶜ
               ((uncontractedStatesEquiv φs c) (some n)) = 0 := by
             simp only [contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply,
               Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply,
               instCommGroup.eq_1, Fin.coe_cast, Fin.getElem_fin, smul_eq_zero]
             right
-            simp [uncontractedListGet]
+            simp only [uncontractedListGet, List.getElem_map,
+              uncontractedList_getElem_uncontractedIndexEquiv_symm, List.get_eq_getElem]
             rw [superCommute_anPart_ofState_diff_grade_zero]
             exact hn
           rw [h1]

HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/TimeContraction.lean

@@ -55,6 +55,13 @@ lemma timeContract_of_not_timeOrderRel (φ ψ : 𝓕.States) (h : ¬ timeOrderRe
   simp only [instCommGroup.eq_1, map_smul, map_add, smul_add]
   rw [smul_smul, smul_smul, mul_comm]
 
+lemma timeContract_of_not_timeOrderRel_expand (φ ψ : 𝓕.States) (h : ¬ timeOrderRel φ ψ) :
+    timeContract φ ψ = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ) • [anPart ψ, ofFieldOp φ]ₛ := by
+  rw [timeContract_of_not_timeOrderRel _ _ h]
+  rw [timeContract_of_timeOrderRel _ _ _]
+  have h1 := IsTotal.total (r := 𝓕.timeOrderRel) φ ψ
+  simp_all
+
 lemma timeContract_mem_center (φ ψ : 𝓕.States) :
     timeContract φ ψ ∈ Subalgebra.center ℂ 𝓕.FieldOpAlgebra := by
   by_cases h : timeOrderRel φ ψ
@@ -81,6 +88,90 @@ lemma timeContract_zero_of_diff_grade (φ ψ : 𝓕.States) (h : (𝓕 |>ₛ φ)
     have ht := IsTotal.total (r := 𝓕.timeOrderRel) φ ψ
     simp_all
 
+lemma normalOrder_timeContract (φ ψ : 𝓕.States) :
+    𝓝(timeContract φ ψ) = 0 := by
+  by_cases h : timeOrderRel φ ψ
+  · rw [timeContract_of_timeOrderRel _ _ h]
+    simp
+  · rw [timeContract_of_not_timeOrderRel _ _ h]
+    simp only [instCommGroup.eq_1, map_smul, smul_eq_zero]
+    have h1 : timeOrderRel ψ φ := by
+      have ht : timeOrderRel φ ψ ∨ timeOrderRel ψ φ := IsTotal.total (r := 𝓕.timeOrderRel) φ ψ
+      simp_all
+    rw [timeContract_of_timeOrderRel _ _ h1]
+    simp
+
+lemma timeOrder_timeContract_eq_time_mid {φ ψ : 𝓕.States}
+    (h1 : timeOrderRel φ ψ) (h2 : timeOrderRel ψ φ) (a b : 𝓕.FieldOpAlgebra) :
+    𝓣(a * timeContract φ ψ * b) = timeContract φ ψ * 𝓣(a * b) := by
+  rw [timeContract_of_timeOrderRel _ _ h1]
+  rw [ofFieldOp_eq_sum]
+  simp only [map_sum, Finset.mul_sum, Finset.sum_mul]
+  congr
+  funext x
+  match φ with
+  | .inAsymp φ =>
+    simp
+  | .position φ =>
+    simp only [anPart_position, instCommGroup.eq_1]
+    apply timeOrder_superCommute_eq_time_mid _ _
+    simp only [crAnTimeOrderRel, h1]
+    simp [crAnTimeOrderRel, h2]
+  | .outAsymp φ =>
+    simp only [anPart_posAsymp, instCommGroup.eq_1]
+    apply timeOrder_superCommute_eq_time_mid _ _
+    simp only [crAnTimeOrderRel, h1]
+    simp [crAnTimeOrderRel, h2]
+
+lemma timeOrder_timeContract_eq_time_left {φ ψ : 𝓕.States}
+    (h1 : timeOrderRel φ ψ) (h2 : timeOrderRel ψ φ) (b : 𝓕.FieldOpAlgebra) :
+    𝓣(timeContract φ ψ * b) = timeContract φ ψ * 𝓣(b) := by
+  trans 𝓣(1 * timeContract φ ψ * b)
+  simp only [one_mul]
+  rw [timeOrder_timeContract_eq_time_mid h1 h2]
+  simp
+
+lemma timeOrder_timeContract_neq_time {φ ψ : 𝓕.States}
+    (h1 : ¬ (timeOrderRel φ ψ ∧ timeOrderRel ψ φ)) :
+    𝓣(timeContract φ ψ) = 0 := by
+  by_cases h2 : timeOrderRel φ ψ
+  · simp_all only [true_and]
+    rw [timeContract_of_timeOrderRel _ _ h2]
+    simp only
+    rw [ofFieldOp_eq_sum]
+    simp only [map_sum]
+    apply Finset.sum_eq_zero
+    intro x hx
+    match φ with
+    | .inAsymp φ =>
+      simp
+    | .position φ =>
+      simp only [anPart_position, instCommGroup.eq_1]
+      apply timeOrder_superCommute_neq_time
+      simp_all [crAnTimeOrderRel]
+    | .outAsymp φ =>
+      simp only [anPart_posAsymp, instCommGroup.eq_1]
+      apply timeOrder_superCommute_neq_time
+      simp_all [crAnTimeOrderRel]
+  · rw [timeContract_of_not_timeOrderRel_expand _ _ h2]
+    simp only [instCommGroup.eq_1, map_smul, smul_eq_zero]
+    right
+    rw [ofFieldOp_eq_sum]
+    simp only [map_sum]
+    apply Finset.sum_eq_zero
+    intro x hx
+    match ψ with
+    | .inAsymp ψ =>
+      simp
+    | .position ψ =>
+      simp only [anPart_position, instCommGroup.eq_1]
+      apply timeOrder_superCommute_neq_time
+      simp_all [crAnTimeOrderRel]
+    | .outAsymp ψ =>
+      simp only [anPart_posAsymp, instCommGroup.eq_1]
+      apply timeOrder_superCommute_neq_time
+      simp_all [crAnTimeOrderRel]
+
 end FieldOpAlgebra
 
 end