feat: Informal refinements of Wick's theorem

2024-12-03 06:26:01 +00:00 · 2024-12-03 06:26:01 +00:00 · c9987bec0b
commit c9987bec0b
parent 35bab3197a
2 changed files with 10 additions and 1 deletions
--- a/HepLean/PerturbationTheory/Wick/Algebra.lean
+++ b/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.