docs: Normal ordering

HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Basic.lean

@@ -219,7 +219,14 @@ lemma ι_normalOrderF_eq_of_equiv (a b : 𝓕.FieldOpFreeAlgebra) (h : a ≈ b)
   simp only [LinearMap.mem_ker, ← map_sub]
   exact ι_normalOrderF_zero_of_mem_ideal (a - b) h
 
-/-- Normal ordering on `FieldOpAlgebra`. -/
+/-- For a field specification `𝓕`, `normalOrder` is the linera map
+
+  `FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕`
+
+  defined as the decent of `ι ∘ₗ normalOrderF` from `FieldOpFreeAlgebra 𝓕` to `FieldOpAlgebra 𝓕`.
+  This decent exists because `ι ∘ₗ normalOrderF` is well-defined on equivalence classes.
+
+  The notation `𝓝(a)` is used for `normalOrder a`.  -/
 noncomputable def normalOrder : FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 where
   toFun := Quotient.lift (ι.toLinearMap ∘ₗ normalOrderF) ι_normalOrderF_eq_of_equiv
   map_add' x y := by

HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean

@@ -217,12 +217,19 @@ lemma anPart_mul_normalOrder_ofFieldOpList_eq_superCommute (φ : 𝓕.FieldOp)
 -/
 
 /--
-For a `CrAnFieldOp` `φ` and a list of `CrAnFieldOp`s `φs`, the following is true
+For a field specification `𝓕`, an element `φ` of `𝓕.CrAnFieldOp`, a list `φs` of `𝓕.CrAnFieldOp`,
+  the following relation holds
+
 `[φ, 𝓝(φ₀…φₙ)]ₛ = ∑ i, 𝓢(φ, φ₀…φᵢ₋₁) • [φ, φᵢ]ₛ * 𝓝(φ₀…φᵢ₋₁φᵢ₊₁…φₙ)`.
 
-The proof of this result ultimetly depends on
-- `superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum`
-- `normalOrderSign_eraseIdx`
+The proof of this result ultimetly goes as follows
+- The definition of `normalOrder` is used to rewrite `𝓝(φ₀…φₙ)` as a scalar multiple of
+  a `ofCrAnList φsn` where `φsn` is the normal ordering of `φ₀…φₙ`.
+- `superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum` is used to rewrite the super commutator of `φ`
+  (considered as a list with one lement) with
+  `ofCrAnList φsn` as a sum of supercommutors, one for each element of `φsn`.
+- The fact that super-commutors are in the center of `𝓕.FieldOpAlgebra` is used to rearange terms.
+- Properties of ordered lists, and `normalOrderSign_eraseIdx` is then used to complete the proof.
 -/
 lemma ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum (φ : 𝓕.CrAnFieldOp)
     (φs : List 𝓕.CrAnFieldOp) : [ofCrAnOp φ, 𝓝(ofCrAnList φs)]ₛ = ∑ n : Fin φs.length,
@@ -335,11 +342,18 @@ noncomputable def contractStateAtIndex (φ : 𝓕.FieldOp) (φs : List 𝓕.Fiel
   | some n => 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (φs.take n)) • [anPart φ, ofFieldOp φs[n]]ₛ
 
 /--
-For a field specification `𝓕`, the following relation holds in the algebra `𝓕.FieldOpAlgebra`,
+For a field specification `𝓕`, a `φ` in `𝓕.FieldOp` and a list `φs` of `𝓕.FieldOp`
+the following relation holds in the algebra `𝓕.FieldOpAlgebra`,
 `φ * 𝓝(φ₀φ₁…φₙ) = 𝓝(φφ₀φ₁…φₙ) + ∑ i, (𝓢(φ,φ₀φ₁…φᵢ₋₁) • [anPartF φ, φᵢ]ₛ) * 𝓝(φ₀φ₁…φᵢ₋₁φᵢ₊₁…φₙ)`.
 
-The proof of this ultimently depends on :
-- `ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum`
+The proof of ultimetly 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 result `ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum` is used
+  to expand `[anPart φ, 𝓝(φ₀φ₁…φₙ)]` as a sum.
 -/
 lemma ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :
     ofFieldOp φ * 𝓝(ofFieldOpList φs) =

HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean

@@ -372,7 +372,7 @@ lemma ι_timeOrderF_eq_of_equiv (a b : 𝓕.FieldOpFreeAlgebra) (h : a ≈ b) :
 `FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕`
 
 defined as the decent of `ι ∘ₗ timeOrderF` from `FieldOpFreeAlgebra 𝓕` to `FieldOpAlgebra 𝓕`.
-This decent exists because `timeOrderF` is well-defined on equivalence classes.
+This decent exists because `ι ∘ₗ timeOrderF` is well-defined on equivalence classes.
 
 The notation `𝓣(a)` is used for `timeOrder a`. -/
 noncomputable def timeOrder : FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 where

HepLean/PerturbationTheory/FieldOpFreeAlgebra/NormalOrder.lean

@@ -27,11 +27,12 @@ namespace FieldOpFreeAlgebra
 
 noncomputable section
 
-/-- The linear map on the free creation and annihlation
-  algebra defined as the map taking
-  a list of CrAnFieldOp to the normal-ordered list of states multiplied by
-  the sign corresponding to the number of fermionic-fermionic
-  exchanges done in ordering. -/
+/-- For a field specification `𝓕`, `normalOrderF` is the linera map
+  `FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpFreeAlgebra 𝓕`
+  defined by its action on the basis `ofCrAnListF φs`, taking `ofCrAnListF φs` to
+  `normalOrderSign φs • ofCrAnListF (normalOrderList φs)`.
+
+  The notation `𝓝ᶠ(a)` is used for `normalOrderF a`. -/
 def normalOrderF : FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpFreeAlgebra 𝓕 :=
   Basis.constr ofCrAnListFBasis ℂ fun φs =>
   normalOrderSign φs • ofCrAnListF (normalOrderList φs)

HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean

@@ -14,13 +14,14 @@ import HepLean.PerturbationTheory.Koszul.KoszulSign
 namespace FieldSpecification
 variable {𝓕 : FieldSpecification}
 
-/-- The normal ordering relation on creation and annihlation operators.
-  For a list of creation and annihlation states, this relation is designed
-  to move all creation states to the left, and all annihlation operators to the right.
-  We have that `normalOrderRel φ1 φ2` is true if
-  - `φ1` is a creation operator
-  or
-  - `φ2` is an annihlate operator. -/
+/-- For a field specification `𝓕`, `𝓕.normalOrderRel` is a relation on `𝓕.CrAnFieldOp`
+  representing normal ordering. It is defined such that `𝓕.normalOrderRel φ₀ φ₁`
+  is true if one of the following is true
+  - `φ₀` is a creation operator
+  - `φ₁` is an annihilation.
+
+  Thus, colloquially `𝓕.normalOrderRel φ₀ φ₁` says the creation operators are 'less then'
+  annihilation operators. -/
 def normalOrderRel : 𝓕.CrAnFieldOp → 𝓕.CrAnFieldOp → Prop :=
   fun a b => CreateAnnihilate.normalOrder (𝓕 |>ᶜ a) (𝓕 |>ᶜ b)
 
@@ -42,9 +43,9 @@ instance (φ φ' : 𝓕.CrAnFieldOp) : Decidable (normalOrderRel φ φ') :=
 
 -/
 
-/-- The sign associated with putting a list of creation and annihlation states into normal order
-  (with the creation operators on the left).
-  We pick up a minus sign for every fermion paired crossed. -/
+/-- For a field speciication `𝓕`, and a list `φs` of `𝓕.CrAnFieldOp`, `𝓕.normalOrderSign φs` is the
+  sign corresponding to the number of `fermionic`-`fermionic` exchanges undertaken to normal-order
+  `φs` using the insertion sort algorithm. -/
 def normalOrderSign (φs : List 𝓕.CrAnFieldOp) : ℂ :=
   Wick.koszulSign 𝓕.crAnStatistics 𝓕.normalOrderRel φs
 
@@ -221,9 +222,12 @@ open FieldStatistic
 
 -/
 
-/-- The normal ordering of a list of creation and annihilation states.
-  To give some schematic. For example:
-  - `normalOrderList [φ1c, φ1a, φ2c, φ2a] = [φ1c, φ2c, φ1a, φ2a]`
+/-- For a field specification `𝓕`, and a list `φs` of `𝓕.CrAnFieldOp`,
+  `𝓕.normalOrderList φs` is the list `φs` normal-ordered using ther
+  insertion sort algorithm. It puts creation operators on the left and annihilation operators on
+  the right. For example:
+
+  `𝓕.normalOrderList [φ1c, φ1a, φ2c, φ2a] = [φ1c, φ2c, φ1a, φ2a]`
 -/
 def normalOrderList (φs : List 𝓕.CrAnFieldOp) : List 𝓕.CrAnFieldOp :=
   List.insertionSort 𝓕.normalOrderRel φs
@@ -339,10 +343,17 @@ lemma normalOrderList_eraseIdx_normalOrderEquiv {φs : List 𝓕.CrAnFieldOp} (n
   simp only [normalOrderList, normalOrderEquiv]
   rw [HepLean.List.eraseIdx_insertionSort_fin]
 
-lemma normalOrderSign_eraseIdx (φs : List 𝓕.CrAnFieldOp) (n : Fin φs.length) :
-    normalOrderSign (φs.eraseIdx n) = normalOrderSign φs *
-    𝓢(𝓕 |>ₛ (φs.get n), 𝓕 |>ₛ (φs.take n)) *
-    𝓢(𝓕 |>ₛ (φs.get n), 𝓕 |>ₛ ((normalOrderList φs).take (normalOrderEquiv n))) := by
+/-- For a field specification `𝓕`, a list `φs = φ₀…φₙ` of `𝓕.CrAnFieldOp` and an `i < φs.length`,
+  the following relation holds
+  `normalOrderSign (φ₀…φᵢ₋₁φᵢ₊₁…φₙ)` is equal to the product of
+  - `normalOrderSign φ₀…φₙ`,
+  - `𝓢(φᵢ, φ₀…φᵢ₋₁)` i.e. the sign needed to remove `φᵢ` from  `φ₀…φₙ`,
+  - `𝓢(φᵢ, _)` where `_` is the list of elements appearing before `φᵢ` after normal ordering. I.e.
+    the sign needed to insert `φᵢ` back into the normal-ordered list at the correct place. -/
+lemma normalOrderSign_eraseIdx (φs : List 𝓕.CrAnFieldOp) (i : Fin φs.length) :
+    normalOrderSign (φs.eraseIdx i) = normalOrderSign φs *
+    𝓢(𝓕 |>ₛ (φs.get i), 𝓕 |>ₛ (φs.take i)) *
+    𝓢(𝓕 |>ₛ (φs.get i), 𝓕 |>ₛ ((normalOrderList φs).take (normalOrderEquiv i))) := by
   rw [normalOrderSign, Wick.koszulSign_eraseIdx, ← normalOrderSign]
   rfl
 

HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean

@@ -223,8 +223,8 @@ lemma crAnTimeOrderRel_refl (φ : 𝓕.CrAnFieldOp) : crAnTimeOrderRel φ φ :=
 
 /-- For a field specification `𝓕`, and a list `φs` of `𝓕.CrAnFieldOp`,
   `𝓕.crAnTimeOrderSign φs` is the sign corresponding to the number of `ferimionic`-`fermionic`
-  undertaken to time-order (i.e. order with respect to `𝓕.crAnTimeOrderRel`) `φs` using the
-  insertion sort algorithm. -/
+  exchanges undertaken to time-order (i.e. order with respect to `𝓕.crAnTimeOrderRel`) `φs` using
+  the insertion sort algorithm. -/
 def crAnTimeOrderSign (φs : List 𝓕.CrAnFieldOp) : ℂ :=
   Wick.koszulSign 𝓕.crAnStatistics 𝓕.crAnTimeOrderRel φs