Merge pull request #253 from HEPLean/FeynmanDiagrams

feat: Informal def for Wick Contraction

HepLean.lean

@@ -59,6 +59,7 @@ import HepLean.FeynmanDiagrams.Wick.Algebra
 import HepLean.FeynmanDiagrams.Wick.Contract
 import HepLean.FeynmanDiagrams.Wick.Species
 import HepLean.FeynmanDiagrams.Wick.String
+import HepLean.FeynmanDiagrams.Wick.Theorem
 import HepLean.FlavorPhysics.CKMMatrix.Basic
 import HepLean.FlavorPhysics.CKMMatrix.Invariants
 import HepLean.FlavorPhysics.CKMMatrix.PhaseFreedom

HepLean/FeynmanDiagrams/Wick/Algebra.lean

@@ -59,7 +59,16 @@ informal_definition toWickAlgebra where
 informal_definition timeOrder where
   math :≈ "A function from WickMonomial to WickAlgebra which takes a monomial and
     returns the monomial with the fields time ordered, with the correct sign
-    determined by the Koszul sign factor."
+    determined by the Koszul sign factor.
+
+    If two fields have the same time, then their order is preserved e.g.
+    T(ψ₁(t)ψ₂(t)) = ψ₁(t)ψ₂(t)
+    and
+    T(ψ₂(t)ψ₁(t)) = ψ₂(t)ψ₁(t).
+    This allows us to make sense of the construction in e.g.
+    https://www.physics.purdue.edu/~clarkt/Courses/Physics662/ps/qftch32.pdf
+    which permits normal-ordering within time-ordering.
+    "
   deps :≈ [``WickAlgebra, ``WickMonomial]
 
 informal_definition normalOrder where
@@ -99,6 +108,15 @@ informal_lemma timeOrder_pair where
   deps :≈ [``WickAlgebra, ``WickMonomial.timeOrder, ``WickMonomial.normalOrder,
     ``contraction]
 
-/-! TODO: Need to set up data and structure for vaccum expectation values. -/
+informal_definition WickMap where
+  math :≈ "A linear map `vev` from the Wick algebra `A` to the underlying field such that
+   `vev(...ψd(t)) = 0` and `vev(ψc(t)...) = 0`."
+  physics :≈ "An abstraction of the notion of a vacuum expectation value, containing
+    the necessary properties for lots of theorems to hold."
+  deps :≈ [``WickAlgebra, ``WickMonomial]
+
+informal_lemma normalOrder_wickMap where
+  math :≈ "Any normal ordering maps to zero under a Wick map."
+  deps :≈ [``WickMap, ``WickMonomial.normalOrder]
 
 end Wick

HepLean/FeynmanDiagrams/Wick/Contract.lean

@@ -641,12 +641,16 @@ informal_definition HasEqualTimeContractions where
   deps :≈ [``WickContract]
 
 informal_definition IsConnected where
-  math :≈ "The condition for a Wick contraction that for any two vertices
+  math :≈ "The condition for a full Wick contraction that for any two vertices
     (including external vertices) are connected by contractions."
   deps :≈ [``WickContract]
 
 informal_definition HasVacuumContributions where
-  math :≈ "The condition for a Wick contraction to have a vacuum contribution."
+  math :≈ "The condition for a full Wick contraction to have a vacuum contribution."
+  deps :≈ [``WickContract]
+
+informal_definition IsOneParticleIrreducible where
+  math :≈ "The condition for a full Wick contraction to be one-particle irreducible."
   deps :≈ [``WickContract]
 
 end WickContract

HepLean/FeynmanDiagrams/Wick/Theorem.lean

@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.FeynmanDiagrams.Wick.Species
+/-!
+
+# Wick's theorem
+
+Wick's theorem is related to a result in probability theory called Isserlis' theorem.
+
+-/
+
+namespace Wick
+open CategoryTheory
+open FeynmanDiagram
+open PreFeynmanRule
+
+informal_lemma wicks_theorem where
+  math :≈ "Wick's theorem for fields which are not normally ordered."
+
+informal_lemma wicks_theorem_normal_order where
+  math :≈ "Wick's theorem for which fields at the same space-time point are normally ordered."
+  ref :≈ "https://www.physics.purdue.edu/~clarkt/Courses/Physics662/ps/qftch32.pdf"
+
+end Wick