refactor: Docs around Wick's theorem

HepLean.lean

@@ -121,9 +121,9 @@ import HepLean.Meta.TransverseTactics
 import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.Basic
 import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.NormalOrder
 import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.SuperCommute
-import HepLean.PerturbationTheory.Algebras.OperatorAlgebra.Basic
-import HepLean.PerturbationTheory.Algebras.OperatorAlgebra.NormalOrder
-import HepLean.PerturbationTheory.Algebras.OperatorAlgebra.TimeContraction
+import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.Basic
+import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.NormalOrder
+import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.TimeContraction
 import HepLean.PerturbationTheory.Algebras.StateAlgebra.Basic
 import HepLean.PerturbationTheory.Algebras.StateAlgebra.TimeOrder
 import HepLean.PerturbationTheory.CreateAnnihilate

HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean

@@ -10,17 +10,19 @@ import HepLean.PerturbationTheory.Koszul.KoszulSign
 
 # Normal Ordering in the CrAnAlgebra
 
+In the module
+`HepLean.PerturbationTheory.FieldSpecification.NormalOrder`
+we defined the normal ordering of a list of `CrAnStates`.
+In this module we extend the normal ordering to a linear map on `CrAnAlgebra`.
+
+We derive properties of this normal ordering.
 
 -/
 
 namespace FieldSpecification
 variable {𝓕 : FieldSpecification}
 open FieldStatistic
-/-!
 
-## Normal order on the CrAnAlgebra
-
--/
 namespace CrAnAlgebra
 
 noncomputable section
@@ -51,6 +53,12 @@ lemma normalOrder_one : normalOrder (𝓕 := 𝓕) 1 = 1 := by
   rw [← ofCrAnList_nil, normalOrder_ofCrAnList]
   simp
 
+/-!
+
+## Normal ordering with a creation operator on the left or annihilation on the right
+
+-/
+
 lemma normalOrder_ofCrAnList_cons_create (φ : 𝓕.CrAnStates)
     (hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) (φs : List 𝓕.CrAnStates) :
     normalOrder (ofCrAnList (φ :: φs)) =
@@ -95,9 +103,48 @@ lemma normalOrder_mul_annihilate (φ : 𝓕.CrAnStates)
   rw [← ofCrAnList_singleton, ← ofCrAnList_append, ofCrAnList_singleton]
   rw [normalOrder_ofCrAnList_append_annihilate φ hφ]
 
+lemma normalOrder_crPart_mul (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
+    normalOrder (crPart (StateAlgebra.ofState φ) * a) =
+    crPart (StateAlgebra.ofState φ) * normalOrder a := by
+  match φ with
+  | .negAsymp φ =>
+    dsimp only [crPart, StateAlgebra.ofState]
+    simp only [FreeAlgebra.lift_ι_apply]
+    exact normalOrder_create_mul ⟨States.negAsymp φ, ()⟩ rfl a
+  | .position φ =>
+    dsimp only [crPart, StateAlgebra.ofState]
+    simp only [FreeAlgebra.lift_ι_apply]
+    refine normalOrder_create_mul _ ?_ _
+    simp [crAnStatesToCreateAnnihilate]
+  | .posAsymp φ =>
+    simp
+
+lemma normalOrder_mul_anPart (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
+    normalOrder (a * anPart (StateAlgebra.ofState φ)) =
+    normalOrder a * anPart (StateAlgebra.ofState φ) := by
+  match φ with
+  | .negAsymp φ =>
+    simp
+  | .position φ =>
+    dsimp only [anPart, StateAlgebra.ofState]
+    simp only [FreeAlgebra.lift_ι_apply]
+    refine normalOrder_mul_annihilate _ ?_ _
+    simp [crAnStatesToCreateAnnihilate]
+  | .posAsymp φ =>
+    dsimp only [anPart, StateAlgebra.ofState]
+    simp only [FreeAlgebra.lift_ι_apply]
+    refine normalOrder_mul_annihilate _ ?_ _
+    simp [crAnStatesToCreateAnnihilate]
+
+/-!
+
+## Normal ordering for an adjacent creation and annihliation state
+
+The main result of this section is `normalOrder_superCommute_annihilate_create`.
+-/
+
 lemma normalOrder_swap_create_annihlate_ofCrAnList_ofCrAnList (φc φa : 𝓕.CrAnStates)
-    (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create)
-    (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
+    (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
     (φs φs' : List 𝓕.CrAnStates) :
     normalOrder (ofCrAnList φs' * ofCrAnState φc * ofCrAnState φa * ofCrAnList φs) =
     𝓢(𝓕 |>ₛ φc, 𝓕 |>ₛ φa) •
@@ -111,8 +158,7 @@ lemma normalOrder_swap_create_annihlate_ofCrAnList_ofCrAnList (φc φa : 𝓕.Cr
   noncomm_ring
 
 lemma normalOrder_swap_create_annihlate_ofCrAnList (φc φa : 𝓕.CrAnStates)
-    (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create)
-    (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
+    (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
     (φs : List 𝓕.CrAnStates) (a : 𝓕.CrAnAlgebra) :
     normalOrder (ofCrAnList φs * ofCrAnState φc * ofCrAnState φa * a) =
     𝓢(𝓕 |>ₛ φc, 𝓕 |>ₛ φa) •
@@ -129,8 +175,7 @@ lemma normalOrder_swap_create_annihlate_ofCrAnList (φc φa : 𝓕.CrAnStates)
   rfl
 
 lemma normalOrder_swap_create_annihlate (φc φa : 𝓕.CrAnStates)
-    (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create)
-    (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
+    (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
     (a b : 𝓕.CrAnAlgebra) :
     normalOrder (a * ofCrAnState φc * ofCrAnState φa * b) =
     𝓢(𝓕 |>ₛ φc, 𝓕 |>ₛ φa) •
@@ -149,11 +194,10 @@ lemma normalOrder_swap_create_annihlate (φc φa : 𝓕.CrAnStates)
   rfl
 
 lemma normalOrder_superCommute_create_annihilate (φc φa : 𝓕.CrAnStates)
-    (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create)
-    (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
+    (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
     (a b : 𝓕.CrAnAlgebra) :
     normalOrder (a * superCommute (ofCrAnState φc) (ofCrAnState φa) * b) = 0 := by
-  rw [superCommute_ofCrAnState]
+  rw [superCommute_ofCrAnState_ofCrAnState]
   simp only [instCommGroup.eq_1, Algebra.smul_mul_assoc]
   rw [mul_sub, sub_mul, map_sub, ← smul_mul_assoc]
   rw [← mul_assoc, ← mul_assoc]
@@ -162,49 +206,15 @@ lemma normalOrder_superCommute_create_annihilate (φc φa : 𝓕.CrAnStates)
     map_smul, sub_self]
 
 lemma normalOrder_superCommute_annihilate_create (φc φa : 𝓕.CrAnStates)
-    (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create)
-    (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
+    (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
     (a b : 𝓕.CrAnAlgebra) :
     normalOrder (a * superCommute (ofCrAnState φa) (ofCrAnState φc) * b) = 0 := by
-  rw [superCommute_ofCrAnState_symm]
+  rw [superCommute_ofCrAnState_ofCrAnState_symm]
   simp only [instCommGroup.eq_1, neg_smul, mul_neg, Algebra.mul_smul_comm, neg_mul,
     Algebra.smul_mul_assoc, map_neg, map_smul, neg_eq_zero, smul_eq_zero]
   apply Or.inr
   exact normalOrder_superCommute_create_annihilate φc φa hφc hφa a b
 
-lemma normalOrder_crPart_mul (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
-    normalOrder (crPart (StateAlgebra.ofState φ) * a) =
-    crPart (StateAlgebra.ofState φ) * normalOrder a := by
-  match φ with
-  | .negAsymp φ =>
-    dsimp only [crPart, StateAlgebra.ofState]
-    simp only [FreeAlgebra.lift_ι_apply]
-    exact normalOrder_create_mul ⟨States.negAsymp φ, ()⟩ rfl a
-  | .position φ =>
-    dsimp only [crPart, StateAlgebra.ofState]
-    simp only [FreeAlgebra.lift_ι_apply]
-    refine normalOrder_create_mul _ ?_ _
-    simp [crAnStatesToCreateAnnihilate]
-  | .posAsymp φ =>
-    simp
-
-lemma normalOrder_mul_anPart (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
-    normalOrder (a * anPart (StateAlgebra.ofState φ)) =
-    normalOrder a * anPart (StateAlgebra.ofState φ) := by
-  match φ with
-  | .negAsymp φ =>
-    simp
-  | .position φ =>
-    dsimp only [anPart, StateAlgebra.ofState]
-    simp only [FreeAlgebra.lift_ι_apply]
-    refine normalOrder_mul_annihilate _ ?_ _
-    simp [crAnStatesToCreateAnnihilate]
-  | .posAsymp φ =>
-    dsimp only [anPart, StateAlgebra.ofState]
-    simp only [FreeAlgebra.lift_ι_apply]
-    refine normalOrder_mul_annihilate _ ?_ _
-    simp [crAnStatesToCreateAnnihilate]
-
 lemma normalOrder_swap_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 𝓕) :
     normalOrder (a * (crPart (StateAlgebra.ofState φ)) * (anPart (StateAlgebra.ofState φ')) * b) =
     𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
@@ -240,6 +250,14 @@ lemma normalOrder_swap_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 
     rfl
     rfl
 
+/-!
+
+## Normal ordering for an anPart and crPart
+
+Using the results from above.
+
+-/
+
 lemma normalOrder_swap_anPart_crPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 𝓕) :
     normalOrder (a * (anPart (StateAlgebra.ofState φ)) * (crPart (StateAlgebra.ofState φ')) * b) =
     𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • normalOrder (a * (crPart (StateAlgebra.ofState φ')) *
@@ -290,15 +308,80 @@ lemma normalOrder_superCommute_anPart_crPart (φ φ' : 𝓕.States) (a b : CrAnA
     simp only [anPart_posAsymp, crPart_position]
     refine normalOrder_superCommute_annihilate_create _ _ (by rfl) (by rfl) _ _
 
+/-!
+
+## The normal ordering of a product of two states
+
+-/
+
+@[simp]
+lemma normalOrder_crPart_mul_crPart (φ φ' : 𝓕.States) :
+    normalOrder (crPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ')) =
+    crPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ') := by
+  rw [normalOrder_crPart_mul]
+  conv_lhs => rw [← mul_one (crPart (StateAlgebra.ofState φ'))]
+  rw [normalOrder_crPart_mul, normalOrder_one]
+  simp
+
+@[simp]
+lemma normalOrder_anPart_mul_anPart (φ φ' : 𝓕.States) :
+    normalOrder (anPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ')) =
+    anPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') := by
+  rw [normalOrder_mul_anPart]
+  conv_lhs => rw [← one_mul (anPart (StateAlgebra.ofState φ))]
+  rw [normalOrder_mul_anPart, normalOrder_one]
+  simp
+
+@[simp]
+lemma normalOrder_crPart_mul_anPart (φ φ' : 𝓕.States) :
+    normalOrder (crPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ')) =
+    crPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') := by
+  rw [normalOrder_crPart_mul]
+  conv_lhs => rw [← one_mul (anPart (StateAlgebra.ofState φ'))]
+  rw [normalOrder_mul_anPart, normalOrder_one]
+  simp
+
+@[simp]
+lemma normalOrder_anPart_mul_crPart (φ φ' : 𝓕.States) :
+    normalOrder (anPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ')) =
+    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
+    (crPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ)) := by
+  conv_lhs => rw [← one_mul (anPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ'))]
+  conv_lhs => rw [← mul_one (1 * (anPart (StateAlgebra.ofState φ) *
+    crPart (StateAlgebra.ofState φ')))]
+  rw [← mul_assoc, normalOrder_swap_anPart_crPart]
+  simp
+
+lemma normalOrder_ofState_mul_ofState (φ φ' : 𝓕.States) :
+    normalOrder (ofState φ * ofState φ') =
+    crPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ') +
+    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
+    (crPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ)) +
+    crPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') +
+    anPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') := by
+  rw [ofState_eq_crPart_add_anPart, ofState_eq_crPart_add_anPart]
+  rw [mul_add, add_mul, add_mul]
+  simp only [map_add, normalOrder_crPart_mul_crPart, normalOrder_anPart_mul_crPart,
+    instCommGroup.eq_1, normalOrder_crPart_mul_anPart, normalOrder_anPart_mul_anPart]
+  abel
+
+/-!
+
+## Normal order with super commutors
+
+-/
+
+/-! TODO: Split the following two lemmas up into smaller parts. -/
+
 lemma normalOrder_superCommute_ofCrAnList_create_create_ofCrAnList
     (φc φc' : 𝓕.CrAnStates) (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create)
     (hφc' : 𝓕 |>ᶜ φc' = CreateAnnihilate.create) (φs φs' : List 𝓕.CrAnStates) :
     (normalOrder (ofCrAnList φs *
-    superCommute (ofCrAnState φc) (ofCrAnState φc') * ofCrAnList φs')) =
+      superCommute (ofCrAnState φc) (ofCrAnState φc') * ofCrAnList φs')) =
       normalOrderSign (φs ++ φc' :: φc :: φs') •
     (ofCrAnList (createFilter φs) * superCommute (ofCrAnState φc) (ofCrAnState φc') *
       ofCrAnList (createFilter φs') * ofCrAnList (annihilateFilter (φs ++ φs'))) := by
-  rw [superCommute_ofCrAnState]
+  rw [superCommute_ofCrAnState_ofCrAnState]
   rw [mul_sub, sub_mul, map_sub]
   conv_lhs =>
     lhs
@@ -372,7 +455,7 @@ lemma normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList
     (ofCrAnList (createFilter (φs ++ φs'))
       * ofCrAnList (annihilateFilter φs) * superCommute (ofCrAnState φa) (ofCrAnState φa')
       * ofCrAnList (annihilateFilter φs')) := by
-  rw [superCommute_ofCrAnState]
+  rw [superCommute_ofCrAnState_ofCrAnState]
   rw [mul_sub, sub_mul, map_sub]
   conv_lhs =>
     lhs
@@ -440,62 +523,17 @@ lemma normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList
   rw [ofCrAnList_append, ofCrAnList_singleton, ofCrAnList_singleton]
   rw [ofCrAnList_append, ofCrAnList_singleton, ofCrAnList_singleton, smul_mul_assoc]
 
-@[simp]
-lemma normalOrder_crPart_mul_crPart (φ φ' : 𝓕.States) :
-    normalOrder (crPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ')) =
-    crPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ') := by
-  rw [normalOrder_crPart_mul]
-  conv_lhs => rw [← mul_one (crPart (StateAlgebra.ofState φ'))]
-  rw [normalOrder_crPart_mul, normalOrder_one]
-  simp
-
-@[simp]
-lemma normalOrder_anPart_mul_anPart (φ φ' : 𝓕.States) :
-    normalOrder (anPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ')) =
-    anPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') := by
-  rw [normalOrder_mul_anPart]
-  conv_lhs => rw [← one_mul (anPart (StateAlgebra.ofState φ))]
-  rw [normalOrder_mul_anPart, normalOrder_one]
-  simp
-
-@[simp]
-lemma normalOrder_crPart_mul_anPart (φ φ' : 𝓕.States) :
-    normalOrder (crPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ')) =
-    crPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') := by
-  rw [normalOrder_crPart_mul]
-  conv_lhs => rw [← one_mul (anPart (StateAlgebra.ofState φ'))]
-  rw [normalOrder_mul_anPart, normalOrder_one]
-  simp
+/-!
 
-@[simp]
-lemma normalOrder_anPart_mul_crPart (φ φ' : 𝓕.States) :
-    normalOrder (anPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ')) =
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
-    (crPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ)) := by
-  conv_lhs => rw [← one_mul (anPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ'))]
-  conv_lhs => rw [← mul_one (1 * (anPart (StateAlgebra.ofState φ) *
-    crPart (StateAlgebra.ofState φ')))]
-  rw [← mul_assoc, normalOrder_swap_anPart_crPart]
-  simp
+## Super commututators involving a normal order.
 
-lemma normalOrder_ofState_mul_ofState (φ φ' : 𝓕.States) :
-    normalOrder (ofState φ * ofState φ') =
-    crPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ') +
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
-    (crPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ)) +
-    crPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') +
-    anPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') := by
-  rw [ofState_eq_crPart_add_anPart, ofState_eq_crPart_add_anPart]
-  rw [mul_add, add_mul, add_mul]
-  simp only [map_add, normalOrder_crPart_mul_crPart, normalOrder_anPart_mul_crPart,
-    instCommGroup.eq_1, normalOrder_crPart_mul_anPart, normalOrder_anPart_mul_anPart]
-  abel
+-/
 
 lemma ofCrAnList_superCommute_normalOrder_ofCrAnList (φs φs' : List 𝓕.CrAnStates) :
     ⟨ofCrAnList φs, normalOrder (ofCrAnList φs')⟩ₛca =
     ofCrAnList φs * normalOrder (ofCrAnList φs') -
     𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • normalOrder (ofCrAnList φs') * ofCrAnList φs := by
-  simp [normalOrder_ofCrAnList, map_smul, superCommute_ofCrAnList, ofCrAnList_append,
+  simp [normalOrder_ofCrAnList, map_smul, superCommute_ofCrAnList_ofCrAnList, ofCrAnList_append,
     smul_sub, smul_smul, mul_comm]
 
 lemma ofCrAnList_superCommute_normalOrder_ofStateList (φs : List 𝓕.CrAnStates)
@@ -509,6 +547,12 @@ lemma ofCrAnList_superCommute_normalOrder_ofStateList (φs : List 𝓕.CrAnState
   rw [ofCrAnList_superCommute_normalOrder_ofCrAnList,
     CrAnSection.statistics_eq_state_statistics]
 
+/-!
+
+## Multiplications with normal order written in terms of super commute.
+
+-/
+
 lemma ofCrAnList_mul_normalOrder_ofStateList_eq_superCommute (φs : List 𝓕.CrAnStates)
     (φs' : List 𝓕.States) :
     ofCrAnList φs * normalOrder (ofStateList φs') =