Merge pull request #317 from HEPLean/WickTheoremDoc

refactor: Wick theorem docs

HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean

@@ -216,6 +216,11 @@ lemma anPart_mul_normalOrder_ofFieldOpList_eq_superCommute (φ : 𝓕.FieldOp)
 
 -/
 
+/--
+The proof of this result ultimetly depends on
+- `superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum`
+- `normalOrderSign_eraseIdx`
+-/
 lemma ofCrAnFieldOp_superCommute_normalOrder_ofCrAnFieldOpList_sum (φ : 𝓕.CrAnFieldOp)
     (φs : List 𝓕.CrAnFieldOp) : [ofCrAnFieldOp φ, 𝓝(ofCrAnFieldOpList φs)]ₛ = ∑ n : Fin φs.length,
     𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (φs.take n)) • [ofCrAnFieldOp φ, ofCrAnFieldOp φs[n]]ₛ
@@ -329,6 +334,9 @@ noncomputable def contractStateAtIndex (φ : 𝓕.FieldOp) (φs : List 𝓕.Fiel
 /--
 For a field specification `𝓕`, the following relation holds in the algebra `𝓕.FieldOpAlgebra`,
 `φ * 𝓝(φ₀φ₁…φₙ) = 𝓝(φφ₀φ₁…φₙ) + ∑ i, (𝓢(φ,φ₀φ₁…φᵢ₋₁) • [anPartF φ, φᵢ]ₛ) * 𝓝(φ₀φ₁…φᵢ₋₁φᵢ₊₁…φₙ)`.
+
+The proof of this ultimently depends on :
+- `ofCrAnFieldOp_superCommute_normalOrder_ofCrAnFieldOpList_sum`
 -/
 lemma ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :
     ofFieldOp φ * 𝓝(ofFieldOpList φs) =

HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean

@@ -12,8 +12,6 @@ import HepLean.PerturbationTheory.WickContraction.StaticContract
 # Static Wick's terms
 
 -/
-
-
 open FieldSpecification
 variable {𝓕 : FieldSpecification}
 
@@ -29,21 +27,45 @@ noncomputable section
 def staticWickTerm {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : 𝓕.FieldOpAlgebra :=
   φsΛ.sign • φsΛ.staticContract * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ)
 
+/-- The static Wick term for the empty contraction of the empty list is `1`. -/
 @[simp]
 lemma staticWickTerm_empty_nil  :
     staticWickTerm (empty (n := ([] : List 𝓕.FieldOp).length)) = 1 := by
   rw [staticWickTerm, uncontractedListGet, nil_zero_uncontractedList]
   simp [sign, empty, staticContract]
 
+/--
+Let `φsΛ` be a Wick Contraction for `φs = φ₀φ₁…φₙ`. Then the following holds
+`(φsΛ ↩Λ φ 0 none).staticWickTerm = φsΛ.sign • φsΛ.staticWickTerm * 𝓝(φ :: [φsΛ]ᵘᶜ)`
+
+The proof of this result relies on
+- `staticContract_insert_none` to rewrite the static contract.
+- `sign_insert_none_zero` to rewrite the sign.
+-/
 lemma staticWickTerm_insert_zero_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) :
     (φsΛ ↩Λ φ 0 none).staticWickTerm =
     φsΛ.sign • φsΛ.staticContract * 𝓝(ofFieldOpList (φ :: [φsΛ]ᵘᶜ)) := by
   symm
   erw [staticWickTerm, sign_insert_none_zero]
-  simp only [staticContract_insertAndContract_none, insertAndContract_uncontractedList_none_zero,
+  simp only [staticContract_insert_none, insertAndContract_uncontractedList_none_zero,
     Algebra.smul_mul_assoc]
 
+/-- Let `φsΛ` be a Wick contraction for `φs = φ₀φ₁…φₙ`.  Then`(φsΛ ↩Λ φ 0 (some k)).wickTerm`
+is equal the product of
+- the sign `𝓢(φ, φ₀…φᵢ₋₁) `
+- the sign `φsΛ.sign`
+- `φsΛ.staticContract`
+- `s • [anPart φ, ofFieldOp φs[k]]ₛ` where `s` is the sign associated with moving `φ` through
+  uncontracted fields in `φ₀…φₖ₋₁`
+- the normal ordering `𝓝([φsΛ]ᵘᶜ.erase (uncontractedFieldOpEquiv φs φsΛ k))`.
+
+The proof of this result relies on
+- `staticContract_insert_some_of_lt` to rewrite static
+ contractions.
+- `normalOrder_uncontracted_some` to rewrite normal orderings.
+- `sign_insert_some_zero` to rewrite signs.
+-/
 lemma staticWickTerm_insert_zero_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (k : { x // x ∈ φsΛ.uncontracted }) :
     (φsΛ ↩Λ φ 0 k).staticWickTerm =
@@ -55,23 +77,16 @@ lemma staticWickTerm_insert_zero_some (φ : 𝓕.FieldOp) (φs : List 𝓕.Field
   simp only [← mul_assoc]
   rw [← smul_mul_assoc]
   congr 1
-  rw [staticContract_insertAndContract_some_eq_mul_contractStateAtIndex_lt]
+  rw [staticContract_insert_some_of_lt]
   swap
   · simp
   rw [smul_smul]
   by_cases hn : GradingCompliant φs φsΛ ∧ (𝓕|>ₛφ) = (𝓕|>ₛ φs[k.1])
   · congr 1
     swap
-    · have h1 := φsΛ.staticContract.2
-      rw [@Subalgebra.mem_center_iff] at h1
-      rw [h1]
-    erw [sign_insert_some]
-    rw [mul_assoc, mul_comm φsΛ.sign, ← mul_assoc]
-    rw [signInsertSome_mul_filter_contracted_of_not_lt]
-    simp only [instCommGroup.eq_1, Fin.zero_succAbove, Fin.not_lt_zero, Finset.filter_False,
-      ofFinset_empty, map_one, one_mul]
-    simp only [Fin.zero_succAbove, Fin.not_lt_zero, not_false_eq_true]
-    exact hn
+    · rw [Subalgebra.mem_center_iff.mp φsΛ.staticContract.2]
+    · rw [sign_insert_some_zero _ _ _ _ hn, mul_comm, ← mul_assoc]
+      simp
   · simp only [Fin.getElem_fin, not_and] at hn
     by_cases h0 : ¬ GradingCompliant φs φsΛ
     · rw [staticContract_of_not_gradingCompliant]
@@ -90,6 +105,18 @@ lemma staticWickTerm_insert_zero_some (φ : 𝓕.FieldOp) (φs : List 𝓕.Field
       rw [h1]
       simp
 
+
+/--
+Let `φsΛ` be a Wick contraction for `φs = φ₀φ₁…φₙ`.  Then
+`φ * φsΛ.staticWickTerm = ∑ k, (φsΛ ↩Λ φ i k).wickTerm`
+where the sum is over all `k` in `Option φsΛ.uncontracted` (so either `none` or `some k`).
+
+The proof of proceeds as follows:
+- `ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum` is used to expand  `φ 𝓝([φsΛ]ᵘᶜ)` as
+  a sum over `k` in `Option φsΛ.uncontracted` of terms involving `[φ, φs[k]]` etc.
+- Then `staticWickTerm_insert_zero_none` and `staticWickTerm_insert_zero_some` are
+  used to equate terms.
+-/
 lemma mul_staticWickTerm_eq_sum (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) :
     ofFieldOp φ * φsΛ.staticWickTerm =
@@ -107,7 +134,7 @@ lemma mul_staticWickTerm_eq_sum (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
   | none =>
     simp only [contractStateAtIndex, uncontractedFieldOpEquiv, Equiv.optionCongr_apply,
       Equiv.coe_trans, Option.map_none', one_mul, Algebra.smul_mul_assoc, Nat.succ_eq_add_one,
-      Fin.zero_eta, Fin.val_zero, List.insertIdx_zero, staticContract_insertAndContract_none,
+      Fin.zero_eta, Fin.val_zero, List.insertIdx_zero, staticContract_insert_none,
       insertAndContract_uncontractedList_none_zero]
     rw [staticWickTerm_insert_zero_none]
     simp only [Algebra.smul_mul_assoc]

HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean

@@ -29,6 +29,7 @@ noncomputable section
 def wickTerm {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : 𝓕.FieldOpAlgebra :=
   φsΛ.sign • φsΛ.timeContract * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ)
 
+/-- The Wick term for the empty contraction of the empty list is `1`. -/
 @[simp]
 lemma wickTerm_empty_nil  :
     wickTerm (empty (n := ([] : List 𝓕.FieldOp).length)) = 1 := by
@@ -36,23 +37,13 @@ lemma wickTerm_empty_nil  :
   simp [sign_empty]
 
 /--
-Let `φsΛ` be a Wick Contraction for `φs = φ₀φ₁…φₙ`. Then the wick-term of ` (φsΛ ↩Λ φ i none)`
+Let `φsΛ` be a Wick Contraction for `φs = φ₀φ₁…φₙ`. Then the following holds
+`(φsΛ ↩Λ φ i none).wickTerm = 𝓢(φ, φ₀…φᵢ₋₁) φsΛ.sign • φsΛ.timeContract * 𝓝(φ :: [φsΛ]ᵘᶜ)`
 
-```(φsΛ ↩Λ φ i none).sign • (φsΛ ↩Λ φ i none).timeContract 𝓞 * 𝓞.crAnF 𝓝ᶠ([φsΛ ↩Λ φ i none]ᵘᶜ)```
-
-is equal to
-
-`s • (φsΛ.sign • φsΛ.timeContract 𝓞 * 𝓞.crAnF 𝓝ᶠ(φ :: [φsΛ]ᵘᶜ))`
-
-where `s` is the exchange sign of `φ` and the uncontracted fields in `φ₀φ₁…φᵢ₋₁`.
-
-The proof of this result relies primarily on:
-- `normalOrderF_uncontracted_none` which replaces `𝓝ᶠ([φsΛ ↩Λ φ i none]ᵘᶜ)` with
-  `𝓝ᶠ(φ :: [φsΛ]ᵘᶜ)` up to a sign.
-- `timeContract_insertAndContract_none` which replaces `(φsΛ ↩Λ φ i none).timeContract 𝓞` with
-  `φsΛ.timeContract 𝓞`.
-- `sign_insert_none` and `signInsertNone_eq_filterset` which are used to take account of
-  signs.
+The proof of this result relies on
+- `normalOrder_uncontracted_none` to rewrite normal orderings.
+- `timeContract_insert_none` to rewrite the time contract.
+- `sign_insert_none` to rewrite the sign.
 -/
 lemma wickTerm_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) :
@@ -62,7 +53,7 @@ lemma wickTerm_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
   rw [wickTerm]
   by_cases hg : GradingCompliant φs φsΛ
   · rw [normalOrder_uncontracted_none, sign_insert_none  _ _ _ _ hg]
-    simp only [Nat.succ_eq_add_one, timeContract_insertAndContract_none, instCommGroup.eq_1,
+    simp only [Nat.succ_eq_add_one, timeContract_insert_none, instCommGroup.eq_1,
       Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_smul]
     congr 1
     rw [← mul_assoc]
@@ -89,18 +80,29 @@ lemma wickTerm_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
       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_insertAndContract_none, Algebra.smul_mul_assoc,
+  · simp only [Nat.succ_eq_add_one, timeContract_insert_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 ↩Λ φ i (some k)` is equal to that for just `c`
-mulitiplied by the exchange sign of `φ` and `φ₀φ₁…φᵢ₋₁`.
+/-- Let `φsΛ` be a Wick contraction for `φs = φ₀φ₁…φₙ`. Let `φ` be a field with time
+greater then or equal to all the fields in `φs`. Let `i` be a in `Fin φs.length.succ` such that
+all files in `φ₀…φᵢ₋₁` have time strictly less then `φ`. Then`(φsΛ ↩Λ φ i (some k)).wickTerm`
+is equal the product of
+- the sign `𝓢(φ, φ₀…φᵢ₋₁) `
+- the sign `φsΛ.sign`
+- `φsΛ.timeContract`
+- `s • [anPart φ, ofFieldOp φs[k]]ₛ` where `s` is the sign associated with moving `φ` through
+  uncontracted fields in `φ₀…φₖ₋₁`
+- the normal ordering `𝓝([φsΛ]ᵘᶜ.erase (uncontractedFieldOpEquiv φs φsΛ k))`.
+
+The proof of this result relies on
+- `timeContract_insert_some_of_not_lt`
+ and `timeContract_insert_some_of_lt` to rewrite time
+ contractions.
+- `normalOrder_uncontracted_some` to rewrite normal orderings.
+- `sign_insert_some_of_not_lt` and `sign_insert_some_of_lt` to rewrite signs.
 -/
 lemma wickTerm_insert_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) (k : φsΛ.uncontracted)
@@ -114,7 +116,7 @@ lemma wickTerm_insert_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
   rw [wickTerm]
   by_cases hg : GradingCompliant φs φsΛ ∧ (𝓕 |>ₛ φ) = (𝓕 |>ₛ φs[k.1])
   · by_cases hk : i.succAbove k < i
-    · rw [WickContraction.timeContract_insertAndContract_some_eq_mul_contractStateAtIndex_not_lt]
+    · rw [WickContraction.timeContract_insert_some_of_not_lt]
       swap
       · exact hn _ hk
       · rw [normalOrder_uncontracted_some, sign_insert_some_of_lt φ φs φsΛ i k hk hg]
@@ -124,7 +126,7 @@ lemma wickTerm_insert_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
         simp
       · omega
     · have hik : i.succAbove ↑k ≠ i := Fin.succAbove_ne i ↑k
-      rw [timeContract_insertAndContract_some_eq_mul_contractStateAtIndex_lt]
+      rw [timeContract_insert_some_of_lt]
       swap
       · exact hlt _
       · rw [normalOrder_uncontracted_some]
@@ -164,17 +166,16 @@ lemma wickTerm_insert_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
       exact hg'
 
 /--
-Given a Wick contraction `φsΛ` of `φs = φ₀φ₁…φₙ` and an `i`, we have that
-`(φsΛ.sign • φsΛ.timeContract 𝓞) * 𝓞.crAnF (φ * 𝓝ᶠ([φsΛ]ᵘᶜ))`
-is equal to the product of
-- the exchange sign of `φ` and `φ₀φ₁…φᵢ₋₁`,
-- the sum of `((φsΛ ↩Λ φ i k).sign • (φsΛ ↩Λ φ i k).timeContract 𝓞) * 𝓞.crAnF 𝓝ᶠ([φsΛ ↩Λ φ i k]ᵘᶜ)`
-  over all `k` in `Option φsΛ.uncontracted`.
+Let `φsΛ` be a Wick contraction for `φs = φ₀φ₁…φₙ`. Let `φ` be a field with time
+greater then or equal to all the fields in `φs`. Let `i` be a in `Fin φs.length.succ` such that
+all files in `φ₀…φᵢ₋₁` have time strictly less then `φ`. Then
+`φ * φsΛ.wickTerm = 𝓢(φ, φ₀…φᵢ₋₁) • ∑ k, (φsΛ ↩Λ φ i k).wickTerm`
+where the sum is over all `k` in `Option φsΛ.uncontracted` (so either `none` or `some k`).
 
-The proof of this result primarily depends on
-- `crAnF_ofFieldOpF_mul_normalOrderF_ofFieldOpFsList_eq_sum` to rewrite `𝓞.crAnF (φ * 𝓝ᶠ([φsΛ]ᵘᶜ))`
-- `wick_term_none_eq_wick_term_cons`
-- `wick_term_some_eq_wick_term_optionEraseZ`
+The proof of proceeds as follows:
+- `ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum` is used to expand  `φ 𝓝([φsΛ]ᵘᶜ)` as
+  a sum over `k` in `Option φsΛ.uncontracted` of terms involving `[φ, φs[k]]` etc.
+- Then `wickTerm_insert_none` and `wickTerm_insert_some` are used to equate terms.
 -/
 lemma mul_wickTerm_eq_sum (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (i : Fin φs.length.succ)
     (φsΛ : WickContraction φs.length) (hlt : ∀ (k : Fin φs.length), timeOrderRel φ φs[k])

HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean

@@ -101,7 +101,7 @@ theorem wicks_theorem : (φs : List 𝓕.FieldOp) → 𝓣(ofFieldOpList φs) =
     · 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_insertAndContract_none,
+      Algebra.smul_mul_assoc, Fintype.sum_option, timeContract_insert_none,
       Finset.univ_eq_attach, smul_add, one_smul, uncontractedListGet]
     · exact fun k => timeOrder_maxTimeField _ _ k
     · exact fun k => lt_maxTimeFieldPosFin_not_timeOrder _ _ k

HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean

@@ -24,11 +24,15 @@ open HepLean.Fin
 
 -/
 
-/-- Given a Wick contraction `c` associated to a list `φs`,
-  a position `i : Fin n.succ`, an element `φ`, and an optional uncontracted element
-  `j : Option (c.uncontracted)` of `c`.
-  The Wick contraction associated with `(φs.insertIdx i φ).length` formed by 'inserting' `φ`
-  into `φs` after the first `i` elements and contracting it optionally with j. -/
+/-- Given a Wick contraction `φsΛ` associated to a list `φs`,
+    a position `i : Fin φs.lengthsucc`, an element `φ`, and an optional uncontracted element
+  `j : Option (φsΛ.uncontracted)` of `φsΛ`.
+  The Wick contraction `φsΛ.insertAndContract φ i j` is defined to be the Wick contraction
+  associated with `(φs.insertIdx i φ)` formed by 'inserting' `φ` into `φs` after the first `i`
+  elements and contracting `φ` optionally with `j`.
+
+  The notation `φsΛ ↩Λ φ i j` is used to denote `φsΛ.insertAndContract φ i j`. Thus,
+  `φsΛ ↩Λ φ i none` indicates the case when we insert `φ` into `φs` but do not contract it.  -/
 def insertAndContract {φs : List 𝓕.FieldOp} (φ : 𝓕.FieldOp) (φsΛ : WickContraction φs.length)
     (i : Fin φs.length.succ) (j : Option φsΛ.uncontracted) :
     WickContraction (φs.insertIdx i φ).length :=

HepLean/PerturbationTheory/WickContraction/Sign/InsertNone.lean

@@ -157,11 +157,6 @@ lemma signInsertNone_eq_prod_prod (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
   erw [hG a]
   rfl
 
-lemma sign_insert_none_zero (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
-    (φsΛ : WickContraction φs.length) : (φsΛ ↩Λ φ 0 none).sign = φsΛ.sign := by
-  rw [sign_insert_none_eq_signInsertNone_mul_sign]
-  simp [signInsertNone]
-
 lemma signInsertNone_eq_prod_getDual?_Some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (hG : GradingCompliant φs φsΛ) :
     φsΛ.signInsertNone φ φs i = ∏ (x : Fin φs.length),
@@ -255,4 +250,9 @@ lemma sign_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
   rw [signInsertNone_eq_filterset]
   exact hG
 
+lemma sign_insert_none_zero (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
+    (φsΛ : WickContraction φs.length) : (φsΛ ↩Λ φ 0 none).sign = φsΛ.sign := by
+  rw [sign_insert_none_eq_signInsertNone_mul_sign]
+  simp [signInsertNone]
+
 end WickContraction

HepLean/PerturbationTheory/WickContraction/Sign/InsertSome.lean

@@ -901,4 +901,15 @@ lemma sign_insert_some_of_not_lt (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
   rw [mul_comm, ← mul_assoc]
   simp
 
+lemma sign_insert_some_zero (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
+    (φsΛ : WickContraction φs.length) (k : φsΛ.uncontracted)
+    (hn : GradingCompliant φs φsΛ ∧ (𝓕|>ₛφ) = 𝓕|>ₛφs[k.1]):
+    (φsΛ ↩Λ φ 0 k).sign =  𝓢(𝓕|>ₛφ, 𝓕 |>ₛ ⟨φs.get, (φsΛ.uncontracted.filter (fun x => x < ↑k))⟩) *
+    φsΛ.sign := by
+  rw [sign_insert_some_of_not_lt]
+  · simp
+  · simp
+  · exact hn
+
+
 end WickContraction

HepLean/PerturbationTheory/WickContraction/Sign/Join.lean

@@ -417,6 +417,11 @@ lemma join_sign_induction {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs
     apply sign_congr
     exact join_uncontractedListGet (singleton hij) φsucΛ'
 
+/-- Let `φsΛ` be a grading compliant Wick contraction for `φs` and
+  `φsucΛ` a Wick contraction for `[φsΛ]ᵘᶜ`. Then  `(join φsΛ φsucΛ).sign = φsΛ.sign * φsucΛ.sign`.
+
+  This lemma manifests the fact that it does not matter which order contracted pairs are brought
+  together when defining the sign of a contraction. -/
 lemma join_sign {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length)
     (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (hc : φsΛ.GradingCompliant) :
     (join φsΛ φsucΛ).sign = φsΛ.sign * φsucΛ.sign := by

HepLean/PerturbationTheory/WickContraction/StaticContract.lean

@@ -29,7 +29,7 @@ noncomputable def staticContract {φs : List 𝓕.FieldOp}
       superCommute_anPart_ofFieldOp_mem_center _ _⟩
 
 @[simp]
-lemma staticContract_insertAndContract_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
+lemma staticContract_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) :
     (φsΛ ↩Λ φ i none).staticContract = φsΛ.staticContract := by
   rw [staticContract, insertAndContract_none_prod_contractions]
@@ -66,7 +66,7 @@ lemma staticContract_insertAndContract_some
 
 open FieldStatistic
 
-lemma staticContract_insertAndContract_some_eq_mul_contractStateAtIndex_lt
+lemma staticContract_insert_some_of_lt
     (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted)
     (hik : i < i.succAbove k) :

HepLean/PerturbationTheory/WickContraction/TimeContract.lean

@@ -34,7 +34,7 @@ noncomputable def timeContract {φs : List 𝓕.FieldOp}
 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 (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
+lemma timeContract_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) :
     (φsΛ ↩Λ φ i none).timeContract = φsΛ.timeContract := by
   rw [timeContract, insertAndContract_none_prod_contractions]
@@ -77,7 +77,7 @@ lemma timeContract_empty (φs : List 𝓕.FieldOp) :
 
 open FieldStatistic
 
-lemma timeContract_insertAndContract_some_eq_mul_contractStateAtIndex_lt
+lemma timeContract_insert_some_of_lt
     (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted)
     (ht : 𝓕.timeOrderRel φ φs[k.1]) (hik : i < i.succAbove k) :
@@ -110,7 +110,7 @@ lemma timeContract_insertAndContract_some_eq_mul_contractStateAtIndex_lt
     simp only [exchangeSign_mul_self]
     · exact ht
 
-lemma timeContract_insertAndContract_some_eq_mul_contractStateAtIndex_not_lt
+lemma timeContract_insert_some_of_not_lt
     (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted)
     (ht : ¬ 𝓕.timeOrderRel φs[k.1] φ) (hik : ¬ i < i.succAbove k) :

scripts/MetaPrograms/notes.lean

@@ -117,7 +117,8 @@ def perturbationTheory : Note where
   title := "Proof of Wick's theorem"
   curators := ["Joseph Tooby-Smith"]
   parts := [
-    .warning "This note is a work in progress and is not finished. Use with caution.",
+    .warning "This note is a work in progress and is not finished. Use with caution.
+      (5th Feb 2025)",
     .h1 "Introduction",
     .name `FieldSpecification.wicks_theorem_context,
     .p "In this note we walk through the important parts of the proof of Wick's theorem
@@ -143,6 +144,7 @@ def perturbationTheory : Note where
     .name `FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF,
     .name `FieldSpecification.FieldOpFreeAlgebra.fieldOpFreeAlgebraGrade,
     .name `FieldSpecification.FieldOpFreeAlgebra.superCommuteF,
+    .name `FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum,
     .h2 "Field-operator algebra",
     .name `FieldSpecification.FieldOpAlgebra,
     .name `FieldSpecification.FieldOpAlgebra.fieldOpAlgebraGrade,
@@ -158,27 +160,54 @@ def perturbationTheory : Note where
     .name `FieldSpecification.normalOrderSign,
     .name `FieldSpecification.FieldOpFreeAlgebra.normalOrderF,
     .name `FieldSpecification.FieldOpAlgebra.normalOrder,
+    .h2 "Some lemmas",
+    .name `FieldSpecification.normalOrderSign_eraseIdx,
+    .name `FieldSpecification.FieldOpAlgebra.ofCrAnFieldOp_superCommute_normalOrder_ofCrAnFieldOpList_sum,
+    .name `FieldSpecification.FieldOpAlgebra.ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum,
     .h1 "Wick Contractions",
     .h2 "Definition",
     .name `WickContraction,
     .name `WickContraction.GradingCompliant,
-    .h2 "Cardinality",
+    .h2 "Aside: Cardinality",
     .name `WickContraction.card_eq_cardFun,
     .h2 "Constructors",
     .p "There are a number of ways to construct a Wick contraction from
       other Wick contractions or single contractions.",
     .name `WickContraction.insertAndContract,
-    .name `WickContraction.erase,
     .name `WickContraction.join,
     .h2 "Sign",
     .name `WickContraction.sign,
     .name `WickContraction.join_sign,
     .name `WickContraction.sign_insert_none,
+    .name `WickContraction.sign_insert_none_zero,
     .name `WickContraction.sign_insert_some_of_not_lt,
     .name `WickContraction.sign_insert_some_of_lt,
-    .h1 "Time and static contractions",
+    .name `WickContraction.sign_insert_some_zero,
+    .h2 "Normal order",
+    .name `FieldSpecification.FieldOpAlgebra.normalOrder_uncontracted_none,
+    .name `FieldSpecification.FieldOpAlgebra.normalOrder_uncontracted_some,
+    .h1 "Static contractions",
+    .name `WickContraction.staticContract,
+    .name `WickContraction.staticContract_insert_some_of_lt,
+    .name `WickContraction.staticContract_insert_none,
+    .h1 "Time contractions",
+    .name `FieldSpecification.FieldOpAlgebra.timeContract,
+    .name `WickContraction.timeContract,
+    .name `WickContraction.timeContract_insert_none,
+    .name `WickContraction.timeContract_insert_some_of_not_lt,
+    .name `WickContraction.timeContract_insert_some_of_lt,
     .h1 "Wick terms",
     .name `WickContraction.wickTerm,
+    .name `WickContraction.wickTerm_empty_nil,
+    .name `WickContraction.wickTerm_insert_none,
+    .name `WickContraction.wickTerm_insert_some,
+    .name `WickContraction.mul_wickTerm_eq_sum,
+    .h1 "Static wick terms",
+    .name `WickContraction.staticWickTerm,
+    .name `WickContraction.staticWickTerm_empty_nil,
+    .name `WickContraction.staticWickTerm_insert_zero_none,
+    .name `WickContraction.staticWickTerm_insert_zero_some,
+    .name `WickContraction.mul_staticWickTerm_eq_sum,
     .h1 "The three Wick's theorems",
     .name `FieldSpecification.wicks_theorem,
     .name `FieldSpecification.FieldOpAlgebra.static_wick_theorem,