feat: Wick contraction docs

HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean

@@ -356,6 +356,11 @@ noncomputable def contractStateAtIndex (φ : 𝓕.States) (φs : List 𝓕.State
   | some n => 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (φs.take n)) •
         𝓞.crAnF (⟨anPart (StateAlgebra.ofState φ), ofState φs[n]⟩ₛca)
 
+/--
+Within a proto-operator algebra,
+`φ * N(φ₀φ₁…φₙ) = N(φφ₀φ₁…φₙ) + ∑ i, (sᵢ • [anPart φ, φᵢ]ₛ) * N(φ₀φ₁…φᵢ₋₁φᵢ₊₁…φₙ)`,
+where `sₙ` is the exchange sign for `φ` and `φ₀φ₁…φᵢ₋₁`.
+-/
 lemma crAnF_ofState_mul_normalOrder_ofStatesList_eq_sum (φ : 𝓕.States)
     (φs : List 𝓕.States) :
     𝓞.crAnF (ofState φ * normalOrder (ofStateList φs)) =
@@ -374,6 +379,10 @@ lemma crAnF_ofState_mul_normalOrder_ofStatesList_eq_sum (φ : 𝓕.States)
 
 -/
 
+/--
+Within a proto-operator algebra, `N(φφ₀φ₁…φₙ) = s • N(φ₀…φₖ₋₁φφₖ…φₙ)`, where
+`s` is the exchange sign for `φ` and `φ₀…φₖ₋₁`.
+-/
 lemma crAnF_ofState_normalOrder_insert (φ : 𝓕.States) (φs : List 𝓕.States)
     (k : Fin φs.length.succ) :
     𝓞.crAnF (normalOrder (ofStateList (φ :: φs))) =

HepLean/PerturbationTheory/Algebras/StateAlgebra/TimeOrder.lean

@@ -18,6 +18,7 @@ noncomputable section
 namespace StateAlgebra
 
 open FieldStatistic
+open HepLean.List
 
 /-- The linear map on the free state algebra defined as the map taking
   a list of states to the time-ordered list of states multiplied by
@@ -64,6 +65,8 @@ lemma timeOrder_ofState_ofState_not_ordered_eq_timeOrder {φ ψ : 𝓕.States} (
   have hx := IsTotal.total (r := timeOrderRel) ψ φ
   simp_all
 
+/-- In the state algebra time, ordering obeys `T(φ₀φ₁…φₙ) = s * φᵢ * T(φ₀φ₁…φᵢ₋₁φᵢ₊₁…φₙ)` where `φᵢ` is the state
+  which has maximum time and `s` is the exchange sign of `φᵢ` and `φ₀φ₁…φᵢ₋₁`. -/
 lemma timeOrder_eq_maxTimeField_mul (φ : 𝓕.States) (φs : List 𝓕.States) :
     timeOrder (ofList (φ :: φs)) =
     𝓢(𝓕 |>ₛ maxTimeField φ φs, 𝓕 |>ₛ (φ :: φs).take (maxTimeFieldPos φ φs)) •
@@ -75,6 +78,56 @@ lemma timeOrder_eq_maxTimeField_mul (φ : 𝓕.States) (φs : List 𝓕.States)
   rw [timerOrderSign_of_eraseMaxTimeField, mul_assoc]
   simp
 
+/-- In the state algebra time, ordering obeys `T(φ₀φ₁…φₙ) = s * φᵢ * T(φ₀φ₁…φᵢ₋₁φᵢ₊₁…φₙ)` where `φᵢ` is the state
+  which has maximum time and `s` is the exchange sign of `φᵢ` and `φ₀φ₁…φᵢ₋₁`.
+  Here `s` is written using finite sets. -/
+lemma timeOrder_eq_maxTimeField_mul_finset (φ : 𝓕.States) (φs : List 𝓕.States) :
+    timeOrder (ofList (φ :: φs)) = 𝓢(𝓕 |>ₛ maxTimeField φ φs, 𝓕 |>ₛ ⟨(eraseMaxTimeField φ φs).get,
+      (Finset.filter (fun x =>
+        (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs) Finset.univ)⟩) •
+    StateAlgebra.ofState (maxTimeField φ φs) * timeOrder (ofList (eraseMaxTimeField φ φs)) := by
+  rw [timeOrder_eq_maxTimeField_mul]
+  congr 3
+  apply FieldStatistic.ofList_perm
+  nth_rewrite 1 [← List.finRange_map_get (φ :: φs)]
+  simp only [List.length_cons, eraseMaxTimeField, insertionSortDropMinPos]
+  rw [eraseIdx_get, ← List.map_take, ← List.map_map]
+  refine List.Perm.map (φ :: φs).get ?_
+  apply (List.perm_ext_iff_of_nodup _ _).mpr
+  · intro i
+    simp only [List.length_cons, maxTimeFieldPos, mem_take_finrange, Fin.val_fin_lt, List.mem_map,
+      Finset.mem_sort, Finset.mem_filter, Finset.mem_univ, true_and, Function.comp_apply]
+    refine Iff.intro (fun hi => ?_) (fun h => ?_)
+    · have h2 := (maxTimeFieldPosFin φ φs).2
+      simp only [eraseMaxTimeField, insertionSortDropMinPos, List.length_cons, Nat.succ_eq_add_one,
+        maxTimeFieldPosFin, insertionSortMinPosFin] at h2
+      use ⟨i, by omega⟩
+      apply And.intro
+      · simp only [Fin.succAbove, List.length_cons, Fin.castSucc_mk, maxTimeFieldPosFin,
+        insertionSortMinPosFin, Nat.succ_eq_add_one, Fin.mk_lt_mk, Fin.val_fin_lt, Fin.succ_mk]
+        rw [Fin.lt_def]
+        split
+        · simp only [Fin.val_fin_lt]
+          omega
+        · omega
+      · simp only [Fin.succAbove, List.length_cons, Fin.castSucc_mk, Fin.succ_mk, Fin.ext_iff,
+        Fin.coe_cast]
+        split
+        · simp
+        · simp_all [Fin.lt_def]
+    · obtain ⟨j, h1, h2⟩ := h
+      subst h2
+      simp only [Fin.lt_def, Fin.coe_cast]
+      exact h1
+  · exact List.Sublist.nodup (List.take_sublist _ _) <|
+      List.nodup_finRange (φs.length + 1)
+  · refine List.Nodup.map ?_ ?_
+    · refine Function.Injective.comp ?hf.hg Fin.succAbove_right_injective
+      exact Fin.cast_injective (eraseIdx_length (φ :: φs) (insertionSortMinPos timeOrderRel φ φs))
+    · exact Finset.sort_nodup (fun x1 x2 => x1 ≤ x2)
+        (Finset.filter (fun x => (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs)
+          Finset.univ)
+
 end StateAlgebra
 end
 end FieldSpecification

HepLean/PerturbationTheory/FieldSpecification/Examples.lean

@@ -13,18 +13,23 @@ import HepLean.PerturbationTheory.FieldSpecification.Basic
 namespace FieldSpecification
 variable (𝓕 : FieldSpecification)
 
-/-- The Field specification corresponding to a single bosonic field. -/
+/-- The Field specification corresponding to a single bosonic field.
+  The type of fields is the unit type, and the statistic of the unique element of the unit
+  type is bosonic. -/
 def singleBoson : FieldSpecification where
   Fields := Unit
   statistics := fun _ => FieldStatistic.bosonic
 
-/-- The Field specification corresponding to a single fermionic field. -/
+/-- The Field specification corresponding to a single fermionic field.
+  The type of fields is the unit type, and the statistic of the unique element of the unit
+  type is fermionic. -/
 def singleFermion : FieldSpecification where
   Fields := Unit
   statistics := fun _ => FieldStatistic.fermionic
 
-/-- The Field specification corresponding to a two bosonic field and
+/-- The Field specification corresponding to two bosonic fields and two fermionic fields.
-  two fermionic fields. -/
+  The type of fields is `Fin 2 ⊕ Fin 2`, and the statistic of the two `.inl` (left) elements
+  is bosonic and the statistic of the two `.inr` (right) elements is fermionic. -/
 def doubleBosonDoubleFermion : FieldSpecification where
   Fields := Fin 2 ⊕ Fin 2
   statistics := fun b =>

HepLean/PerturbationTheory/WicksTheorem.lean

@@ -25,6 +25,11 @@ open HepLean.List
 open WickContraction
 open FieldStatistic
 
+/--
+Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`.
+We have  (roughly) `N(c.insertList φ φs i none).uncontractedList = s • N(φ * c.uncontractedList)`
+Where `s` is the exchange sign for `φ` and the uncontracted fields in `φ₀φ₁…φᵢ`.
+-/
 lemma insertList_none_normalOrder (φ : 𝓕.States) (φs : List 𝓕.States)
     (i : Fin φs.length.succ) (c : WickContraction φs.length) :
     𝓞.crAnF (normalOrder (ofStateList (List.map (φs.insertIdx i φ).get
@@ -91,6 +96,12 @@ lemma insertList_none_normalOrder (φ : 𝓕.States) (φs : List 𝓕.States)
   simp only [Nat.succ_eq_add_one]
   rw [insertList_uncontractedList_none_map]
 
+/--
+Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`.
+We have (roughly) `N(c.insertList φ φs i k).uncontractedList`
+is equal to `N((c.uncontractedList).eraseIdx k')`
+where `k'` is the position in `c.uncontractedList` corresponding to `k`.
+-/
 lemma insertList_some_normalOrder (φ : 𝓕.States) (φs : List 𝓕.States)
     (i : Fin φs.length.succ) (c : WickContraction φs.length) (k : c.uncontracted) :
     𝓞.crAnF (normalOrder (ofStateList (List.map (φs.insertIdx i φ).get
@@ -107,6 +118,12 @@ lemma insertList_some_normalOrder (φ : 𝓕.States) (φs : List 𝓕.States)
   congr
   conv_rhs => rw [get_eq_insertIdx_succAbove φ φs i]
 
+/--
+Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`.
+This lemma states that `(c.sign • c.timeContract 𝓞) * N(c.uncontracted)`
+for `c` equal to `c.insertList φ φs i none` is equal to that for just `c`
+mulitiplied by the exchange sign of `φ` and `φ₀φ₁…φᵢ₋₁`.
+-/
 lemma sign_timeContract_normalOrder_insertList_none (φ : 𝓕.States) (φs : List 𝓕.States)
     (i : Fin φs.length.succ) (c : WickContraction φs.length) :
     (c.insertList φ φs i none).sign • (c.insertList φ φs i none).timeContract 𝓞
@@ -150,6 +167,13 @@ lemma sign_timeContract_normalOrder_insertList_none (φ : 𝓕.States) (φs : Li
     simp only [ZeroMemClass.coe_zero, zero_mul, smul_zero]
     exact hg
 
+/--
+Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`.
+This lemma states that
+`(c.sign • c.timeContract 𝓞) * N(c.uncontracted)`
+for `c` equal to `c.insertList φ φs i (some k)` is equal to that for just `c`
+mulitiplied by the exchange sign of `φ` and `φ₀φ₁…φᵢ₋₁`.
+-/
 lemma sign_timeContract_normalOrder_insertList_some (φ : 𝓕.States) (φs : List 𝓕.States)
     (i : Fin φs.length.succ) (c : WickContraction φs.length) (k : c.uncontracted)
     (hlt : ∀ (k : Fin φs.length), timeOrderRel φ φs[k])
@@ -214,6 +238,15 @@ lemma sign_timeContract_normalOrder_insertList_some (φ : 𝓕.States) (φs : Li
         zero_mul, instCommGroup.eq_1]
       exact hg'
 
+/--
+Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`.
+This lemma states that
+`(c.sign • c.timeContract 𝓞) * N(c.uncontracted)`
+is equal to the sum of
+`(c'.sign • c'.timeContract 𝓞) * N(c'.uncontracted)`
+for all `c' = (c.insertList φ φs i k)` for `k : Option (c.uncontracted)`, multiplied by
+the exchange sign of `φ` and `φ₀φ₁…φᵢ₋₁`.
+-/
 lemma mul_sum_contractions (φ : 𝓕.States) (φs : List 𝓕.States) (i : Fin φs.length.succ)
     (c : WickContraction φs.length) (hlt : ∀ (k : Fin φs.length), timeOrderRel φ φs[k])
     (hn : ∀ (k : Fin φs.length), i.succAbove k < i → ¬timeOrderRel φs[k] φ) :
@@ -226,8 +259,7 @@ lemma mul_sum_contractions (φ : 𝓕.States) (φs : List 𝓕.States) (i : Fin
       (ofStateList ((c.insertList φ φs i k).uncontractedList.map (φs.insertIdx i φ).get)))) := by
   rw [crAnF_ofState_mul_normalOrder_ofStatesList_eq_sum, Finset.mul_sum,
     uncontractedStatesEquiv_list_sum, Finset.smul_sum]
-  simp only [Finset.univ_eq_attach, instCommGroup.eq_1,
+  simp only [instCommGroup.eq_1, Nat.succ_eq_add_one]
-    Nat.succ_eq_add_one, timeContract_insertList_none]
   congr 1
   funext n
   match n with
@@ -261,54 +293,6 @@ lemma wicks_theorem_congr {φs φs' : List 𝓕.States} (h : φs = φs') :
   subst h
   simp
 
-lemma timeOrder_eq_maxTimeField_mul_finset (φ : 𝓕.States) (φs : List 𝓕.States) :
-    timeOrder (ofList (φ :: φs)) = 𝓢(𝓕 |>ₛ maxTimeField φ φs, 𝓕 |>ₛ ⟨(eraseMaxTimeField φ φs).get,
-      (Finset.filter (fun x =>
-        (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs) Finset.univ)⟩) •
-    StateAlgebra.ofState (maxTimeField φ φs) * timeOrder (ofList (eraseMaxTimeField φ φs)) := by
-  rw [timeOrder_eq_maxTimeField_mul]
-  congr 3
-  apply FieldStatistic.ofList_perm
-  nth_rewrite 1 [← List.finRange_map_get (φ :: φs)]
-  simp only [List.length_cons, eraseMaxTimeField, insertionSortDropMinPos]
-  rw [eraseIdx_get, ← List.map_take, ← List.map_map]
-  refine List.Perm.map (φ :: φs).get ?_
-  apply (List.perm_ext_iff_of_nodup _ _).mpr
-  · intro i
-    simp only [List.length_cons, maxTimeFieldPos, mem_take_finrange, Fin.val_fin_lt, List.mem_map,
-      Finset.mem_sort, Finset.mem_filter, Finset.mem_univ, true_and, Function.comp_apply]
-    refine Iff.intro (fun hi => ?_) (fun h => ?_)
-    · have h2 := (maxTimeFieldPosFin φ φs).2
-      simp only [eraseMaxTimeField, insertionSortDropMinPos, List.length_cons, Nat.succ_eq_add_one,
-        maxTimeFieldPosFin, insertionSortMinPosFin] at h2
-      use ⟨i, by omega⟩
-      apply And.intro
-      · simp only [Fin.succAbove, List.length_cons, Fin.castSucc_mk, maxTimeFieldPosFin,
-        insertionSortMinPosFin, Nat.succ_eq_add_one, Fin.mk_lt_mk, Fin.val_fin_lt, Fin.succ_mk]
-        rw [Fin.lt_def]
-        split
-        · simp only [Fin.val_fin_lt]
-          omega
-        · omega
-      · simp only [Fin.succAbove, List.length_cons, Fin.castSucc_mk, Fin.succ_mk, Fin.ext_iff,
-        Fin.coe_cast]
-        split
-        · simp
-        · simp_all [Fin.lt_def]
-    · obtain ⟨j, h1, h2⟩ := h
-      subst h2
-      simp only [Fin.lt_def, Fin.coe_cast]
-      exact h1
-  · exact List.Sublist.nodup (List.take_sublist _ _) <|
-      List.nodup_finRange (φs.length + 1)
-  · refine List.Nodup.map ?_ ?_
-    · refine Function.Injective.comp ?hf.hg Fin.succAbove_right_injective
-      exact Fin.cast_injective (eraseIdx_length (φ :: φs) (insertionSortMinPos timeOrderRel φ φs))
-    · exact Finset.sort_nodup (fun x1 x2 => x1 ≤ x2)
-        (Finset.filter (fun x => (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs)
-          Finset.univ)
-
-
 /-!
 
 ## Wick's theorem
@@ -335,7 +319,15 @@ remark wicks_theorem_context := "
   the remaining fields. Wick's theorem is also the precursor to the diagrammatic
   approach to quantum field theory called Feynman diagrams."
 
-/-- Wick's theorem for time-ordered products of bosonic and fermionic fields. -/
+/-- Wick's theorem for time-ordered products of bosonic and fermionic fields.
+  The time ordered product `T(φ₀φ₁…φₙ)` is equal to the sum of terms,
+  for all possible Wick contractions `c` of the list of fields `φs := φ₀φ₁…φₙ`, given by
+  the multiple of:
+- The sign corresponding to the number of fermionic-fermionic exchanges one must do
+    to put  elements in contracted pairs of `c` next to each other.
+- The product of time-contractions of the contracted pairs of `c`.
+- The normal-ordering of the uncontracted fields in `c`.
+-/
 theorem wicks_theorem : (φs : List 𝓕.States) → 𝓞.crAnF (ofStateAlgebra (timeOrder (ofList φs))) =
     ∑ (c : WickContraction φs.length), (c.sign φs • c.timeContract 𝓞) *
       𝓞.crAnF (normalOrder (ofStateList (c.uncontractedList.map φs.get)))

docs/CuratedNotes/PerturbationTheory.html

@@ -54,12 +54,13 @@ layout: default
   {% if entry.type == "name" %}
 
   <div style="background-color: #f5f5f5; padding: 10px; border-radius: 4px;">
-    <p>{{ entry.name }}: {{ entry.docString }}</p>
+    <p> <a href = "{{ entry.link }}" style="font-weight: bold; color: #2c5282;">{{ entry.name }}</a>: {{ entry.docString | markdownify}}</p>
     <details class="code-block-container">
     <summary>Show Lean code:</summary>
     <pre style="background: none; margin: 0;"><code class="language-lean">{{ entry.declString }}</code></pre>
     </details>
   </div>
+  <br>
 
   {% endif %}
   {% if entry.type == "remark" %}

scripts/MetaPrograms/notes.lean

@@ -39,14 +39,18 @@ def DeclInfo.ofName (n : Name) : MetaM DeclInfo := do
     declString := declString,
     docString := docString}
 
-def DeclInfo.toYML (d : DeclInfo) : String :=
+def DeclInfo.toYML (d : DeclInfo) : MetaM String := do
   let declStringIndent := d.declString.replace "\n" "\n      "
-  s!"
+  let docStringIndent := d.docString.replace "\n" "\n      "
+  let link ←  Name.toGitHubLink d.fileName d.line
+  return s!"
   - type: name
     name: {d.name}
     line: {d.line}
     fileName: {d.fileName}
-    docString: \"{d.docString}\"
+    link: \"{link}\"
+    docString: |
+      {docStringIndent}
     declString: |
       {declStringIndent}"
 
@@ -82,7 +86,7 @@ def NotePart.toYMLM : ((List String) × Nat × Nat) →  NotePart → MetaM ((Li
       {contentIndent}"
     return ⟨x.1 ++ [newString], x.2⟩
   | false =>
-  let newString :=  (← DeclInfo.ofName n).toYML
+  let newString ← (← DeclInfo.ofName n).toYML
   return ⟨x.1 ++ [newString], x.2⟩
 
 structure Note where
@@ -126,15 +130,40 @@ def perturbationTheory : Note where
     .h2 "Field specifications",
     .name `fieldSpecification_intro,
     .name `FieldSpecification,
+    .p "Some examples of `FieldSpecification`s are given below:",
+    .name `FieldSpecification.singleBoson,
+    .name `FieldSpecification.singleFermion,
+    .name `FieldSpecification.doubleBosonDoubleFermion,
     .h2 "States",
+    .p "Given a field, there are three common states (or operators) of that field that we work with.
+      These are the in and out asymptotic states and the position states.",
+    .p "For a field structure `𝓕` these states are defined as:",
+    .name `FieldSpecification.IncomingAsymptotic,
+    .name `FieldSpecification.OutgoingAsymptotic,
+    .name `FieldSpecification.PositionStates,
+    .p "We will want to consider all three of these types of states simultanously so we define
+      and inductive type `States` which is the disjoint union of these three types of states.",
+    .name `FieldSpecification.States,
+    .name `FieldSpecification.StateAlgebra,
     .h2 "Time ordering",
+    .name `FieldSpecification.timeOrderRel,
+    .name `FieldSpecification.timeOrderSign,
+    .name `FieldSpecification.StateAlgebra.timeOrder,
+    .name `FieldSpecification.StateAlgebra.timeOrder_eq_maxTimeField_mul_finset,
     .h2 "Creation and annihilation states",
     .h2 "Normal ordering",
-    .h1 "Algebras",
+    .h2 "Proto-operator algebra",
-    .h2 "State free-algebra",
+    .h1 "Wick Contractions",
-    .h2 "CrAnState free-algebra",
+    .h1 "Proof of Wick's theorem",
-    .h2 "Proto operator algebra",
+    .h2 "The case of the nil list",
-    .h1 "Contractions"
+    .p "Our proof of Wick's theorem will be via induction on the number of fields that
+      are in the time-ordered product. The base case is when there are no files.
+      The proof of Wick's theorem follows from definitions and simple lemmas.",
+    .name `FieldSpecification.wicks_theorem_nil,
+    .name `FieldSpecification.ProtoOperatorAlgebra.crAnF_ofState_mul_normalOrder_ofStatesList_eq_sum,
+    .name `FieldSpecification.ProtoOperatorAlgebra.crAnF_ofState_normalOrder_insert,
+    .name `FieldSpecification.mul_sum_contractions,
+    .name `FieldSpecification.wicks_theorem,
     ]
 
 unsafe def main (_ : List String) : IO UInt32 := do