From ee2134e448cba578a42a6693ff5edd0d454c6aa0 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 6 Feb 2025 13:28:52 +0000
Subject: [PATCH] doc: Related to time ordering

---
 .../FieldOpAlgebra/TimeOrder.lean             | 16 ++++++++--
 .../FieldOpFreeAlgebra/TimeOrder.lean         |  7 +++--
 .../FieldSpecification/TimeOrder.lean         | 29 +++++++++++--------
 scripts/MetaPrograms/notes.lean               | 12 ++++----
 4 files changed, 41 insertions(+), 23 deletions(-)

diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean
index 98cec2d..b3f17fc 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean
@@ -367,7 +367,14 @@ lemma ι_timeOrderF_eq_of_equiv (a b : 𝓕.FieldOpFreeAlgebra) (h : a ≈ b) :
   simp only [LinearMap.mem_ker, ← map_sub]
   exact ι_timeOrderF_zero_of_mem_ideal (a - b) h
 
-/-- Time ordering on `FieldOpAlgebra`. -/
+/-- For a field specification `𝓕`, `timeOrder` is the linear map
+
+`FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕`
+
+defined as the decent of `ι ∘ₗ timeOrderF` from `FieldOpFreeAlgebra 𝓕` to `FieldOpAlgebra 𝓕`.
+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
   toFun := Quotient.lift (ι.toLinearMap ∘ₗ timeOrderF) ι_timeOrderF_eq_of_equiv
   map_add' x y := by
@@ -423,8 +430,11 @@ lemma timeOrder_ofFieldOpList_singleton (φ : 𝓕.FieldOp) :
     𝓣(ofFieldOpList [φ]) = ofFieldOpList [φ] := by
   rw [ofFieldOpList, timeOrder_eq_ι_timeOrderF, timeOrderF_ofFieldOpListF_singleton]
 
-/-- The time order of a list `𝓣(φ₀…φₙ)` is equal to
-`𝓢(φᵢ,φ₀…φᵢ₋₁) • φᵢ * 𝓣(φ₀…φᵢ₋₁φᵢ₊₁φₙ)` where `φᵢ` is the maximal time field in `φ₀…φₙ`-/
+/-- For a field specification `𝓕`, the time order operator acting on a
+  list of `𝓕.FieldOp`, `𝓣(φ₀…φₙ)`, is equal to
+  `𝓢(φᵢ,φ₀…φᵢ₋₁) • φᵢ * 𝓣(φ₀…φᵢ₋₁φᵢ₊₁φₙ)` where `φᵢ` is the maximal time field in `φ₀…φₙ`.
+
+  The proof of this result ultimitley relies on basic properties of ordering and signs. -/
 lemma timeOrder_eq_maxTimeField_mul_finset (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :
     𝓣(ofFieldOpList (φ :: φs)) = 𝓢(𝓕 |>ₛ maxTimeField φ φs, 𝓕 |>ₛ ⟨(eraseMaxTimeField φ φs).get,
       (Finset.univ.filter (fun x =>
diff --git a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/TimeOrder.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/TimeOrder.lean
index 19b4b5a..75ef74d 100644
--- a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/TimeOrder.lean
+++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/TimeOrder.lean
@@ -26,9 +26,12 @@ open HepLean.List
 
 -/
 
-/-- Time ordering for the `FieldOpFreeAlgebra` defined by taking
+/-- 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)`.
-  The notation `𝓣ᶠ(a)` is used for the time-ordering of `a : FieldOpFreeAlgebra`. -/
+
+  The notation `𝓣ᶠ(a)` is used for `timeOrderF a` -/
 def timeOrderF : FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpFreeAlgebra 𝓕 :=
   Basis.constr ofCrAnListFBasis ℂ fun φs =>
   crAnTimeOrderSign φs • ofCrAnListF (crAnTimeOrderList φs)
diff --git a/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean b/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean
index c6a7f6f..4243840 100644
--- a/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean
@@ -191,14 +191,17 @@ lemma timeOrderList_eq_maxTimeField_timeOrderList (φ : 𝓕.FieldOp) (φs : Lis
 
 -/
 
-/-- For a field specification `𝓕`,  `𝓕.crAnTimeOrderRel` is time ordering relation on
-  `𝓕.CrAnFieldOp` defined to put those field operators with greatest time to the left on
-  ordering a list. Thus `𝓕.crAnTimeOrderRel φ₀ φ₁` is true if and only if one of the following is
-  true
-- `φ₀` is an outgoing asymptotic creation and annihilation field operator
-- `φ₁` is an incoming asymptotic creation and annihilation field operator
-- `φ₀` and `φ₁` are both position operators where `φ₀` occurs at a time greater then or equal to
-  that of `φ₁`. -/
+/-- For a field specification `𝓕`,  `𝓕.crAnTimeOrderRel` is a relation on
+  `𝓕.CrAnFieldOp` representing time ordering.
+  It is defined as such that `𝓕.crAnTimeOrderRel φ₀ φ₁` is true if and only if one of the following
+  holds
+- `φ₀` is an *outgoing* asymptotic operator
+- `φ₁` is an *incoming* asymptotic field operator
+- `φ₀` and `φ₁` are both position field operators where
+  the `SpaceTime` point of `φ₀` has a time *greater* then or equal to that of `φ₁`.
+
+Thus, colloquially `𝓕.crAnTimeOrderRel φ₀ φ₁` if `φ₀` has time *greater* then or equal to `φ₁`.
+ -/
 def crAnTimeOrderRel (a b : 𝓕.CrAnFieldOp) : Prop := 𝓕.timeOrderRel a.1 b.1
 
 /-- The relation `crAnTimeOrderRel` is decidable, but not computablly so due to
@@ -218,9 +221,10 @@ instance : IsTrans 𝓕.CrAnFieldOp 𝓕.crAnTimeOrderRel where
 lemma crAnTimeOrderRel_refl (φ : 𝓕.CrAnFieldOp) : crAnTimeOrderRel φ φ := by
   exact (IsTotal.to_isRefl (r := 𝓕.crAnTimeOrderRel)).refl φ
 
-/-- The sign associated with putting a list of `CrAnFieldOp` into time order (with
-  the state of greatest time to the left).
-  We pick up a minus sign for every fermion paired crossed. -/
+/-- 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. -/
 def crAnTimeOrderSign (φs : List 𝓕.CrAnFieldOp) : ℂ :=
   Wick.koszulSign 𝓕.crAnStatistics 𝓕.crAnTimeOrderRel φs
 
@@ -246,7 +250,8 @@ lemma crAnTimeOrderSign_swap_eq_time {φ ψ : 𝓕.CrAnFieldOp}
     crAnTimeOrderSign (φs ++ φ :: ψ :: φs') = crAnTimeOrderSign (φs ++ ψ :: φ :: φs') := by
   exact Wick.koszulSign_swap_eq_rel _ _ h1 h2 _ _
 
-/-- Sort a list of `CrAnFieldOp` based on `crAnTimeOrderRel`. -/
+/-- For a field specification `𝓕`, and a list `φs` of `𝓕.CrAnFieldOp`,
+  `𝓕.crAnTimeOrderList φs` is the list `φs` time-ordered using the insertion sort algorithm. -/
 def crAnTimeOrderList (φs : List 𝓕.CrAnFieldOp) : List 𝓕.CrAnFieldOp :=
   List.insertionSort 𝓕.crAnTimeOrderRel φs
 
diff --git a/scripts/MetaPrograms/notes.lean b/scripts/MetaPrograms/notes.lean
index b87f0bb..0d63e2e 100644
--- a/scripts/MetaPrograms/notes.lean
+++ b/scripts/MetaPrograms/notes.lean
@@ -179,17 +179,17 @@ def perturbationTheory : Note where
     .name ``FieldSpecification.FieldOpAlgebra.fieldOpAlgebraGrade .complete,
     .name ``FieldSpecification.FieldOpAlgebra.superCommute .complete,
     .h1 "Time ordering",
-    .name ``FieldSpecification.crAnTimeOrderRel .incomplete,
-    .name ``FieldSpecification.crAnTimeOrderSign .incomplete,
-    .name ``FieldSpecification.FieldOpFreeAlgebra.timeOrderF .incomplete,
-    .name ``FieldSpecification.FieldOpAlgebra.timeOrder .incomplete,
-    .name ``FieldSpecification.FieldOpAlgebra.timeOrder_eq_maxTimeField_mul_finset .incomplete,
+    .name ``FieldSpecification.crAnTimeOrderRel .complete,
+    .name ``FieldSpecification.crAnTimeOrderList .complete,
+    .name ``FieldSpecification.crAnTimeOrderSign .complete,
+    .name ``FieldSpecification.FieldOpFreeAlgebra.timeOrderF .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.timeOrder .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.timeOrder_eq_maxTimeField_mul_finset .complete,
     .h1 "Normal ordering",
     .name ``FieldSpecification.normalOrderRel .incomplete,
     .name ``FieldSpecification.normalOrderSign .incomplete,
     .name ``FieldSpecification.FieldOpFreeAlgebra.normalOrderF .incomplete,
     .name ``FieldSpecification.FieldOpAlgebra.normalOrder .incomplete,
-    .h2 "Some lemmas",
     .name ``FieldSpecification.normalOrderSign_eraseIdx .incomplete,
     .name ``FieldSpecification.FieldOpAlgebra.ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum .incomplete,
     .name ``FieldSpecification.FieldOpAlgebra.ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum .incomplete,