docs: More docs related to Wicks theorem

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) :