Merge pull request #256 from HEPLean/FeynmanDiagrams

feat: Informal refinements of Wick's theorem

HepLean/PerturbationTheory/Wick/Algebra.lean

@@ -30,7 +30,9 @@ open PreFeynmanRule
 
 informal_definition WickAlgebra where
   math :≈ "
-    Modifications of this may be needed.
+    Modifications of this may be needed, in particular
+    need to add asympotic states.
+
     A structure with the following data:
     - A ℤ₂-graded algebra A.
     - A map from `ψ : 𝓔 × SpaceTime → A` where 𝓔 are field colors.

HepLean/PerturbationTheory/Wick/Theorem.lean

@@ -24,4 +24,11 @@ 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"
 
+informal_lemma wicks_theorem_vev where
+  math :≈ "Wick's theorem in a vev leaving only full contractions of Wick strings left."
+
+informal_lemma wicks_theorem_asymptotic_states where
+  math :≈ "Wick's theorem for a term in the Dyson series within asymptotic states
+    leaves only full contractions with the asymptotic states."
+
 end Wick