Merge pull request #254 from HEPLean/FeynmanDiagrams

chore: File for momentum & position space wick contract

HepLean.lean

@@ -57,6 +57,8 @@ import HepLean.FeynmanDiagrams.Instances.Phi4
 import HepLean.FeynmanDiagrams.Momentum
 import HepLean.FeynmanDiagrams.Wick.Algebra
 import HepLean.FeynmanDiagrams.Wick.Contract
+import HepLean.FeynmanDiagrams.Wick.MomentumSpace
+import HepLean.FeynmanDiagrams.Wick.PositionSpace
 import HepLean.FeynmanDiagrams.Wick.Species
 import HepLean.FeynmanDiagrams.Wick.String
 import HepLean.FeynmanDiagrams.Wick.Theorem

HepLean/FeynmanDiagrams/Wick/Contract.lean

@@ -635,6 +635,10 @@ def unbound {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
     · exact List.Sorted.get_strictMono w.unboundList_sorted
     · exact fun ⦃a b⦄ a => a
 
+informal_lemma level_fintype where
+  math :≈ "Level is a finite type, as there are only finitely many ways to contract a Wick string."
+  deps :≈ [``Level]
+
 informal_definition HasEqualTimeContractions where
   math :≈ "The condition for a Wick contraction to have two fields contracted
     which are of equal time, i.e. come from the same vertex."

HepLean/FeynmanDiagrams/Wick/MomentumSpace.lean

@@ -0,0 +1,35 @@
+/-
+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.Contract
+/-!
+
+# Wick contraction in momentum space
+
+Every complete Wick contraction leads to a function on momenta, following
+the Feynman rules.
+
+-/
+
+namespace Wick
+
+informal_definition toMomentumTensorTree where
+  math :≈ "A function which takes a Wick contraction,
+    and corresponding momenta, and outputs the corresponding
+    tensor tree associated with that contraction. The rules for how this is done
+    is given by the `Feynman rules`.
+    The appropriate ring to consider here is a ring permitting the abstract notion of a
+    Dirac delta function. "
+  ref :≈ "
+    Some references for Feynman rules are:
+    - QED Feynman rules: http://hitoshi.berkeley.edu/public_html/129A/point.pdf,
+    - Weyl Fermions: http://scipp.ucsc.edu/~haber/susybook/feyn115.pdf."
+
+informal_definition toMomentumTensor where
+  math :≈ "The tensor associated to `toMomentumTensorTree` associated with a Wick contraction,
+    and corresponding internal momenta, and external momenta."
+  deps :≈ [``toMomentumTensorTree]
+
+end Wick

HepLean/FeynmanDiagrams/Wick/PositionSpace.lean

@@ -0,0 +1,25 @@
+/-
+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.Basic
+import HepLean.Meta.Informal
+/-!
+
+# Wick contraction in position space
+
+Every complete Wick contraction leads to a function on positions, following
+the Feynman rules.
+
+## Further reading
+
+The following reference provides a good resource for Wick contractions of external fields.
+- http://www.dylanjtemples.com:82/solutions/QFT_Solution_I-6.pdf
+
+-/
+
+namespace Wick
+
+
+end Wick

HepLean/FeynmanDiagrams/Wick/String.lean

@@ -95,11 +95,15 @@ inductive WickStringLast where
 open WickStringLast
 
 /-- A wick string is a representation of a string of fields from a theory.
-  E.g. `φ(x1) φ(x2) φ(y) φ(y) φ(y) φ(x3)`. The use of vertices in the Wick string
+  The use of vertices in the Wick string
   allows us to identify which fields have the same space-time coordinate.
 
   Note: Fields are added to `c` from right to left - matching how we would write this on
-  pen and paper. -/
+  pen and paper.
+
+  The incoming and outgoing fields should be viewed as asymptotic fields.
+  While the internal fields associated with vertices are fields at fixed space-time points.
+  -/
 inductive WickString : {ni : ℕ} → (i : Fin ni → 𝓔) → {n : ℕ} → (c : Fin n → 𝓔) →
   {no : ℕ} → (o : Fin no → 𝓔) → WickStringLast → Type where
   | empty : WickString Fin.elim0 Fin.elim0 Fin.elim0 incoming