From ea29b15e4a5d1246968c863570221d075b914901 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 12 Feb 2025 06:14:11 +0000
Subject: [PATCH] refactor: Slight adjustments to doc-strings

---
 HepLean/Mathematics/List.lean                 |  2 +-
 .../FieldOpAlgebra/NormalOrder/Lemmas.lean    | 23 +++++++++++++------
 .../FieldOpAlgebra/StaticWickTerm.lean        |  4 ++--
 .../FieldOpAlgebra/SuperCommute.lean          |  2 ++
 .../FieldOpAlgebra/WickTerm.lean              |  4 ++--
 .../FieldOpAlgebra/WicksTheoremNormal.lean    |  6 ++---
 .../FieldOpFreeAlgebra/NormalOrder.lean       |  4 ++++
 .../FieldOpFreeAlgebra/SuperCommute.lean      |  1 +
 .../FieldOpFreeAlgebra/TimeOrder.lean         |  7 +++++-
 .../FieldSpecification/Basic.lean             |  8 ++++---
 .../FieldSpecification/CrAnFieldOp.lean       | 12 ++++++----
 .../FieldStatistics/ExchangeSign.lean         |  2 ++
 .../WickContraction/InsertAndContract.lean    | 12 +++++++---
 .../WickContraction/Sign/Basic.lean           |  3 ++-
 HepLean/Tensors/Tree/Elab.lean                |  4 ++--
 15 files changed, 64 insertions(+), 30 deletions(-)

diff --git a/HepLean/Mathematics/List.lean b/HepLean/Mathematics/List.lean
index 6cfa02c..32b60ae 100644
--- a/HepLean/Mathematics/List.lean
+++ b/HepLean/Mathematics/List.lean
@@ -353,7 +353,7 @@ lemma orderedInsert_eraseIdx_orderedInsertPos_le {I : Type} (le1 : I → I → P
     omega
 
 /-- The equivalence between `Fin (r0 :: r).length` and `Fin (List.orderedInsert le1 r0 r).length`
-  according to where the elements map. I.e. `0` is taken to `orderedInsertPos le1 r r0`. -/
+  according to where the elements map, i.e. `0` is taken to `orderedInsertPos le1 r r0`. -/
 def orderedInsertEquiv {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) :
     Fin (r0 :: r).length ≃ Fin (List.orderedInsert le1 r0 r).length := by
   let e2 : Fin (List.orderedInsert le1 r0 r).length ≃ Fin (r0 :: r).length :=
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean
index fd6cdb0..1650212 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean
@@ -119,7 +119,7 @@ lemma crPart_mul_normalOrder (φ : 𝓕.FieldOp) (a : 𝓕.FieldOpAlgebra) :
 -/
 
 /-- For a field specification `𝓕`, and `a` and `b` in `𝓕.FieldOpAlgebra` the normal ordering
-  of the super commutator of `a` and `b` vanishes. I.e. `𝓝([a,b]ₛ) = 0`. -/
+  of the super commutator of `a` and `b` vanishes, i.e. `𝓝([a,b]ₛ) = 0`. -/
 @[simp]
 lemma normalOrder_superCommute_eq_zero (a b : 𝓕.FieldOpAlgebra) :
     𝓝([a, b]ₛ) = 0 := by
@@ -346,15 +346,24 @@ noncomputable def contractStateAtIndex (φ : 𝓕.FieldOp) (φs : List 𝓕.Fiel
 
 /--
 For a field specification `𝓕`, a `φ` in `𝓕.FieldOp` and a list `φs` of `𝓕.FieldOp`
-the following relation holds in the algebra `𝓕.FieldOpAlgebra`,
-`φ * 𝓝(φ₀φ₁…φₙ) = 𝓝(φφ₀φ₁…φₙ) + ∑ i, (𝓢(φ,φ₀φ₁…φᵢ₋₁) • [anPart φ, φᵢ]ₛ) * 𝓝(φ₀φ₁…φᵢ₋₁φᵢ₊₁…φₙ)`.
+then `φ * 𝓝(φ₀φ₁…φₙ)` is equal to
+
+`𝓝(φφ₀φ₁…φₙ) + ∑ i, (𝓢(φ,φ₀φ₁…φᵢ₋₁) • [anPart φ, φᵢ]ₛ) * 𝓝(φ₀…φᵢ₋₁φᵢ₊₁…φₙ)`.
 
 The proof of ultimately goes as follows:
 - `ofFieldOp_eq_crPart_add_anPart` is used to split `φ` into its creation and annihilation parts.
-- The fact that `crPart φ * 𝓝(φ₀φ₁…φₙ) = 𝓝(crPart φ * φ₀φ₁…φₙ)` is used.
-- The fact that `anPart φ * 𝓝(φ₀φ₁…φₙ)` is
-  `𝓢(φ, φ₀φ₁…φₙ) 𝓝(φ₀φ₁…φₙ) * anPart φ + [anPart φ, 𝓝(φ₀φ₁…φₙ)]` is used
-- The fact that `𝓢(φ, φ₀φ₁…φₙ) 𝓝(φ₀φ₁…φₙ) * anPart φ = 𝓝(anPart φ * φ₀φ₁…φₙ)`
+- The following relation is then used
+
+  `crPart φ * 𝓝(φ₀φ₁…φₙ) = 𝓝(crPart φ * φ₀φ₁…φₙ)`.
+
+- It used that  `anPart φ * 𝓝(φ₀φ₁…φₙ)` is equal to
+
+  `𝓢(φ, φ₀φ₁…φₙ) 𝓝(φ₀φ₁…φₙ) * anPart φ + [anPart φ, 𝓝(φ₀φ₁…φₙ)]`
+
+- Then it is used that
+
+  `𝓢(φ, φ₀φ₁…φₙ) 𝓝(φ₀φ₁…φₙ) * anPart φ = 𝓝(anPart φ * φ₀φ₁…φₙ)`
+
 - The result `ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum` is used
   to expand `[anPart φ, 𝓝(φ₀φ₁…φₙ)]` as a sum.
 -/
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean
index d4abf71..599e9fd 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean
@@ -41,9 +41,9 @@ lemma staticWickTerm_empty_nil :
 
 /--
 For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, and an element `φ` of
-  `𝓕.FieldOp`, the following relation holds
+  `𝓕.FieldOp`, then  `(φsΛ ↩Λ φ 0 none).staticWickTerm` is equal to
 
-`(φsΛ ↩Λ φ 0 none).staticWickTerm = φsΛ.sign • φsΛ.staticWickTerm * 𝓝(φ :: [φsΛ]ᵘᶜ)`
+`φsΛ.sign • φsΛ.staticWickTerm * 𝓝(φ :: [φsΛ]ᵘᶜ)`
 
 The proof of this result relies on
 - `staticContract_insert_none` to rewrite the static contract.
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean
index cce56cd..e9e4522 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean
@@ -89,7 +89,9 @@ lemma superCommuteRight_eq_of_equiv (a1 a2 : 𝓕.FieldOpFreeAlgebra) (h : a1 
   simp
 
 /-- For a field specification `𝓕`, `superCommute` is the linear map
+
   `FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕`
+
   defined as the decent of `ι ∘ superCommuteF` in both arguments.
   In particular for `φs` and `φs'` lists of `𝓕.CrAnFieldOp` in `FieldOpAlgebra 𝓕` the following
   relation holds:
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean
index 200f7d9..4f4f85e 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean
@@ -43,9 +43,9 @@ lemma wickTerm_empty_nil :
 
 /--
 For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
-  `𝓕.FieldOp`, and `i ≤ φs.length` the following relation holds
+  `𝓕.FieldOp`, and `i ≤ φs.length`, then `(φsΛ ↩Λ φ i none).wickTerm` is equal to
 
-`(φsΛ ↩Λ φ i none).wickTerm = 𝓢(φ, φ₀…φᵢ₋₁) φsΛ.sign • φsΛ.timeContract * 𝓝(φ :: [φsΛ]ᵘᶜ)`
+`𝓢(φ, φ₀…φᵢ₋₁) φsΛ.sign • φsΛ.timeContract * 𝓝(φ :: [φsΛ]ᵘᶜ)`
 
 The proof of this result relies on
 - `normalOrder_uncontracted_none` to rewrite normal orderings.
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean
index b2132b7..35a2400 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean
@@ -23,7 +23,7 @@ open EqTimeOnly
 /--
 For a list `φs` of `𝓕.FieldOp`, then
 
-`𝓣(φs) = ∑ φsΛ, φsΛ.1.wickTerm • φsΛ.1.timeContract.1 * 𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ))`
+`𝓣(φs) = ∑ φsΛ, φsΛ.sign • φsΛ.timeContract * 𝓣(𝓝([φsΛ]ᵘᶜ))`
 
 where the sum is over all Wick contraction `φsΛ` which only have equal time contractions.
 
@@ -92,7 +92,7 @@ lemma timeOrder_ofFieldOpList_eq_eqTimeOnly_empty (φs : List 𝓕.FieldOp) :
 /--
 For a list `φs` of `𝓕.FieldOp`, then
 
-`𝓣(𝓝(φs)) = 𝓣(φs) - ∑ φsΛ, φsΛ.1.wickTerm • φsΛ.1.timeContract.1 * 𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ))`
+`𝓣(𝓝(φs)) = 𝓣(φs) - ∑ φsΛ, φsΛ.sign • φsΛ.timeContract.1 * 𝓣(𝓝([φsΛ]ᵘᶜ))`
 
 where the sum is over all *non-empty* Wick contraction `φsΛ` which only
   have equal time contractions.
@@ -222,7 +222,7 @@ lemma wicks_theorem_normal_order_empty : 𝓣(𝓝(ofFieldOpList [])) =
 where the sum is over all Wick contraction `φsΛ` in which no two contracted elements
 have the same time.
 
-The proof of proceeds by induction on `φs`, with the base case `[]` holding by following
+The proof proceeds by induction on `φs`, with the base case `[]` holding by following
 through definitions. and the inductive case holding as a result of
 - `timeOrder_haveEqTime_split`
 - `normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty`
diff --git a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/NormalOrder.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/NormalOrder.lean
index a2ddbb0..29deeaa 100644
--- a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/NormalOrder.lean
+++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/NormalOrder.lean
@@ -28,9 +28,13 @@ namespace FieldOpFreeAlgebra
 noncomputable section
 
 /-- For a field specification `𝓕`, `normalOrderF` is the linear map
+
   `FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpFreeAlgebra 𝓕`
+
   defined by its action on the basis `ofCrAnListF φs`, taking `ofCrAnListF φs` to
+
   `normalOrderSign φs • ofCrAnListF (normalOrderList φs)`.
+
   That is, `normalOrderF` normal-orders the field operators and multiplies by the sign of the
   normal order.
 
diff --git a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean
index 77046ea..2e19473 100644
--- a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean
+++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean
@@ -26,6 +26,7 @@ open FieldStatistic
 /-- For a field specification `𝓕`, the super commutator `superCommuteF` is defined as the linear
   map `𝓕.FieldOpFreeAlgebra →ₗ[ℂ] 𝓕.FieldOpFreeAlgebra →ₗ[ℂ] 𝓕.FieldOpFreeAlgebra`
   which on the lists `φs` and `φs'` of `𝓕.CrAnFieldOp` gives
+
   `superCommuteF φs φs' = φs * φs' - 𝓢(φs, φs') • φs' * φs`.
 
   The notation `[a, b]ₛca` can be used for `superCommuteF a b`. -/
diff --git a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/TimeOrder.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/TimeOrder.lean
index ae1f4d0..a6daed3 100644
--- a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/TimeOrder.lean
+++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/TimeOrder.lean
@@ -27,9 +27,14 @@ open HepLean.List
 -/
 
 /-- For a field specification `𝓕`, `timeOrderF` is the linear map
+
   `FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpFreeAlgebra 𝓕`
+
   defined by its action on the basis `ofCrAnListF φs`, taking
-  `ofCrAnListF φs` to `crAnTimeOrderSign φs • ofCrAnListF (crAnTimeOrderList φs)`.
+  `ofCrAnListF φs` to
+
+  `crAnTimeOrderSign φs • ofCrAnListF (crAnTimeOrderList φs)`.
+
   That is, `timeOrderF` time-orders the field operators and multiplies by the sign of the
   time order.
 
diff --git a/HepLean/PerturbationTheory/FieldSpecification/Basic.lean b/HepLean/PerturbationTheory/FieldSpecification/Basic.lean
index cf59085..2b95607 100644
--- a/HepLean/PerturbationTheory/FieldSpecification/Basic.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/Basic.lean
@@ -85,12 +85,14 @@ As some intuition, if `f` corresponds to a Weyl-fermion field, then
 - For `inAsymp f e p`, `e` would correspond to a spin `s`, and `inAsymp f e p` would, once
   represented in the operator algebra,
   be proportional to the creation operator `a(p, s)`.
-- `position f e x`, `e` would correspond to a Lorentz index `α`, and `position f e x` would,
+- `position f e x`, `e` would correspond to a Lorentz index `a`, and `position f e x` would,
   once represented in the operator algebra, be proportional to the operator
-  `∑ s, ∫ d^3p/(…) (x_α(p,s)  a(p, s) e^{-i p x} + y_α(p,s) a^†(p, s) e^{-i p x})`.
+
+  `∑ s, ∫ d³p/(…) (xₐ(p,s)  a(p, s) e ^ (-i p x) + yₐ(p,s) a†(p, s) e ^ (-i p x))`.
+
 - `outAsymp f e p`, `e` would correspond to a spin `s`, and `outAsymp f e p` would,
   once represented in the operator algebra, be proportional to the
-  annihilation operator `a^†(p, s)`.
+  annihilation operator `a†(p, s)`.
 
 This type contains all operators which are related to a field.
 -/
diff --git a/HepLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean b/HepLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean
index 13141fd..2725b1e 100644
--- a/HepLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean
@@ -81,12 +81,14 @@ As some intuition, if `f` corresponds to a Weyl-fermion field, it would contribu
   the following elements to `𝓕.CrAnFieldOp`
 - an element corresponding to incoming asymptotic operators for each spin `s`: `a(p, s)`.
 - an element corresponding to the creation parts of position operators for each each Lorentz
-  index `α`:
-  `∑ s, ∫ d^3p/(…) (x_α(p,s)  a(p, s) e^{-i p x})`.
+  index `a`:
+
+  `∑ s, ∫ d³p/(…) (xₐ (p,s)  a(p, s) e ^ (-i p x))`.
 - an element corresponding to annihilation parts of position operator,
-  for each each Lorentz index `α`:
-  `∑ s, ∫ d^3p/(…) (y_α(p,s) a^†(p, s) e^{-i p x})`.
-- an element corresponding to outgoing asymptotic operators for each spin `s`: `a^†(p, s)`.
+  for each each Lorentz index `a`:
+
+  `∑ s, ∫ d³p/(…) (yₐ(p,s) a†(p, s) e ^ (-i p x))`.
+- an element corresponding to outgoing asymptotic operators for each spin `s`: `a†(p, s)`.
 
 -/
 def CrAnFieldOp : Type := Σ (s : 𝓕.FieldOp), 𝓕.fieldOpToCrAnType s
diff --git a/HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean b/HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean
index 5fad4dd..03c8e46 100644
--- a/HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean
+++ b/HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean
@@ -25,7 +25,9 @@ namespace FieldStatistic
 variable {𝓕 : Type}
 
 /-- The exchange sign, `exchangeSign`, is defined as the group homomorphism
+
   `FieldStatistic →* FieldStatistic →* ℂ`,
+
   for which `exchangeSign a b` is `-1` if both `a` and `b` are `fermionic` and `1` otherwise.
   The exchange sign is the sign one picks up on exchanging an operator or field `φ₁` of statistic
   `a` with an operator or field `φ₂` of statistic `b`, i.e. `φ₁φ₂ → φ₂φ₁`.
diff --git a/HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean b/HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean
index 284cff2..1a0bffe 100644
--- a/HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean
+++ b/HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean
@@ -291,9 +291,15 @@ lemma insert_fin_eq_self (φ : 𝓕.FieldOp) {φs : List 𝓕.FieldOp}
   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Λ`.
 
-  In other words, `∑ (φ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`. -/
+  In other words,
+
+  `∑ (φsΛ : WickContraction (φs.insertIdx i φ).length), f φsΛ`
+
+  where `(φs.insertIdx i φ)` is `φs` with `φ` inserted at position `i`. is equal to
+
+  `∑ (φsΛ : WickContraction φs.length), ∑ k, f (φsΛ ↩Λ φ i k) `.
+
+  where the sum over `k` is over all `k` in `Option φsΛ.uncontracted`. -/
 lemma insertLift_sum (φ : 𝓕.FieldOp) {φs : List 𝓕.FieldOp}
     (i : Fin φs.length.succ) [AddCommMonoid M] (f : WickContraction (φs.insertIdx i φ).length → M) :
     ∑ c, f c =
diff --git a/HepLean/PerturbationTheory/WickContraction/Sign/Basic.lean b/HepLean/PerturbationTheory/WickContraction/Sign/Basic.lean
index 07e4657..adc4c08 100644
--- a/HepLean/PerturbationTheory/WickContraction/Sign/Basic.lean
+++ b/HepLean/PerturbationTheory/WickContraction/Sign/Basic.lean
@@ -22,7 +22,8 @@ open FieldStatistic
 /-- Given a Wick contraction `c : WickContraction n` and `i1 i2 : Fin n` the finite set
   of elements of `Fin n` between `i1` and `i2` which are either uncontracted
   or are contracted but are contracted with an element occurring after `i1`.
-  I.e. the elements of `Fin n` between `i1` and `i2` which are not contracted with before `i1`.
+  In other words, the elements of `Fin n` between `i1` and `i2` which are not
+  contracted with before `i1`.
   One should assume `i1 < i2` otherwise this finite set is empty. -/
 def signFinset (c : WickContraction n) (i1 i2 : Fin n) : Finset (Fin n) :=
   Finset.univ.filter (fun i => i1 < i ∧ i < i2 ∧
diff --git a/HepLean/Tensors/Tree/Elab.lean b/HepLean/Tensors/Tree/Elab.lean
index d1c6130..f869b4b 100644
--- a/HepLean/Tensors/Tree/Elab.lean
+++ b/HepLean/Tensors/Tree/Elab.lean
@@ -39,8 +39,8 @@ import HepLean.Lorentz.ComplexTensor.Basic
 ## Comments
 
 - In all of theses expressions `μ`, `ν` etc are free. It does not matter what they are called,
-  Lean will elaborate them in the same way. I.e. `{T | μ ν ⊗ T3 | μ ν }ᵀ` is exactly the same
-  to Lean as `{T | α β ⊗ T3 | α β }ᵀ`.
+  Lean will elaborate them in the same way. In other words, `{T | μ ν ⊗ T3 | μ ν }ᵀ` is exactly
+  the same to Lean as `{T | α β ⊗ T3 | α β }ᵀ`.
 - Note that compared to ordinary index notation, we do not rise or lower the indices.
   This is for two reasons: 1) It is difficult to make this general for all tensor species,
   2) It is a redundancy in ordinary index notation, since the tensor `T` itself already tells you