Merge pull request #313 from HEPLean/WickTheoremDoc

refactor: Note html

HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean

@@ -342,11 +342,19 @@ lemma wicks_theorem_congr {φs φs' : List 𝓕.FieldOp} (h : φs = φs') :
   simp
 
 remark wicks_theorem_context := "
-  Wick's theorem is one of the most important results in perturbative quantum field theory.
-  It expresses a time-ordered product of fields as a sum of terms consisting of
-  time-contractions of pairs of fields multiplied by the normal-ordered product of
-  the remaining fields. Wick's theorem is also the precursor to the diagrammatic
-  approach to quantum field theory called Feynman diagrams."
+  In perturbation quantum field theory, Wick's theorem allows
+  us to expand expectation values of time-ordered products of fields in terms of normal-orders
+  and time contractions.
+  The theorem is used to simplify the calculation of scattering amplitudes, and is the precurser
+  to Feynman diagrams.
+
+  There is are actually three different versions of Wick's theorem used.
+  The static version, the time-dependent version, and the normal-ordered time-dependent version.
+  HepLean contains a formalization of all three of these theorems in complete generality for
+  mixtures of bosonic and fermionic fields.
+
+  The statement of these theorems for bosons is simplier then when fermions are involved, since
+  one does not have to worry about the minus-signs picked up on exchanging 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,

HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean

@@ -35,7 +35,7 @@ namespace FieldSpecification
 variable {𝓕 : FieldSpecification}
 
 /-- For a field specification `𝓕`, the algebra `𝓕.FieldOpFreeAlgebra` is
-  the algebra is generated by creation and annihilation parts of field operators defined in
+  the free algebra generated by creation and annihilation parts of field operators defined in
   `𝓕.CrAnFieldOp`.
   It represents the algebra containing all possible products and linear combinations
   of creation and annihilation parts of field operators, without imposing any conditions.
@@ -44,6 +44,12 @@ abbrev FieldOpFreeAlgebra (𝓕 : FieldSpecification) : Type := FreeAlgebra ℂ
 
 namespace FieldOpFreeAlgebra
 
+remark naming_convention := "
+  For mathematicial objects defined in relation to `FieldOpFreeAlgebra` we will often postfix
+  their names with an `F` to indicate that they are related to the free algebra.
+  This is to avoid confusion when working within the context of `FieldOpAlgebra` which is defined
+  as a quotient of `FieldOpFreeAlgebra`."
+
 /-- Maps a creation and annihlation state to the creation and annihlation free-algebra. -/
 def ofCrAnOpF (φ : 𝓕.CrAnFieldOp) : FieldOpFreeAlgebra 𝓕 :=
   FreeAlgebra.ι ℂ φ

HepLean/PerturbationTheory/FieldStatistics/Basic.lean

@@ -26,7 +26,8 @@ namespace FieldStatistic
 
 variable {𝓕 : Type}
 
-/-- Field statistics form a commuative group isomorphic to `ℤ₂`. -/
+/-- Field statistics form a commuative group isomorphic to `ℤ₂` in which `bosonic` is the identity
+  and `fermionic` is the non-trivial element. -/
 @[simp]
 instance : CommGroup FieldStatistic where
   one := bosonic

HepLean/PerturbationTheory/WickContraction/Card.lean

@@ -236,6 +236,9 @@ def cardFun : ℕ → ℕ
   | 1 => 1
   | Nat.succ (Nat.succ n) => cardFun (Nat.succ n) + (n + 1) * cardFun n
 
+/-- The number of Wick contractions for `n : ℕ` fields, i.e. the cardinality of
+  `WickContraction n`, is equal to the terms in
+  Online Encyclopedia of Integer Sequences (OEIS) A000085. -/
 theorem card_eq_cardFun : (n : ℕ) → Fintype.card (WickContraction n) = cardFun n
   | 0 => by decide
   | 1 => by decide

docs/CuratedNotes/PerturbationTheory.html

@@ -1,6 +1,12 @@
 ---
 layout: default
 ---
+<style>
+  body {
+    color: black;
+  }
+</style>
+
 <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.9.0/styles/default.min.css">
 <script src="https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.9.0/highlight.min.js"></script>
 
@@ -31,10 +37,10 @@
 <p>
 {% for entry in site.data.perturbationTheory.parts %}
 {% if entry.type == "h1" %}
-  {{ entry.sectionNo }}. {{ entry.content }}<br>
+  <a href="#section-{{ entry.sectionNo }}" style="color: #2c5282;">{{ entry.sectionNo }}. {{ entry.content }}</a><br>
 {% endif %}
 {% if entry.type == "h2" %}
-  - {{ entry.sectionNo }}. {{ entry.content }}<br>
+&nbsp;&nbsp;&nbsp;&nbsp;<a href="#section-{{ entry.sectionNo }}"  style="color: #2c5282;">{{ entry.sectionNo }}. {{ entry.content }}</a><br>
 {% endif %}
 {% endfor %}
 </p>
@@ -43,10 +49,10 @@
 <br>
 {% for entry in site.data.perturbationTheory.parts %}
   {% if entry.type == "h1" %}
-    <h1>{{ entry.sectionNo }}. {{ entry.content }}</h1>
+    <h1 id="section-{{ entry.sectionNo }}">{{ entry.sectionNo }}. {{ entry.content }}</h1>
   {% endif %}
   {% if entry.type == "h2" %}
-    <h2>{{ entry.sectionNo }}. {{ entry.content }}</h2>
+    <h2 id="section-{{ entry.sectionNo }}">{{ entry.sectionNo }}. {{ entry.content }} </h2>
   {% endif %}
   {% if entry.type == "p" %}
     <p>{{ entry.content }}</p>

scripts/MetaPrograms/notes.lean

@@ -125,56 +125,55 @@ def perturbationTheory : Note where
       as it appears in HepLean. We start with some basic definitions.",
     .h1 "Field operators",
     .h2 "Field statistics",
-    .p "A quantum field can either be a bosonic or fermionic. This information is
-      contained in the inductive type `FieldStatistic`. This is defined as follows:",
     .name `FieldStatistic,
-    .p "Field statistics form a commuative group isomorphic to ℤ₂, with
-      the bosonic element of `FieldStatistic` being the identity element.",
-    .p "Most of our use of field statistics will come by comparing two field statistics
-      and picking up a minus sign when they are both fermionic. This concept is
-      made precise using the notion of an exchange sign, defined as:",
+    .name `FieldStatistic.instCommGroup,
     .name `FieldStatistic.exchangeSign,
-    .p "We use the notation `𝓢(a,b)` as shorthand for the exchange sign of `a` and `b`.",
     .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 "Field operators",
     .name `FieldSpecification.FieldOp,
     .name `FieldSpecification.CrAnFieldOp,
     .h2 "Field-operator free algebra",
     .name `FieldSpecification.FieldOpFreeAlgebra,
+    .name `FieldSpecification.FieldOpFreeAlgebra.naming_convention,
+    .name `FieldSpecification.FieldOpFreeAlgebra.superCommuteF,
     .h2 "Field-operator algebra",
     .name `FieldSpecification.FieldOpAlgebra,
+    .name `FieldSpecification.FieldOpAlgebra.superCommute,
     .h1 "Time ordering",
-    .name `FieldSpecification.timeOrderRel,
-    .name `FieldSpecification.timeOrderSign,
+    .name `FieldSpecification.crAnTimeOrderRel,
+    .name `FieldSpecification.crAnTimeOrderSign,
+    .name `FieldSpecification.FieldOpFreeAlgebra.timeOrderF,
+    .name `FieldSpecification.FieldOpAlgebra.timeOrder,
     .h1 "Normal ordering",
+    .name `FieldSpecification.normalOrderRel,
+    .name `FieldSpecification.normalOrderSign,
+    .name `FieldSpecification.FieldOpFreeAlgebra.normalOrderF,
+    .name `FieldSpecification.FieldOpAlgebra.normalOrder,
     .h1 "Wick Contractions",
     .h2 "Definition",
+    .name `WickContraction,
+    .name `WickContraction.GradingCompliant,
     .h2 "Constructors",
     .p "There are a number of ways to construct a Wick contraction from
       other Wick contractions or single contractions.",
+    .name `WickContraction.insertAndContract,
+    .name `WickContraction.erase,
+    .name `WickContraction.join,
     .h2 "Sign",
-    .h1 "Static Wick's theorem",
-    .h1 "Time-dependent Wick's theorem",
-    .h2 "Wick terms",
-    .name `FieldSpecification.wick_term_terminology,
-    .name `FieldSpecification.wick_term_none_eq_wick_term_cons,
-    .name `FieldSpecification.wick_term_some_eq_wick_term_optionEraseZ,
-    .name `FieldSpecification.wick_term_cons_eq_sum_wick_term,
-    .h2 "The case of the nil list",
-    .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 fields.
-      The proof of Wick's theorem follows from definitions and simple lemmas.",
-    .name `FieldSpecification.wicks_theorem_nil,
-    .h2 "Wick's theorems",
+    .name `WickContraction.sign,
+    .name `WickContraction.signInsertNone_eq_filterset,
+    .name `WickContraction.signInsertSome_mul_filter_contracted_of_not_lt,
+    .name `WickContraction.join_sign,
+    .h2 "Cardinality",
+    .name `WickContraction.card_eq_cardFun,
+    .h1 "Time and static contractions",
+    .h1 "The three Wick's theorems",
     .name `FieldSpecification.wicks_theorem,
-    .h1 "Wick's theorem with normal ordering"]
-
+    .name `FieldSpecification.FieldOpAlgebra.static_wick_theorem,
+    .name `FieldSpecification.FieldOpAlgebra.wicks_theorem_normal_order
+    ]
 
 unsafe def main (_ : List String) : IO UInt32 := do
   initSearchPath (← findSysroot)