feat: Add informal Feynman diagram

2024-12-03 10:18:41 +00:00 · 2024-12-03 10:18:41 +00:00 · 7e8c636f63
commit 7e8c636f63
parent a6c83bd142
1 changed files with 11 additions and 0 deletions
--- a/HepLean/PerturbationTheory/FeynmanDiagrams/Light.lean
+++ b/HepLean/PerturbationTheory/FeynmanDiagrams/Light.lean
@ -15,3 +15,14 @@ The implmentation here is done in conjunction with Wicks species etc.

 This file is currently a stub.
 -/
+
+informal_definition FeynmanDiagram where
+  math :≈ "
+    Let S be a WickSpecies
+    A Feynman diagram contains the following data:
+    - A type of vertices 𝓥 → S.𝓯 ⊕ S.𝓘.
+    - A type of edges 𝓔 → S.𝓕.
+    - A type of half-edges 𝓱𝓔 → 𝓔 × 𝓥 × S.𝓯.
+    Subject to the following conditions:
+    ...
+  "