feat: Update Wick theorem docs

HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean

@@ -501,18 +501,18 @@ def anPart (φ : 𝓕.FieldOp) : 𝓕.FieldOpAlgebra := ι (anPartF φ)
 lemma anPart_eq_ι_anPartF (φ : 𝓕.FieldOp) : anPart φ = ι (anPartF φ) := rfl
 
 @[simp]
-lemma anPart_negAsymp (φ : 𝓕.IncomingAsymptotic) :
+lemma anPart_negAsymp (φ : 𝓕.Fields × Lorentz.Contr 4) :
     anPart (FieldOp.inAsymp φ) = 0 := by
   simp [anPart, anPartF]
 
 @[simp]
-lemma anPart_position (φ : 𝓕.PositionFieldOp) :
+lemma anPart_position (φ : 𝓕.Fields × SpaceTime) :
     anPart (FieldOp.position φ) =
     ofCrAnFieldOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩ := by
   simp [anPart, ofCrAnFieldOp]
 
 @[simp]
-lemma anPart_posAsymp (φ : 𝓕.OutgoingAsymptotic) :
+lemma anPart_posAsymp (φ : 𝓕.Fields × Lorentz.Contr 4) :
     anPart (FieldOp.outAsymp φ) = ofCrAnFieldOp ⟨FieldOp.outAsymp φ, ()⟩ := by
   simp [anPart, ofCrAnFieldOp]
 
@@ -522,18 +522,18 @@ def crPart (φ : 𝓕.FieldOp) : 𝓕.FieldOpAlgebra := ι (crPartF φ)
 lemma crPart_eq_ι_crPartF (φ : 𝓕.FieldOp) : crPart φ = ι (crPartF φ) := rfl
 
 @[simp]
-lemma crPart_negAsymp (φ : 𝓕.IncomingAsymptotic) :
+lemma crPart_negAsymp (φ : 𝓕.Fields × Lorentz.Contr 4) :
     crPart (FieldOp.inAsymp φ) = ofCrAnFieldOp ⟨FieldOp.inAsymp φ, ()⟩ := by
   simp [crPart, ofCrAnFieldOp]
 
 @[simp]
-lemma crPart_position (φ : 𝓕.PositionFieldOp) :
+lemma crPart_position (φ : 𝓕.Fields × SpaceTime) :
     crPart (FieldOp.position φ) =
     ofCrAnFieldOp ⟨FieldOp.position φ, CreateAnnihilate.create⟩ := by
   simp [crPart, ofCrAnFieldOp]
 
 @[simp]
-lemma crPart_posAsymp (φ : 𝓕.OutgoingAsymptotic) :
+lemma crPart_posAsymp (φ : 𝓕.Fields × Lorentz.Contr 4) :
     crPart (FieldOp.outAsymp φ) = 0 := by
   simp [crPart]
 

HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean

@@ -506,5 +506,13 @@ lemma timeOrder_timeOrder_right (a b : 𝓕.FieldOpAlgebra) :
   rw [timeOrder_timeOrder_mid]
   simp
 
+/-- Time ordering is a projection. -/
+lemma timeOrder_timeOrder (a : 𝓕.FieldOpAlgebra) :
+    𝓣(𝓣(a)) = 𝓣(a) := by
+  trans 𝓣(𝓣(a) * 1)
+  · simp
+  · rw [← timeOrder_timeOrder_left]
+    simp
+
 end FieldOpAlgebra
 end FieldSpecification

HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean

@@ -34,11 +34,12 @@ super commutation relations between creation and annihilation operators.
 namespace FieldSpecification
 variable {𝓕 : FieldSpecification}
 
-/-- The creation and annihlation free-algebra.
-  The free algebra generated by `CrAnFieldOp`,
-  that is a position based states or assymptotic states with a specification of
-  whether the state is a creation or annihlation state.
-  As a module `FieldOpFreeAlgebra` is spanned by lists of `CrAnFieldOp`. -/
+/-- For a field specification `𝓕`, the algebra `𝓕.FieldOpFreeAlgebra` is
+  the algebra is 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.
+-/
 abbrev FieldOpFreeAlgebra (𝓕 : FieldSpecification) : Type := FreeAlgebra ℂ 𝓕.CrAnFieldOp
 
 namespace FieldOpFreeAlgebra
@@ -120,18 +121,18 @@ def crPartF : 𝓕.FieldOp → 𝓕.FieldOpFreeAlgebra := fun φ =>
   | FieldOp.outAsymp _ => 0
 
 @[simp]
-lemma crPartF_negAsymp (φ : 𝓕.IncomingAsymptotic) :
+lemma crPartF_negAsymp (φ : 𝓕.Fields × Lorentz.Contr 4) :
     crPartF (FieldOp.inAsymp φ) = ofCrAnOpF ⟨FieldOp.inAsymp φ, ()⟩ := by
   simp [crPartF]
 
 @[simp]
-lemma crPartF_position (φ : 𝓕.PositionFieldOp) :
+lemma crPartF_position (φ : 𝓕.Fields × SpaceTime) :
     crPartF (FieldOp.position φ) =
     ofCrAnOpF ⟨FieldOp.position φ, CreateAnnihilate.create⟩ := by
   simp [crPartF]
 
 @[simp]
-lemma crPartF_posAsymp (φ : 𝓕.OutgoingAsymptotic) :
+lemma crPartF_posAsymp (φ : 𝓕.Fields × Lorentz.Contr 4) :
     crPartF (FieldOp.outAsymp φ) = 0 := by
   simp [crPartF]
 
@@ -145,18 +146,18 @@ def anPartF : 𝓕.FieldOp → 𝓕.FieldOpFreeAlgebra := fun φ =>
   | FieldOp.outAsymp φ => ofCrAnOpF ⟨FieldOp.outAsymp φ, ()⟩
 
 @[simp]
-lemma anPartF_negAsymp (φ : 𝓕.IncomingAsymptotic) :
+lemma anPartF_negAsymp (φ : 𝓕.Fields × Lorentz.Contr 4) :
     anPartF (FieldOp.inAsymp φ) = 0 := by
   simp [anPartF]
 
 @[simp]
-lemma anPartF_position (φ : 𝓕.PositionFieldOp) :
+lemma anPartF_position (φ : 𝓕.Fields × SpaceTime) :
     anPartF (FieldOp.position φ) =
     ofCrAnOpF ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩ := by
   simp [anPartF]
 
 @[simp]
-lemma anPartF_posAsymp (φ : 𝓕.OutgoingAsymptotic) :
+lemma anPartF_posAsymp (φ : 𝓕.Fields × Lorentz.Contr 4) :
     anPartF (FieldOp.outAsymp φ) = ofCrAnOpF ⟨FieldOp.outAsymp φ, ()⟩ := by
   simp [anPartF]
 

HepLean/PerturbationTheory/FieldOpFreeAlgebra/TimeOrder.lean

@@ -26,7 +26,9 @@ open HepLean.List
 
 -/
 
-/-- Time ordering for the `FieldOpFreeAlgebra`. -/
+/-- Time ordering for the `FieldOpFreeAlgebra` defined by taking
+  `ofCrAnListF φs` to `crAnTimeOrderSign φs • ofCrAnListF (crAnTimeOrderList φs)`.
+  The notation `𝓣ᶠ(a)` is used for the time-ordering of `a : FieldOpFreeAlgebra`. -/
 def timeOrderF : FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpFreeAlgebra 𝓕 :=
   Basis.constr ofCrAnListFBasis ℂ fun φs =>
   crAnTimeOrderSign φs • ofCrAnListF (crAnTimeOrderList φs)

HepLean/PerturbationTheory/FieldSpecification/Basic.lean

@@ -45,28 +45,24 @@ structure FieldSpecification where
 namespace FieldSpecification
 variable (𝓕 : FieldSpecification)
 
-/-- An incoming asymptotic state is a field and a momentum. -/
-def IncomingAsymptotic : Type := 𝓕.Fields × Lorentz.Contr 4
-
-/-- An outgoing asymptotic states is a field and a momentum. -/
-def OutgoingAsymptotic : Type := 𝓕.Fields × Lorentz.Contr 4
-
-/-- A position state is a field and a space-time position. -/
-def PositionFieldOp : Type := 𝓕.Fields × SpaceTime
-
-/-- The type FieldOp is the inductive type combining the asymptotic states and position states. -/
+/-- For a field specification `𝓕`, the type `𝓕.FieldOp` is defined such that every element of
+  `FieldOp` corresponds either to:
+- an incoming asymptotic field operator `.inAsymp` specified by a field and a `4`-momentum.
+- an position operator `.position` specified by a field and a point in spacetime.
+- an outgoing asymptotic field operator `.outAsymp` specified by a field and a `4`-momentum.
+-/
 inductive FieldOp (𝓕 : FieldSpecification) where
-  | inAsymp : 𝓕.IncomingAsymptotic → 𝓕.FieldOp
-  | position : 𝓕.PositionFieldOp → 𝓕.FieldOp
-  | outAsymp : 𝓕.OutgoingAsymptotic → 𝓕.FieldOp
+  | inAsymp : 𝓕.Fields × Lorentz.Contr 4 → 𝓕.FieldOp
+  | position : 𝓕.Fields × SpaceTime → 𝓕.FieldOp
+  | outAsymp : 𝓕.Fields × Lorentz.Contr 4 → 𝓕.FieldOp
 
-/-- Taking a state to its underlying field. -/
+/-- Taking a field operator to its underlying field. -/
 def fieldOpToField : 𝓕.FieldOp → 𝓕.Fields
   | FieldOp.inAsymp φ => φ.1
   | FieldOp.position φ => φ.1
   | FieldOp.outAsymp φ => φ.1
 
-/-- The bool on `FieldOp` which is true only for position states. -/
+/-- The bool on `FieldOp` which is true only for position field operator. -/
 def statesIsPosition : 𝓕.FieldOp → Bool
   | FieldOp.position _ => true
   | _ => false

HepLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean

@@ -34,9 +34,9 @@ In this module in addition to defining `CrAnFieldOp` we also define some maps:
 namespace FieldSpecification
 variable (𝓕 : FieldSpecification)
 
-/-- To each state the specificaition of the type of creation and annihlation parts.
-  For asymptotic staes there is only one allowed part, whilst for position states
-  there is two. -/
+/-- To each field operator the specificaition of the type of creation and annihlation parts.
+  For asymptotic staes there is only one allowed part, whilst for position
+  field operator there is two. -/
 def fieldOpToCrAnType : 𝓕.FieldOp → Type
   | FieldOp.inAsymp _ => Unit
   | FieldOp.position _ => CreateAnnihilate
@@ -62,12 +62,19 @@ def fieldOpToCreateAnnihilateTypeCongr : {i j : 𝓕.FieldOp} → i = j →
     𝓕.fieldOpToCrAnType i ≃ 𝓕.fieldOpToCrAnType j
   | _, _, rfl => Equiv.refl _
 
-/-- A creation and annihlation state is a state plus an valid specification of the
-  creation or annihliation part of that state. (For asympotic states there is only one valid
-  choice). -/
+/--
+For a field specification `𝓕`, the type `𝓕.CrAnFieldOp` is defined such that every element
+corresponds to
+- an incoming asymptotic field operator `.inAsymp` and the unique element of `Unit`,
+  corresponding to the statement that an `inAsymp` state is a creation operator.
+- a position operator `.position` and an element of `CreateAnnihilate`,
+  corresponding to either the creation part or the annihilation part of a position operator.
+- an outgoing asymptotic field operator `.outAsymp` and the unique element of `Unit`,
+  corresponding to the statement that an `outAsymp` state is an annihilation operator.
+-/
 def CrAnFieldOp : Type := Σ (s : 𝓕.FieldOp), 𝓕.fieldOpToCrAnType s
 
-/-- The map from creation and annihlation states to their underlying states. -/
+/-- The map from creation and annihlation field operator to their underlying states. -/
 def crAnFieldOpToFieldOp : 𝓕.CrAnFieldOp → 𝓕.FieldOp := Sigma.fst
 
 @[simp]

HepLean/PerturbationTheory/FieldStatistics/Basic.lean

@@ -15,9 +15,8 @@ Basic properties related to whether a field, or list of fields, is bosonic or fe
 
 -/
 
-/-- A field can either be bosonic or fermionic in nature.
-  That is to say, they can either have Bose-Einstein statistics or
-  Fermi-Dirac statistics. -/
+/-- The type `FieldStatistic` is the type containing two elements `bosonic` and `fermionic`.
+  This type is used to specify if a field or operator obeys bosonic or fermionic statistics. -/
 inductive FieldStatistic : Type where
   | bosonic : FieldStatistic
   | fermionic : FieldStatistic

HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean

@@ -24,10 +24,12 @@ namespace FieldStatistic
 
 variable {𝓕 : Type}
 
-/-- The exchange sign of two field statistics is defined to be
-  `-1` if both field statistics are `fermionic` and `1` otherwise.
-  It is a group homomorphism from `FieldStatistic` to the group of homomorphisms from
-  `FieldStatistic` to `ℂ`. -/
+/-- The exchange sign is the group homomorphism `FieldStatistic →* FieldStatistic →* ℂ`,
+  which on two field statistics `a` and `b` is defined to be
+  `-1` if both `a` and `b` are `fermionic` and `1` otherwise.
+  It corresponds to the sign that one picks up when swapping fields `φ₁φ₂ → φ₂φ₁` with
+  `φ₁` and `φ₂` of statistics `a` and `b` respectively.
+  The notation `𝓢(a, b)` is used for the exchange sign of `a` and `b`. -/
 def exchangeSign : FieldStatistic →* FieldStatistic →* ℂ where
   toFun a :=
     {
@@ -55,8 +57,7 @@ def exchangeSign : FieldStatistic →* FieldStatistic →* ℂ where
     <;> fin_cases b <;> fin_cases c
     <;> simp
 
-/-- The echange sign of two field statistics.
-  Defined to be `-1` if both field statistics are `fermionic` and `1` otherwise. -/
+@[inherit_doc exchangeSign]
 scoped[FieldStatistic] notation "𝓢(" a "," b ")" => exchangeSign a b
 
 /-- The exchange sign is symmetric. -/

docs/CuratedNotes/PerturbationTheory.html

@@ -51,6 +51,11 @@ <h2>{{ entry.sectionNo }}. {{ entry.content }}</h2>
   {% if entry.type == "p" %}
     <p>{{ entry.content }}</p>
   {% endif %}
+  {% if entry.type == "warning" %}
+  <div class="alert alert-danger" role="alert">
+    <b>Warning:</b> {{ entry.content }}
+  </div>
+  {% endif %}
   {% if entry.type == "name" %}
 
   <div style="background-color: #f5f5f5; padding: 10px; border-radius: 4px;">

scripts/MetaPrograms/notes.lean

@@ -20,6 +20,7 @@ inductive NotePart
   | h2 : String → NotePart
   | p : String → NotePart
   | name : Name → NotePart
+  | warning : String → NotePart
 
 structure DeclInfo where
   line : Nat
@@ -73,6 +74,11 @@ def NotePart.toYMLM : ((List String) × Nat × Nat) →  NotePart → MetaM ((Li
   - type: p
     content: \"{s}\""
     return ⟨x.1 ++ [newString], x.2⟩
+  | x, NotePart.warning s =>
+    let newString := s!"
+  - type: warning
+    content: \"{s}\""
+    return ⟨x.1 ++ [newString], x.2⟩
   | x, NotePart.name n => do
   match (← RemarkInfo.IsRemark n) with
   | true =>
@@ -111,12 +117,13 @@ def perturbationTheory : Note where
   title := "Proof of Wick's theorem"
   curators := ["Joseph Tooby-Smith"]
   parts := [
+    .warning "This note is a work in progress and is not finished. Use with caution.",
     .h1 "Introduction",
     .name `FieldSpecification.wicks_theorem_context,
     .p "In this note we walk through the important parts of the proof of Wick's theorem
       for both fermions and bosons,
       as it appears in HepLean. We start with some basic definitions.",
-    .h1 "Preliminary 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:",
@@ -135,23 +142,25 @@ def perturbationTheory : Note where
     .name `FieldSpecification.singleBoson,
     .name `FieldSpecification.singleFermion,
     .name `FieldSpecification.doubleBosonDoubleFermion,
-    .h2 "FieldOp",
-    .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.PositionFieldOp,
-    .p "We will want to consider all three of these types of states simultanously so we define
-      and inductive type `FieldOp` which is the disjoint union of these three types of states.",
+    .h2 "Field operators",
     .name `FieldSpecification.FieldOp,
-    .h2 "Time ordering",
+    .name `FieldSpecification.CrAnFieldOp,
+    .h2 "Field-operator free algebra",
+    .name `FieldSpecification.FieldOpFreeAlgebra,
+    .h2 "Field-operator algebra",
+    .name `FieldSpecification.FieldOpAlgebra,
+    .h1 "Time ordering",
     .name `FieldSpecification.timeOrderRel,
     .name `FieldSpecification.timeOrderSign,
-    .h2 "Creation and annihilation states",
-    .h2 "Normal ordering",
+    .h1 "Normal ordering",
     .h1 "Wick Contractions",
-    .h1 "Proof of Wick's theorem",
+    .h2 "Definition",
+    .h2 "Constructors",
+    .p "There are a number of ways to construct a Wick contraction from
+      other Wick contractions or single contractions.",
+    .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,
@@ -163,7 +172,9 @@ def perturbationTheory : Note where
       The proof of Wick's theorem follows from definitions and simple lemmas.",
     .name `FieldSpecification.wicks_theorem_nil,
     .h2 "Wick's theorems",
-    .name `FieldSpecification.wicks_theorem]
+    .name `FieldSpecification.wicks_theorem,
+    .h1 "Wick's theorem with normal ordering"]
+
 
 unsafe def main (_ : List String) : IO UInt32 := do
   initSearchPath (← findSysroot)