4. Stone's theorem🔗

This chapter describes how the library encodes one-parameter unitary groups and their generators, and proves Stone's theorem. It corresponds to Section 10.4 of the blueprint, which, like Sections 10.2 and 10.3, follows Hall's Quantum Theory for Mathematicians. It builds on the unbounded chapter: a generator is an unbounded operator, and the unitary group e^{itA} comes from the functional calculus of the unbounded spectral theorem. The chapter also covers two results on unitary groups that Section 10.6 of the blueprint states for the Haag–Kastler axioms: the positive-energy condition, which rests on Stone's theorem, and the passage from weak to strong continuity, which supplies its hypothesis.

4.1. Overview🔗

As you will recall, a quantum state evolves as \psi(t) = e^{-it\hat H}\psi_0 (with \hbar = 1), and the Schrödinger equation i\,d\psi/dt = \hat H\psi says that the derivative of the evolution at t = 0 is -i\hat H. Every continuous one-parameter symmetry works the same way: translations along a direction are generated by a component of momentum, rotations about an axis by a component of angular momentum. For a bounded \hat H the exponential is a norm-convergent power series. The Hamiltonians of physics are usually unbounded, and then neither the series nor the derivative makes sense on all of H. Stone's theorem makes the correspondence exact.

A one-parameter unitary group is a family of unitaries U(t), t \in \mathbb{R}, with U(0) = \mathbf{1} and U(s + t) = U(s)U(t). It is strongly continuous when t \mapsto U(t)\psi is continuous for every \psi. Norm continuity would be too strong: the translations (U(t)\psi)(x) = \psi(x + t) on L^2(\mathbb{R}) are strongly but not norm continuous. The infinitesimal generator of U is

A\psi = \lim_{t \to 0,\ t \neq 0} \frac{1}{i}\,\frac{U(t)\psi - \psi}{t},

defined on the \psi for which the limit exists. With this sign, e^{itA} has generator A, and the time evolution e^{-it\hat H} has generator -\hat H. Stone's theorem says that U \mapsto A and A \mapsto (t \mapsto e^{itA}) are mutually inverse bijections between the strongly continuous one-parameter unitary groups and the self-adjoint operators on H.

The section is formalised in these parts:

One-parameter unitary groups. The group law and strong continuity; continuity at t = 0 suffices; U(t)^* = U(-t); and conjugation by a unitary W: t \mapsto WU(t)W^{-1} is again a one-parameter unitary group, with generator WAW^{-1} on W\,\mathrm{Dom}(A).
The generator. Its domain and value, both characterised by the limit above; the symmetry identity \langle \varphi, A\psi \rangle = \langle A\varphi, \psi \rangle; and, for \psi \in \mathrm{Dom}(A), U(t)\psi \in \mathrm{Dom}(A), AU(t)\psi = U(t)A\psi, and t \mapsto U(t)\psi is differentiable with derivative iAU(t)\psi. This last statement is the Schrödinger equation in the Hilbert-space sense.
The bounded case. For bounded self-adjoint P, the exponential series \exp(itP) is a strongly continuous one-parameter unitary group with generator P, defined on all of H.
The exponential of a self-adjoint operator. For self-adjoint A, e^{itA} = \int e^{it\lambda} \, d\mu^A(\lambda) is a strongly continuous one-parameter unitary group whose generator is A, domains included.
Density. The generator of a strongly continuous one-parameter unitary group is densely defined.
Stone's theorem. The generator A of a strongly continuous one-parameter unitary group U is self-adjoint, U(t) = e^{itA} for every t, and A is the only self-adjoint operator with this property.
Positive energy. A family of unitaries has positive energy when it is a strongly continuous one-parameter unitary group whose generator, in general unbounded, is a positive operator. By Stone's theorem this holds exactly when V(t) = e^{itA} with A positive and self-adjoint. It is the form in which the library states the spectrum condition.
Weak continuity. A family of unitaries U(x), indexed by any topological space, whose matrix elements \langle \xi, U(x)\eta \rangle are continuous for \xi, \eta in a dense set, is strongly continuous.

Every statement of Section 10.4 is proved in Lean, as are the positive-energy results and the weak-continuity lemma, with no sorry. The four standard results the blueprint states without proof (the Bochner integral, smooth approximate identities, two facts about derivatives, and the calculus of convolutions) are Mathlib theorems. Where a result assumes anything of H, it is completeness; no result assumes H separable or nonzero. The declarations of Section 10.4 are in the namespace Physicslib4.Spectral.Stone, positive energy is in Physicslib4.AQFT, and the weak-continuity lemma is in Physicslib4.

4.2. Design🔗

The sign conventions for generators and time translations are stated once in the conventions chapter, under Sign and notational conventions.

Section 10.4 of the blueprint has no paragraph labelled "Formalization note"; its remarks on the Lean formalization sit inside entries, mostly naming the Mathlib results a proof uses, and this section links the entries it draws on. The conventions of the unbounded chapter carry over: an unbounded operator is a partial linear map H →ₗ.[ℂ] H, equality of operators includes equality of domains, symmetry assumes no density, and self-adjointness is Mathlib's IsSelfAdjoint.

4.2.1. Unitarity, the group law and continuity are separate🔗

A unitary is a linear isometry equivalence H ≃ₗᵢ[ℂ] H, as everywhere in the library, so a family of unitaries is a function U : ℝ → (H ≃ₗᵢ[ℂ] H) and is unitary by its type. The group law is the structure IsOneParameterUnitaryGroup U, whose two fields state U(0)\psi = \psi and U(s + t)\psi = U(s)U(t)\psi vector by vector. Strong continuity is the separate predicate IsStronglyContinuous U, defined for any family. Each result assumes only what it uses: the symmetry identity of the generator needs the group law but not continuity, and the weak-continuity lemma needs neither.

4.2.2. The generator is a partial map defined by a limit🔗

generator U is a partial linear map. Its domain, generatorDomain U, is the submodule of the \psi for which the difference quotient generatorQuotient U ψ t, that is (it)^{-1}(U(t)\psi - \psi), converges along the punctured filter 𝓝[≠] 0; its value is Mathlib's limUnder along that filter. The domain is exactly the set where the orbit has a derivative at t = 0, as in the blueprint (def:hall-10.13). exists_generator_eq_iff handles membership and value together: \psi is in the domain with A\psi = \chi exactly when the quotient tends to \chi. At t = 0 the quotient is 0, by Lean's convention 0^{-1} = 0, and the punctured limit never uses this value.

The definition assumes nothing about U: no group law, no continuity, and no density of the domain, which is a theorem rather than part of the type. Because the library's symmetry predicate does not presuppose a dense domain, the symmetry identity is itself the statement that the generator is symmetric, isSymmetric_generator, for every one-parameter unitary group (the remark in lmm:generator-symmetry-identity).

4.2.3. The exponential comes from the functional calculus🔗

For unbounded A the series \sum_n (itA)^n/n! is meaningless, since A^n\psi need not be defined. The library defines e^{itA} as expUnitary hA t, the bounded integral of f_t(\lambda) = e^{it\lambda} (expFun t) against the spectral measure of A, which is unitary and is made an element of H ≃ₗᵢ[ℂ] H. functionalCalculus_expFun identifies it with the functional calculus f_t(A), so the results on bounded integrals against a projection-valued measure apply. The spectral measure and the functional calculus are described in the unbounded chapter. The bounded case uses Mathlib's series NormedSpace.exp instead, which needs no spectral theorem.

expUnitary takes the proof hA : IsSelfAdjoint A as an argument, since only a self-adjoint operator has a spectral measure. For this reason Stone's theorem states the self-adjointness of the generator as an existential, ∃ hA : IsSelfAdjoint (generator U), …, and writes e^{itA} as expUnitary hA t.

Strong continuity of e^{itA} and its derivative at t = 0 come from norm identities: \|e^{itA}\psi - e^{isA}\psi\|^2 = \int |e^{it\lambda} - e^{is\lambda}|^2 \, d\mu^A_\psi(\lambda), and for \psi \in \mathrm{Dom}(A) the squared error of the difference quotient is \int |g_t(\lambda) - \lambda|^2 \, d\mu^A_\psi(\lambda), with g_t(\lambda) = (e^{it\lambda} - 1)/(it). Both tend to 0 by dominated convergence in Mathlib's filter form, tendsto_integral_filter_of_dominated_convergence (the proofs of lmm:exp-strongly-continuous and lmm:exp-derivative-at-zero), along s \to t and along the punctured filter at 0, with dominating functions 4 and 4\lambda^2; the second is integrable because \psi \in \mathrm{Dom}(A). So the generator of e^{itA} extends A. It is symmetric, and a self-adjoint operator has no proper symmetric extension, so it equals A (prpstn:hall-10.14).

4.2.4. Density by smoothing🔗

For a real weight f, the average B_f\psi = \int f(\tau)\,U(\tau)\psi \, d\tau is average U f ψ, a Bochner integral. The density proof (lmm:hall-10.18) writes it as a convolution, U(t)B_f\psi = (f \star g_\psi)(-t) with g_\psi(x) = U(-x)\psi (average_eq_convolution), so that Mathlib's convolution calculus does the analysis. HasCompactSupport.hasDerivAt_convolution_left differentiates t \mapsto U(t)B_f\psi for a compactly supported C^1 weight, which puts B_f\psi in the domain of the generator, and ContDiffBump.convolution_tendsto_right_of_continuous gives B_{f_n}\psi \to \psi for normalised bump functions of outer radius 1/(n + 1). The density theorem assumes H complete: without completeness, Mathlib's Bochner integral is 0. The argument is the one-parameter case of Gårding's smoothing argument.

4.2.5. The proof of the theorem, and uniqueness🔗

The proof of stone follows the blueprint (thrm:hall-10.15). The generator A is essentially self-adjoint, because the deficiency subspaces \mathrm{Ker}(A^* \mp i\mathbf{1}) are trivial: for \psi in one of them and \varphi \in \mathrm{Dom}(A), \langle U(t)\varphi, \psi \rangle is a bounded solution of y' = \pm y, hence 0. The orbits of U and of e^{itA^{(\mathrm{cl})}}, for the closure A^{(\mathrm{cl})}, agree on \mathrm{Dom}(A), since their difference starts at 0 and has constant norm, so U(t) = e^{itA^{(\mathrm{cl})}} by density. The generator of e^{itA^{(\mathrm{cl})}} is A^{(\mathrm{cl})}, so A = A^{(\mathrm{cl})}.

Uniqueness needs no further argument. The generator is a function of U, so if U(t) = e^{itB} for a self-adjoint B, the generator of U is the generator of e^{itB}, which is B. The same argument gives generator_eq_of_eq_expUnitary, for any family V with V(t) = e^{itB}. For bounded operators, exp_generator_unique proves uniqueness directly, by differentiating \exp(itP) at t = 0.

4.2.6. Positive energy is a property of the generator🔗

IsPositiveEnergy V is a structure with three fields: the group law, strong continuity, and positivity of generator V, which is the library's Spectral.Unbounded.IsPositive (symmetric, with \mathrm{Re}\langle \psi, A\psi \rangle \ge 0 on the domain). The condition is imposed on the generator itself, which may be unbounded, and needs no self-adjointness hypothesis, since the generator is defined for every family. Stone's theorem then gives the textbook form (thrm:positive-energy-iff-exp): V has positive energy exactly when V(t) = e^{itA} with A positive and self-adjoint. For time translations the unitaries are U(t) = e^{it\hat H}, in the convention U(a) = e^{-iP\cdot a}, where P\cdot a = -P^0 a^0 + \vec P\cdot\vec a uses the signature (-,+,+,+) and P^0 = \hat H; this is the inverse of the Schrödinger evolution, so their generator is \hat H and positive energy says \hat H \ge 0.

The definition refers to no spacetime. A vacuum state (HaagKastlerNet.IsVacuumState) asks for positive energy of the unitary group of every future-timelike translation subgroup, and a ground state for a flow, in Minkowski or curved spacetime, asks it of the unitary group implementing the flow; see the Haag–Kastler chapter and the curved-spacetime chapter.

4.2.7. Where weak continuity suffices🔗

Stone's theorem assumes strong continuity, and for a one-parameter unitary group continuity at t = 0 suffices (isStronglyContinuous_iff_tendsto_zero). In the applications the unitaries come from the GNS construction of an invariant state \omega, where what can be computed are the matrix elements \langle \pi(a)\Omega, U(g)\pi(b)\Omega \rangle = \omega(a^*\gamma_g(b)) on the dense set of vectors \pi(a)\Omega. strongContinuous_of_weak upgrades their continuity to strong continuity. It is stated for any family of unitaries indexed by a topological space, with no group law and no completeness of H, and taking the dense set to be all of H shows that a weakly continuous family of unitaries is strongly continuous. The GNS theorems exists_gns_unitary_of_invariant_strongContinuous and its bundled form use it (thrm:invariant-state-gns-unitary-general; see also the GNS chapter).

4.3. Main definitions and theorems🔗

Definitions are shown with their docstrings, which give the mathematics and the blueprint entry; theorems with their statements, as Lean prints them, and a line or two of explanation. Each subsection opens with the blueprint entries it covers. In the printed statements, H ≃ₗᵢ[ℂ] H is the type of unitaries, H →ₗ.[ℂ] H that of unbounded operators, and ↑ is a coercion (a bounded operator regarded as a linear map, a real number regarded as complex). Names in the printed statements are relative to the opened namespaces: HasDenseDomain and IsPositive are Spectral.Unbounded.HasDenseDomain and Spectral.Unbounded.IsPositive, and generator and expUnitary are in Spectral.Stone. The four standard results that the blueprint imports (thrm:bochner-integral, lmm:smooth-approximate-identity, prpstn:calculus-facts, lmm:convolution-facts) are Mathlib theorems, named in the blueprint. For the declarations not shown here, see the API documentation and the files listed at the end of the chapter.

4.3.1. One-parameter unitary groups and their generators🔗

Blueprint: def:hall-10.11, lmm:strongly-continuous-iff-at-zero, lmm:unitary-group-inner-adjoint, def:hall-10.13, lmm:generator-spec, lmm:generator-symmetry-identity, lmm:generator-const, lmm:conj-unitary-group, lmm:generator-conj, lmm:orbit-hasDerivAt, lmm:generator-commutes, lmm:hall-10.17.

structure

Physicslib4.Spectral.Stone.IsOneParameterUnitaryGroup.{u_1}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
  (U : ℝ → H ≃ₗᵢ[ℂ] H) : Prop
Physicslib4.Spectral.Stone.IsOneParameterUnitaryGroup.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  (U : ℝ → H ≃ₗᵢ[ℂ] H) : Prop

A family U(t), t ∈ ℝ, of unitary operators on H is a one-parameter unitary group: U(0) = 𝟙 and U(s + t) = U(s)U(t) for all real s and t.

Symmetries of a quantum system that depend on one real parameter, such as time translations, translations along a fixed direction or rotations about a fixed axis, act on the Hilbert space by unitary operators, and performing two of them in succession adds the parameters. The group law forces U(t)* = U(t)⁻¹ = U(−t) (IsOneParameterUnitaryGroup.adjoint_eq). No continuity in t is assumed; that is IsStronglyContinuous, and Stone's theorem (stone) uses both.

Implementation note: a unitary is a linear isometry equivalence H ≃ₗᵢ[ℂ] H, as elsewhere in the project, so each U(t) is unitary by its type and the structure records only the two group identities, stated vector by vector.

Blueprint: def:hall-10.11

Constructor

Physicslib4.Spectral.Stone.IsOneParameterUnitaryGroup.mk.{u_1}

Fields

map_zero : ∀ (ψ : H), (U 0) ψ = ψ

U(0) is the identity: U(0)ψ = ψ for every ψ.

map_add : ∀ (s t : ℝ) (ψ : H), (U (s + t)) ψ = (U s) ((U t) ψ)

The group law U(s + t) = U(s)U(t), applied to each vector ψ.

def

Physicslib4.Spectral.Stone.IsStronglyContinuous.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : ℝ → H ≃ₗᵢ[ℂ] H) :
  Prop
Physicslib4.Spectral.Stone.IsStronglyContinuous.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  (U : ℝ → H ≃ₗᵢ[ℂ] H) : Prop

A family U(t) of unitary operators is strongly continuous: t ↦ U(t)ψ is continuous for every vector ψ.

Strong continuity asks that each state vector move continuously, ‖U(t)ψ − U(s)ψ‖ → 0 as s → t, and not that U(s) → U(t) in operator norm. The weaker notion is the one physics needs: the translations (U(t)ψ)(x) = ψ(x + t) on L²(ℝ) are strongly continuous but not norm continuous. For a one-parameter unitary group, continuity at t = 0 already suffices (isStronglyContinuous_iff_tendsto_zero).

Implementation note: the predicate applies to any family U : ℝ → (H ≃ₗᵢ[ℂ] H); the group law is the separate hypothesis IsOneParameterUnitaryGroup U. Continuity is Mathlib's Continuous, for the norm topology of H.

Blueprint: def:hall-10.11

def

Physicslib4.Spectral.Stone.generator.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : ℝ → H ≃ₗᵢ[ℂ] H) :
  H →ₗ.[ℂ] H
Physicslib4.Spectral.Stone.generator.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  (U : ℝ → H ≃ₗᵢ[ℂ] H) : H →ₗ.[ℂ] H

The infinitesimal generator A of a family U(t) of unitaries: Aψ is the limit of (1/i)(U(t)ψ − ψ)/t as t → 0, t ≠ 0, on the subspace of vectors ψ where that limit exists.

Formally U(t) = e^(itA), and A is −i times the derivative of U(t) at t = 0. Stone's theorem (stone) makes this exact: for a strongly continuous one-parameter unitary group, A is self-adjoint and U(t) = e^(itA). Conversely, for self-adjoint A the group e^(itA) has generator A (generator_expUnitary). This is how observables arise from symmetries: the generator of the translations (U(t)ψ)(x) = ψ(x + t) on L²(ℝ) is the momentum operator −i d/dx, and in this sign convention a time evolution e^(−itĤ) has generator −Ĥ. The definition itself assumes nothing about U: no group law, no continuity, and no density of the domain. Those enter only the results about A; density of the domain is hasDenseDomain_generator.

Implementation note: A is a LinearPMap (H →ₗ.[ℂ] H) with domain generatorDomain U, and its value is Mathlib's limUnder along the punctured filter 𝓝[≠] 0, which is the limit wherever one exists. Membership and value are handled together by exists_generator_eq_iff.

Blueprint: def:hall-10.13

Continuity at t = 0 suffices (isStronglyContinuous_iff_tendsto_zero), and U(t)^* = U(-t) (IsOneParameterUnitaryGroup.adjoint_eq). The domain and value of the generator are characterised by the limit in exists_generator_eq_iff, and the symmetry identity is isSymmetric_generator. For \psi \in \mathrm{Dom}(A), the orbit t \mapsto U(t)\psi stays in the domain and has derivative iAU(t)\psi = iU(t)A\psi (IsOneParameterUnitaryGroup.hasDerivAt_orbit_generator). The trivial group has generator 0 (generator_refl); the conjugated group WU(t)W^{-1} is a strongly continuous one-parameter unitary group (IsOneParameterUnitaryGroup.conj, IsStronglyContinuous.conj) with generator WAW^{-1} on W\,\mathrm{Dom}(A) (mem_generator_conj_domain_iff, generator_conj_apply).

4.3.2. The bounded case🔗

Blueprint: lmm:exp-bounded-unitary-group, lmm:exp-bounded-hasDerivAt, lmm:generator-exp-bounded.

For bounded self-adjoint P, \exp(itP) is Mathlib's NormedSpace.exp of (t\,i)P. It is a one-parameter unitary group (exists_isOneParameterUnitaryGroup_exp), strongly continuous (isStronglyContinuous_of_eq_exp), and its generator is P on all of H:

open Physicslib4 Spectral Stone in
Physicslib4.Spectral.Stone.generator_eq_of_eq_exp.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
  [CompleteSpace H] {P : H →L[ℂ] H} {V : ℝ → H ≃ₗᵢ[ℂ] H}
  (hV : ∀ (t : ℝ) (x : H), (V t) x = (NormedSpace.exp ((↑t * Complex.I) • P)) x) : generator V = (↑P).toPMap ⊤#check generator_eq_of_eq_exp

Physicslib4.Spectral.Stone.generator_eq_of_eq_exp.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
  [CompleteSpace H] {P : H →L[ℂ] H} {V : ℝ → H ≃ₗᵢ[ℂ] H}
  (hV : ∀ (t : ℝ) (x : H), (V t) x = (NormedSpace.exp ((↑t * Complex.I) • P)) x) : generator V = (↑P).toPMap ⊤

(↑P).toPMap ⊤ is P as a partial map with domain H. The statement assumes nothing of P; self-adjointness is needed only for V to exist.

4.3.3. The unitary group of a self-adjoint operator🔗

Blueprint: lmm:exp-unitary, def:exp-unitary-group, lmm:exp-group-law, lmm:exp-strongly-continuous, lmm:functional-calculus-sub-bounded, lmm:exp-quotient-norm-identity, lmm:exp-derivative-at-zero, prpstn:hall-10.14.

def

Physicslib4.Spectral.Stone.expUnitary.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
  {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) (t : ℝ) : H ≃ₗᵢ[ℂ] H
Physicslib4.Spectral.Stone.expUnitary.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  [CompleteSpace H] {A : H →ₗ.[ℂ] H}
  (hA : IsSelfAdjoint A) (t : ℝ) :
  H ≃ₗᵢ[ℂ] H

The unitary operator e^(itA) of a self-adjoint operator A, defined by the spectral theorem as ∫ e^(itλ) dμ(A)(λ).

When A is unbounded the exponential series makes no sense, since Aⁿψ need not be defined. The spectral theorem replaces it: e^(itA) integrates the function e^(itλ) against the spectral measure μ(A). Because |e^(itλ)| = 1 the result is a bounded operator defined on all of H, and it is unitary (integral_expFun_mem_unitary). As a function of t it is a strongly continuous one-parameter unitary group (isOneParameterUnitaryGroup_expUnitary, isStronglyContinuous_expUnitary) with infinitesimal generator A (generator_expUnitary). For a Hamiltonian Ĥ, the time evolution operator e^(−itĤ) is this unitary at the parameter −t.

Implementation note: the operator is the bounded integral ProjectionValuedMeasure.integral of expFun t against Unbounded.spectralMeasure hA, made an element of H ≃ₗᵢ[ℂ] H by Unitary.linearIsometryEquiv. That it is the functional calculus f_t(A) is functionalCalculus_expFun. The definition takes the proof hA of self-adjointness as an argument, which is why stone states self-adjointness of the generator as an existential.

Blueprint: def:exp-unitary-group

The group law, strong continuity and the generator are one statement, the blueprint's Proposition 10.14:

open Physicslib4 Spectral Stone in
Physicslib4.Spectral.Stone.generator_expUnitary.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
  [CompleteSpace H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) :
  IsOneParameterUnitaryGroup (expUnitary hA) ∧ IsStronglyContinuous (expUnitary hA) ∧ generator (expUnitary hA) = A#check generator_expUnitary

Physicslib4.Spectral.Stone.generator_expUnitary.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
  [CompleteSpace H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) :
  IsOneParameterUnitaryGroup (expUnitary hA) ∧ IsStronglyContinuous (expUnitary hA) ∧ generator (expUnitary hA) = A

The last conjunct is an equality of partial maps, so \mathrm{Dom}(A) is exactly the set of \psi for which the difference quotient converges. The derivative of e^{itA}\psi at 0 is tendsto_generatorQuotient_expUnitary.

4.3.4. Density of the generator's domain🔗

Blueprint: lmm:averaging-translate, lmm:averaging-in-generator-domain, lmm:averaging-approximates, lmm:hall-10.18.

def

Physicslib4.Spectral.Stone.average.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : ℝ → H ≃ₗᵢ[ℂ] H)
  (f : ℝ → ℝ) (ψ : H) : H
Physicslib4.Spectral.Stone.average.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  (U : ℝ → H ≃ₗᵢ[ℂ] H) (f : ℝ → ℝ)
  (ψ : H) : H

The average B_f ψ = ∫ f(τ) U(τ)ψ dτ of the orbit of a vector ψ against a real weight function f.

Averaging the orbit τ ↦ U(τ)ψ against a smooth bump f smooths it in the group parameter: the average lies in the domain of the generator when f is continuously differentiable with compact support (average_mem_generator_domain), and it tends to ψ as f concentrates at τ = 0 (tendsto_average_bump). These two facts give density of the generator's domain (hasDenseDomain_generator). This is the one-parameter case of Gårding's smoothing argument.

Implementation note: the integral is Mathlib's Bochner integral for Lebesgue measure on ℝ, which is 0 when the integrand is not integrable or H is not complete. The results that use the average assume U strongly continuous and f a compactly supported C¹ weight or a bump function. To use Mathlib's convolution calculus, the average is rewritten as a convolution f ⋆ g_ψ with g_ψ(x) = U(−x)ψ (average_eq_convolution, which holds for every f).

Blueprint: lmm:averaging-translate

open Physicslib4 Spectral Stone in
Physicslib4.Spectral.Stone.hasDenseDomain_generator.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
  [CompleteSpace H] {U : ℝ → H ≃ₗᵢ[ℂ] H} (hU : IsOneParameterUnitaryGroup U) (hc : IsStronglyContinuous U) :
  HasDenseDomain (generator U)#check hasDenseDomain_generator

Physicslib4.Spectral.Stone.hasDenseDomain_generator.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
  [CompleteSpace H] {U : ℝ → H ≃ₗᵢ[ℂ] H} (hU : IsOneParameterUnitaryGroup U) (hc : IsStronglyContinuous U) :
  HasDenseDomain (generator U)

The two steps are average_mem_generator_domain (an average against a compactly supported C^1 weight is in the domain) and tendsto_average_bump (averages against shrinking bumps tend to \psi). Both assume strong continuity; the convolution formula average_eq_convolution needs only the group law.

4.3.5. Stone's theorem🔗

Blueprint: lmm:linear-ode-scalar, lmm:orbit-inner-ode, lmm:bounded-exp-solution-zero, lmm:generator-ker-adjoint-trivial, lmm:generator-essentially-self-adjoint, lmm:orbit-difference-hasDerivAt, lmm:norm-const-of-symmetric-derivative, lmm:orbits-agree-on-domain, lmm:agree-on-dense-subspace, thrm:hall-10.15.

open Physicslib4 Spectral Stone in
Physicslib4.Spectral.Stone.stone.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
  {U : ℝ → H ≃ₗᵢ[ℂ] H} (hU : IsOneParameterUnitaryGroup U) (hc : IsStronglyContinuous U) :
  ∃ (hA : IsSelfAdjoint (generator U)),
    HasDenseDomain (generator U) ∧
      (∀ (t : ℝ), U t = expUnitary hA t) ∧
        ∀ (B : H →ₗ.[ℂ] H) (hB : IsSelfAdjoint B), (∀ (t : ℝ), U t = expUnitary hB t) → B = generator U#check stone

Physicslib4.Spectral.Stone.stone.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
  {U : ℝ → H ≃ₗᵢ[ℂ] H} (hU : IsOneParameterUnitaryGroup U) (hc : IsStronglyContinuous U) :
  ∃ (hA : IsSelfAdjoint (generator U)),
    HasDenseDomain (generator U) ∧
      (∀ (t : ℝ), U t = expUnitary hA t) ∧
        ∀ (B : H →ₗ.[ℂ] H) (hB : IsSelfAdjoint B), (∀ (t : ℝ), U t = expUnitary hB t) → B = generator U

The generator is self-adjoint and densely defined, U(t) = e^{itA} for every t, and every self-adjoint B with U(t) = e^{itB} is the generator. The steps of the proof are ker_adjoint_generator_subSmul_eq_bot (trivial deficiency subspaces), isEssentiallySelfAdjoint_generator and orbit_eq_expUnitary_closure (the orbits of U and e^{itA^{(\mathrm{cl})}} agree on \mathrm{Dom}(A)).

The self-adjointness proof hA is the first component of the existential, and the other conjuncts mention it. A proof that uses the theorem takes the components apart with obtain:

open Physicslib4 Spectral Stone in
example {H : Type*} [NormedAddCommGroup H]
    [InnerProductSpace ℂ H] [CompleteSpace H]
    {U : ℝ → (H ≃ₗᵢ[ℂ] H)}
    (hU : IsOneParameterUnitaryGroup U)
    (hc : IsStronglyContinuous U) (t : ℝ) :
    ∃ hA : IsSelfAdjoint (generator U),
      U t = expUnitary hA t := byH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HU:ℝ → H ≃ₗᵢ[ℂ] HhU:IsOneParameterUnitaryGroup Uhc:IsStronglyContinuous Ut:ℝ⊢ ∃ (hA : IsSelfAdjoint (generator U)), U t = expUnitary hA t
  obtain ⟨hA, -, hexp, -⟩ := stone hU hcH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace HU:ℝ → H ≃ₗᵢ[ℂ] HhU:IsOneParameterUnitaryGroup Uhc:IsStronglyContinuous Ut:ℝhA:IsSelfAdjoint (generator U)hexp:∀ (t : ℝ), U t = expUnitary hA t⊢ ∃ (hA : IsSelfAdjoint (generator U)), U t = expUnitary hA t
  exact ⟨hA, hexp t⟩All goals completed! 🐙

4.3.6. Positive energy🔗

Blueprint: def:positive-energy, lmm:positive-energy-const, lmm:exp-generator-unique, lmm:positive-conj, lmm:positive-energy-conj, lmm:positive-energy-strong-continuous, lmm:positive-energy-exp-bounded, thrm:positive-energy-iff-exp, thrm:positive-energy-api.

structure

Physicslib4.AQFT.IsPositiveEnergy.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] (V : ℝ → H ≃ₗᵢ[ℂ] H) :
  Prop
Physicslib4.AQFT.IsPositiveEnergy.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  (V : ℝ → H ≃ₗᵢ[ℂ] H) : Prop

A one-parameter unitary group has positive energy when it is strongly continuous and its generator is a positive operator.

For a family V(t), t ∈ ℝ, of unitaries on H this asks three things: V(0) = 𝟙 and V(s + t) = V(s)V(t); t ↦ V(t)ψ is continuous for every ψ; and the infinitesimal generator A is positive. Here Aψ is the limit of (V(t)ψ − ψ)/(it) as t → 0, defined on the vectors ψ for which the limit exists, and positive means symmetric with ⟨ψ, Aψ⟩ ≥ 0 for every ψ in Dom(A). The generator is in general unbounded, and the condition is imposed on it directly. By Stone's theorem A is then densely defined and self-adjoint and V(t) = e^(itA), so positive energy says exactly that V(t) = e^(itA) with A positive and self-adjoint (isPositiveEnergy_iff_exists_exp). For the unitaries of time translations, U(t) = e^(itĤ) in the convention U(a) = e^(−iP·a), where P·a = −P⁰a⁰ + P⃗·a⃗ uses the signature (−,+,+,+) and P⁰ = Ĥ (the inverse of the Schrödinger evolution e^(−itĤ)). Then A is the Hamiltonian Ĥ, and the condition says that the energy is bounded below by 0.

This is the form in which the library states the spectrum condition. A vacuum state (HaagKastlerNet.IsVacuumState) asks that t ↦ U(γ(t)) have positive energy for every future-timelike translation subgroup γ, and a ground state for a flow (HaagKastlerNet.IsGroundStateForFlow, for a flow of Poincaré transformations in Minkowski spacetime or of isometries in curved spacetime) asks it of the unitary group implementing the flow. The definition refers to no spacetime.

Implementation note: unitaries are H ≃ₗᵢ[ℂ] H, and the generator is generator V, an H →ₗ.[ℂ] H; positivity is Spectral.Unbounded.IsPositive, stated as 0 ≤ Re⟨ψ, Aψ⟩. The three conditions are the three fields, so each is available by projection.

Blueprint: def:positive-energy

Constructor

Physicslib4.AQFT.IsPositiveEnergy.mk.{u_1}

Fields

isOneParameterUnitaryGroup : IsOneParameterUnitaryGroup V

V is a one-parameter unitary group.

isStronglyContinuous : IsStronglyContinuous V

V is strongly continuous.

isPositive_generator : IsPositive (generator V)

The infinitesimal generator of V is a positive operator.

The exponential form:

open Physicslib4 AQFT in
Physicslib4.AQFT.isPositiveEnergy_iff_exists_exp.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
  [CompleteSpace H] {V : ℝ → H ≃ₗᵢ[ℂ] H} :
  IsPositiveEnergy V ↔ ∃ A, ∃ (hA : IsSelfAdjoint A), IsPositive A ∧ ∀ (t : ℝ), V t = expUnitary hA t#check isPositiveEnergy_iff_exists_exp

Physicslib4.AQFT.isPositiveEnergy_iff_exists_exp.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
  [CompleteSpace H] {V : ℝ → H ≃ₗᵢ[ℂ] H} :
  IsPositiveEnergy V ↔ ∃ A, ∃ (hA : IsSelfAdjoint A), IsPositive A ∧ ∀ (t : ℝ), V t = expUnitary hA t

The operator A is unique (generator_eq_of_eq_expUnitary). The trivial group has positive energy (isPositiveEnergy_const_refl), so does \exp(itP) for a bounded positive P (isPositiveEnergy_exp), and positive energy is preserved by unitary conjugation (IsPositiveEnergy.conj, with IsPositive.of_conj). IsPositiveEnergy.strongContinuous unpacks strong continuity. The blueprint collects these six results in thrm:positive-energy-api.

4.3.7. Weak continuity🔗

Blueprint: lmm:weak-continuity-implies-strong.

open Physicslib4 in
Physicslib4.strongContinuous_of_weak.{u_1, u_2} {X : Type u_1} [TopologicalSpace X] {H : Type u_2}
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : X → H ≃ₗᵢ[ℂ] H) {D : Set H} (hD : Dense D)
  (hweak : ∀ ξ ∈ D, ∀ η ∈ D, Continuous fun x => inner ℂ ξ ((U x) η)) (ψ : H) : Continuous fun x => (U x) ψ#check strongContinuous_of_weak

Physicslib4.strongContinuous_of_weak.{u_1, u_2} {X : Type u_1} [TopologicalSpace X] {H : Type u_2}
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : X → H ≃ₗᵢ[ℂ] H) {D : Set H} (hD : Dense D)
  (hweak : ∀ ξ ∈ D, ∀ η ∈ D, Continuous fun x => inner ℂ ξ ((U x) η)) (ψ : H) : Continuous fun x => (U x) ψ

inner ℂ ξ ((U x) η) is \langle \xi, U(x)\eta \rangle. The GNS theorems that use it are exists_gns_unitary_of_invariant_strongContinuous and exists_gns_unitaryRep_of_invariant_strongContinuous.

4.4. Where to look🔗

Section 10.4 is formalised in Physicslib4/Spectral/Stone/, in five files, by topic. Each entry links to the API documentation of a representative declaration, from which the rest of the file can be browsed.

Basic.lean: one-parameter unitary groups, strong continuity, the generator and its domain, the symmetry identity, orbits, the trivial group and conjugation, and the equation y' = cy (eq_mul_exp_of_hasDerivAt), generator.
Bounded.lean: the exponential series of a bounded self-adjoint operator and its generator, generator_eq_of_eq_exp.
Exponential.lean: the unitary group e^{itA} of a self-adjoint operator and its generator, generator_expUnitary.
Density.lean: averages of orbits and the density of the generator's domain, hasDenseDomain_generator.
Theorem.lean: essential self-adjointness of the generator and Stone's theorem, stone.

Two files outside the directory hold the results of Section 10.6 described here:

Physicslib4/AQFT/PositiveEnergy.lean: the positive-energy condition, isPositiveEnergy_iff_exists_exp.
Physicslib4/Analysis/StrongContinuity.lean: weak continuity implies strong continuity, strongContinuous_of_weak.

The unbounded operators, the spectral measure and the functional calculus these files use are described in the unbounded chapter. The blueprint section is Section 10.4, and each entry there links to the Lean declarations that formalise it.