Tutorial for the Lean 4 Library physicslib4
Published:
Posts by Category
aqft
Local Isometric Invariant States
Published:
This blog post introduces the notion of “isometric invariant states” in Algebraic Quantum Field Theory (AQFT) in Minkowski spacetime (a theory defined in Unpacking the Haag Kastler Axioms) and also does the same for AQFT in Lorentzian spacetime (a theory defined in Haag Kastler Axioms in Curved Spacetime). Such “isometric invariant states” capture the physics of quantum systems that are invariant under isometries of spacetime.
GNS Construction Theorem
Published:
In this blog post we will state and prove the GNS Construction Theorem, which we make extensive use of in subsequent blog posts.
Haag Kastler Axioms in Curved Spacetime
Published:
This blog post presents the axioms governing Algebraic Quantum Field Theory (AQFT) in curved spacetime, generalizing the axioms of AQFT in Minkowski spacetime from the blog post Unpacking the Haag Kastler Axioms.
Unpacking the Haag Kastler Axioms
Published:
The aim of this blog post is to “sharpen” the statement of the Haag Kastler axioms (Haag and Kastler). As originally presented they were revolutionary. However, several small details were left under-specified. This blog post will hopefully clarify some of these details.
functional-analysis
Spectral Theorem for Unbounded, Self-Adjoint Operators
Published:
Here we will state and prove the Spectral Theorem for Unbounded, Self-Adjoint Operators. This theorem extends the Spectral Theorem for Bounded, Self-Adjoint Operators to the small handful of genuinely unbounded self-adjoint operators that do arise in AQFT — the momentum operator on Minkowski space is a standard example — even though the large majority of operators of interest there, local observables in particular, are bounded. It is a prerequisite for handling these unbounded operators within the rest of the AQFT work that motivated this series.
Spectral Theorem for Bounded, Self-Adjoint Operators
Published:
Here we will state and prove the Spectral Theorem for Bounded, Self-Adjoint Operators. This theorem sits at the core of much of AQFT, and extensive use of this theorem will be made in subsequent work.
lcaqft
Local Isometric Invariant States
Published:
This blog post introduces the notion of “isometric invariant states” in Algebraic Quantum Field Theory (AQFT) in Minkowski spacetime (a theory defined in Unpacking the Haag Kastler Axioms) and also does the same for AQFT in Lorentzian spacetime (a theory defined in Haag Kastler Axioms in Curved Spacetime). Such “isometric invariant states” capture the physics of quantum systems that are invariant under isometries of spacetime.
Haag Kastler Axioms in Curved Spacetime
Published:
This blog post presents the axioms governing Algebraic Quantum Field Theory (AQFT) in curved spacetime, generalizing the axioms of AQFT in Minkowski spacetime from the blog post Unpacking the Haag Kastler Axioms.