docs: Notes for normal-ordered Wicks

HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean

@@ -284,6 +284,14 @@ lemma insert_fin_eq_self (φ : 𝓕.FieldOp) {φs : List 𝓕.FieldOp}
     use z
     rfl
 
+/-- For a list `φs` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
+  `𝓕.FieldOp`,  a `i ≤ φs.length` a sum over
+  Wick contractions of `φs` with `φ` inserted at `i` is equal to the sum over Wick contractions
+  `φsΛ` of just `φs` and the sum over optional uncontracted elements of the `φsΛ`.
+
+  I.e. `∑ (φsΛ : WickContraction (φs.insertIdx i φ).length), f φsΛ` is equal to
+  `∑ (φsΛ : WickContraction φs.length), ∑ (k : Option φsΛ.uncontracted), f (φsΛ ↩Λ φ i k) `.
+  where `(φs.insertIdx i φ)` is `φs` with `φ` inserted at position `i`. -/
 lemma insertLift_sum (φ : 𝓕.FieldOp) {φs : List 𝓕.FieldOp}
     (i : Fin φs.length.succ) [AddCommMonoid M] (f : WickContraction (φs.insertIdx i φ).length → M) :
     ∑ c, f c =

HepLean/PerturbationTheory/WickContraction/Sign/Join.lean

@@ -429,6 +429,11 @@ lemma join_sign {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length)
     (join φsΛ φsucΛ).sign = φsΛ.sign * φsucΛ.sign := by
   exact join_sign_induction φsΛ φsucΛ hc (φsΛ).1.card rfl
 
+/-- For a list `φs` of `𝓕.FieldOp`, a  Wick contraction `φsΛ` of `φs`,
+  and a Wick contraction `φsucΛ` of `[φsΛ]ᵘᶜ`,
+  `(join φsΛ φsucΛ).sign • (join φsΛ φsucΛ).timeContract` is equal to the product of
+  - `φsΛ.sign • φsΛ.timeContract` and
+  - `φsucΛ.sign • φsucΛ.timeContract`. -/
 lemma join_sign_timeContract {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length)
     (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) :
     (join φsΛ φsucΛ).sign • (join φsΛ φsucΛ).timeContract.1 =

HepLean/PerturbationTheory/WickContraction/StaticContract.lean

@@ -18,9 +18,11 @@ namespace WickContraction
 variable {n : ℕ} (c : WickContraction n)
 open HepLean.List
 open FieldOpAlgebra
-/-- Given a Wick contraction `φsΛ` associated with a list `φs`, the
-  product of all time-contractions of pairs of contracted elements in `φs`,
-  as a member of the center of `𝓞.A`. -/
+
+/-- For a list `φs` of `𝓕.FieldOp` and a Wick contraction `φsΛ` the
+  element of the center of `𝓕.FieldOpAlgebra`, `φsΛ.staticContract` is defined as the product
+  of `[anPart φs[j], φs[k]]ₛ` over contracted pairs `{j, k}` (both indices of `φs`) in `φsΛ`
+  with `j < k`. -/
 noncomputable def staticContract {φs : List 𝓕.FieldOp}
     (φsΛ : WickContraction φs.length) :
     Subalgebra.center ℂ 𝓕.FieldOpAlgebra :=
@@ -28,6 +30,13 @@ noncomputable def staticContract {φs : List 𝓕.FieldOp}
     ofFieldOp (φs.get (φsΛ.sndFieldOfContract a))]ₛ,
       superCommute_anPart_ofFieldOp_mem_center _ _⟩
 
+/-- For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
+  `𝓕.FieldOp`, and a `i ≤ φs.length`  the following relation holds
+
+  `(φsΛ ↩Λ φ i none).staticContract = φsΛ.staticContract`
+
+  The prove of this result ultimately a consequence of definitions.
+-/
 @[simp]
 lemma staticContract_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) :
@@ -37,15 +46,17 @@ lemma staticContract_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
   ext a
   simp
 
-/-- For `φsΛ` a Wick contraction for `φs = φ₀…φₙ`, the time contraction
-  `(φsΛ ↩Λ φ i (some j)).timeContract 𝓞` is equal to the multiple of
-- the time contraction of `φ` with `φⱼ` if `i < i.succAbove j` else
-    `φⱼ` with `φ`.
-- `φsΛ.timeContract 𝓞`.
-This follows from the fact that `(φsΛ ↩Λ φ i (some j))` has one more contracted pair than `φsΛ`,
-corresponding to `φ` contracted with `φⱼ`. The order depends on whether we insert `φ` before
-or after `φⱼ`. -/
-lemma staticContract_insertAndContract_some
+
+/--
+  For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
+  `𝓕.FieldOp`,  a `i ≤ φs.length` and a `k` in `φsΛ.uncontracted`, then
+  `(φsΛ ↩Λ φ i (some k)).staticContract` is equal to the product of
+  - `[anPart φ, φs[k]]ₛ` if `i ≤ k` or `[anPart φs[k], φ]ₛ` if `k < i`
+  - `φsΛ.staticContract`.
+
+  The proof of this result ultimately a consequence of definitions.
+-/
+lemma staticContract_insert_some
     (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) :
     (φsΛ ↩Λ φ i (some j)).staticContract =
@@ -74,7 +85,7 @@ lemma staticContract_insert_some_of_lt
     𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (φsΛ.uncontracted.filter (fun x => x < k))⟩)
     • (contractStateAtIndex φ [φsΛ]ᵘᶜ ((uncontractedFieldOpEquiv φs φsΛ) (some k)) *
       φsΛ.staticContract) := by
-  rw [staticContract_insertAndContract_some]
+  rw [staticContract_insert_some]
   simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul, instCommGroup.eq_1,
     contractStateAtIndex, uncontractedFieldOpEquiv, Equiv.optionCongr_apply,
     Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, Fin.coe_cast,

HepLean/PerturbationTheory/WickContraction/TimeCond.lean

@@ -96,6 +96,9 @@ lemma empty_mem {φs : List 𝓕.FieldOp} : empty (n := φs.length).EqTimeOnly :
   rw [eqTimeOnly_iff_forall_finset]
   simp [empty]
 
+/-- Let `φs` be a list of `𝓕.FieldOp` and `φsΛ` a `WickContraction` of `φs` with
+  in which every contraction involves two `FieldOp`s that have the same time. Then
+  `φsΛ.staticContract = φsΛ.timeContract`. -/
 lemma staticContract_eq_timeContract_of_eqTimeOnly (h : φsΛ.EqTimeOnly) :
     φsΛ.staticContract = φsΛ.timeContract := by
   simp only [staticContract, timeContract]
@@ -190,6 +193,12 @@ lemma timeOrder_timeContract_mul_of_eqTimeOnly_mid {φs : List 𝓕.FieldOp}
     𝓣(a * φsΛ.timeContract.1 * b) = φsΛ.timeContract.1 * 𝓣(a * b) := by
   exact timeOrder_timeContract_mul_of_eqTimeOnly_mid_induction φsΛ hl a b φsΛ.1.card rfl
 
+/-- Let `φs` be a list of `𝓕.FieldOp`, `φsΛ` a `WickContraction` of `φs` with
+  in which every contraction involves two `FieldOp`s that have the same time and
+  `b` a general element in `𝓕.FieldOpAlgebra`. Then
+  `𝓣(φsΛ.timeContract.1 * b) = φsΛ.timeContract.1 * 𝓣(b)`.
+
+  This follows from properties of orderings and the ideal defining `𝓕.FieldOpAlgebra`. -/
 lemma timeOrder_timeContract_mul_of_eqTimeOnly_left {φs : List 𝓕.FieldOp}
     (φsΛ : WickContraction φs.length)
     (hl : φsΛ.EqTimeOnly) (b : 𝓕.FieldOpAlgebra) :
@@ -238,6 +247,9 @@ lemma timeOrder_timeContract_of_not_eqTimeOnly {φs : List 𝓕.FieldOp}
   intro h
   simp_all
 
+/-- Let `φs` be a list of `𝓕.FieldOp` and `φsΛ` a `WickContraction` with
+  at least one contraction between `FieldOp` that do not have the same time. Then
+  `𝓣(φsΛ.staticContract.1) = 0`. -/
 lemma timeOrder_staticContract_of_not_mem {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length)
     (hl : ¬ φsΛ.EqTimeOnly) : 𝓣(φsΛ.staticContract.1) = 0 := by
   obtain ⟨i, j, hij, φsucΛ, rfl, hr⟩ := exists_join_singleton_of_not_eqTimeOnly φsΛ hl

HepLean/PerturbationTheory/WickContraction/TimeContract.lean

@@ -18,9 +18,11 @@ namespace WickContraction
 variable {n : ℕ} (c : WickContraction n)
 open HepLean.List
 open FieldOpAlgebra
-/-- Given a Wick contraction `φsΛ` associated with a list `φs`, the
-  product of all time-contractions of pairs of contracted elements in `φs`,
-  as a member of the center of `𝓞.A`. -/
+
+/-- For a list `φs` of `𝓕.FieldOp` and a Wick contraction `φsΛ` the
+  element of the center of `𝓕.FieldOpAlgebra`, `φsΛ.timeContract` is defined as the product
+  of `timeContract φs[j] φs[k]` over contracted pairs `{j, k}` (both indices of `φs`) in `φsΛ`
+  with `j < k`. -/
 noncomputable def timeContract {φs : List 𝓕.FieldOp}
     (φsΛ : WickContraction φs.length) :
     Subalgebra.center ℂ 𝓕.FieldOpAlgebra :=
@@ -28,11 +30,12 @@ noncomputable def timeContract {φs : List 𝓕.FieldOp}
     (φs.get (φsΛ.fstFieldOfContract a)) (φs.get (φsΛ.sndFieldOfContract a)),
     timeContract_mem_center _ _⟩
 
-/-- For `φsΛ` a Wick contraction for `φs`, the time contraction `(φsΛ ↩Λ φ i none).timeContract 𝓞`
-  is equal to `φsΛ.timeContract 𝓞`.
+/-- For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
+  `𝓕.FieldOp`, and a `i ≤ φs.length`  the following relation holds
 
-This result follows from the fact that `timeContract` only depends on contracted pairs,
-and `(φsΛ ↩Λ φ i none)` has the 'same' contracted pairs as `φsΛ`. -/
+  `(φsΛ ↩Λ φ i none).timeContract = φsΛ.timeContract`
+
+  The prove of this result ultimately a consequence of definitions. -/
 @[simp]
 lemma timeContract_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) :
@@ -42,14 +45,13 @@ lemma timeContract_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
   ext a
   simp
 
-/-- For `φsΛ` a Wick contraction for `φs = φ₀…φₙ`, the time contraction
-  `(φsΛ ↩Λ φ i (some j)).timeContract 𝓞` is equal to the multiple of
-- the time contraction of `φ` with `φⱼ` if `i < i.succAbove j` else
-    `φⱼ` with `φ`.
-- `φsΛ.timeContract 𝓞`.
-This follows from the fact that `(φsΛ ↩Λ φ i (some j))` has one more contracted pair than `φsΛ`,
-corresponding to `φ` contracted with `φⱼ`. The order depends on whether we insert `φ` before
-or after `φⱼ`. -/
+/--  For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
+  `𝓕.FieldOp`,  a `i ≤ φs.length` and a `k` in `φsΛ.uncontracted`, then
+  `(φsΛ ↩Λ φ i (some k)).timeContract` is equal to the product of
+  - `timeContract φ φs[k]` if `i ≤ k` or `timeContract φs[k] φ` if `k < i`
+  - `φsΛ.timeContract`.
+
+  The proof of this result ultimately a consequence of definitions. -/
 lemma timeContract_insertAndContract_some
     (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) :
@@ -77,6 +79,17 @@ lemma timeContract_empty (φs : List 𝓕.FieldOp) :
 
 open FieldStatistic
 
+/-! For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
+  `𝓕.FieldOp`,  a `i ≤ φs.length` and a `k` in `φsΛ.uncontracted` such that `i ≤ k`, with the
+  condition that `φ` has greater or equal time to `φs[k]`, then
+  `(φsΛ ↩Λ φ i (some k)).timeContract` is equal to the product of
+  - `[anPart φ, φs[k]]ₛ`
+  - `φsΛ.timeContract`
+  - two copies of the exchange sign of `φ` with the uncontracted fields in `φ₀…φₖ₋₁`.
+    These two exchange signs cancle each other out but are included for convenience.
+
+  The proof of this result ultimately a consequence of definitions and
+  `timeContract_of_timeOrderRel`. -/
 lemma timeContract_insert_some_of_lt
     (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted)
@@ -110,6 +123,19 @@ lemma timeContract_insert_some_of_lt
     simp only [exchangeSign_mul_self]
     · exact ht
 
+/-! For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
+  `𝓕.FieldOp`,  a `i ≤ φs.length` and a `k` in `φsΛ.uncontracted` such that `k < i`, with the
+  condition that `φs[k]` does not have has greater or equal time to `φ`, then
+  `(φsΛ ↩Λ φ i (some k)).timeContract` is equal to the product of
+  - `[anPart φ, φs[k]]ₛ`
+  - `φsΛ.timeContract`
+  - the exchange sign of `φ` with the uncontracted fields in `φ₀…φₖ₋₁`.
+  - the exchange sign of `φ` with the uncontracted fields in `φ₀…φₖ`.
+
+  Most of the contributes to the exchange signs cancle.
+
+  The proof of this result ultimately a consequence of definitions and
+  `timeContract_of_not_timeOrderRel_expand`. -/
 lemma timeContract_insert_some_of_not_lt
     (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted)