DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat: Add informal Wick map

Browse source
This commit is contained in:
jstoobysmith 2024-12-02 07:33:53 +00:00
parent 626bc38c61
commit 29ed297ff5
1 changed files with 6 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

7
HepLean/FeynmanDiagrams/Wick/Algebra.lean
View file

@ -108,6 +108,11 @@ 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]
end Wick