This chapter describes how the library encodes unbounded operators on a complex Hilbert space and
proves the spectral theorem for unbounded self-adjoint operators. It corresponds to
Section 10.3
of the blueprint, which, like Section 10.2, follows Hall's
Quantum Theory for Mathematicians. It builds on the
bounded spectral theory chapter: projection-valued measures, the bounded
operator-valued integral and bounded quadratic forms are taken from there. Stone's theorem, in
Section 10.4 of the blueprint, builds on this one.
3.1. Overview🔗
As you will recall, the position operator (X\psi)(x) = x\,\psi(x) and the momentum operator
P = -i\,d/dx on L^2(\mathbb{R}) are not bounded, and cannot be defined on every
square-integrable wave function: x\,\psi(x) need not be square-integrable, and \psi need not be
differentiable. By the Hellinger–Toeplitz theorem, a symmetric operator defined on all of a Hilbert
space is bounded, so any observable with unbounded spectrum, such as most Hamiltonians, has to live on a
dense subspace, its domain. The domain is part of the operator: -i\,d/dx on smooth compactly
supported functions and on the Sobolev space H^1(\mathbb{R}) are different operators, and only the
second is self-adjoint. The spectral theorem holds for self-adjoint operators, and the physicist's
"Hermitian" (symmetric) is not enough.
The spectral theorem for an unbounded self-adjoint operator A says what the bounded one does,
with the domain made explicit: there is exactly one projection-valued measure \mu^A on the Borel
sets of \mathbb{R} with
A = \int_{\mathbb{R}} \lambda \, d\mu^A(\lambda), \qquad
\mathrm{Dom}(A) = \Big\{\psi : \int_{\mathbb{R}} \lambda^2 \, d\mu^A_\psi(\lambda) < \infty\Big\},
where \mu^A_\psi(E) = \langle \psi, \mu^A(E)\psi \rangle. For a measurable f, f(A) is
\int f \, d\mu^A, defined on the \psi with \int |f|^2 \, d\mu^A_\psi < \infty; the time
evolution e^{-it\hat H} generated by a Hamiltonian \hat H is a bounded case of this.
The section is formalised in five stages, as in the blueprint:
-
Unbounded operators. An operator is a linear map on a subspace, its domain. The section treats
dense domains, adjoints, symmetric, self-adjoint and essentially self-adjoint operators, closed and
closable operators and closures, kernels and ranges, and the resolvent set and spectrum. It proves
that \mathrm{Range}(T)^\perp = \mathrm{Ker}(T^*), that the spectrum of a self-adjoint operator
is real, that an essentially self-adjoint operator has exactly one self-adjoint extension, and the
criterion: a densely defined symmetric T is essentially self-adjoint exactly when
T - i\mathbf{1} and T + i\mathbf{1} have dense ranges. An operator that acts by bounded
self-adjoint operators on the summands of a direct sum is essentially self-adjoint.
-
Integration against a projection-valued measure. For a measurable, possibly unbounded,
f and a projection-valued measure \mu, \int f \, d\mu is an unbounded operator with domain
W_f = \{\psi : \int |f|^2 \, d\mu_\psi < \infty\}. The domain is dense, the operator is
characterised by \langle \psi, (\int f \, d\mu)\psi \rangle = \int f \, d\mu_\psi, it agrees
with the bounded integral for bounded f, and it is self-adjoint for real f.
-
Bounded normal operators. For a bounded normal A the section proves the two-variable
spectral mapping theorem \sigma(p(A, A^*)) = \{p(\lambda, \bar\lambda) : \lambda \in \sigma(A)\}
for polynomials p, and the continuous functional calculus on C(\sigma(A), \mathbb{C}),
characterised as the unique bounded linear map extending p \mapsto p(A, A^*).
-
The abstract functional calculus. Any isometric *-homomorphism
\Phi : C(X, \mathbb{C}) \to \mathcal{B}(H) on a compact metric space X, sending 1 to
\mathbf{1}, comes from a projection-valued measure on X. Applied to the calculus of a
normal operator, this gives the spectral theorem for bounded normal operators.
-
The Cayley transform. A self-adjoint A has a unitary Cayley transform
U = (A + i\mathbf{1})(A - i\mathbf{1})^{-1}. The spectral measure of U, carried from the unit
circle to \mathbb{R} by the inverse of the Cayley map x \mapsto (x + i)/(x - i), integrates
the identity function to A, and it is the only projection-valued measure on \mathbb{R} that
does. This is the spectral theorem for unbounded self-adjoint operators; the functional calculus
f(A) follows.
Every statement of the section is proved in Lean, with no sorry. The standard results the
blueprint states without proof, such as the monotone and dominated convergence theorems and the
basic facts about L^2 and \ell^2, are Mathlib theorems. The spectral theorem is proved for
unbounded self-adjoint and for bounded normal operators; the spectral theorem for unbounded normal
operators is not stated in the blueprint or proved in the library. The declarations are in the
namespace Physicslib4.Spectral.Unbounded, written without the prefix below.
3.2. Design🔗
The conventions inherited from Mathlib, among them the adjoint of a partial map and the guarded
integral, are collected in the conventions chapter under
Implementation choices.
Where the library departs from the blueprint's route, this section says so, and links the
blueprint's formalization note where it has one. The conventions of the
bounded chapter carry over unchanged: bounded operators are
H →L[ℂ] H, no result on the way to the spectral theorem assumes H separable (only
completeSpace_and_separableSpace_of_isClosed,
the blueprint's lemma on closed subspaces, does), and bounded operators are obtained from bounded
quadratic forms.
3.2.1. Unbounded operators are Mathlib's partial linear maps🔗
An unbounded operator is an element of H →ₗ.[ℂ] H, Mathlib's LinearPMap: a submodule
T.domain of H together with a linear map from it to H; T is applied to elements of the
subtype T.domain. Two partial maps are equal only if their domains are, so every equation
between unbounded operators in the library, such as T^* = T, includes the equality of
domains. Mathlib supplies the order S ≤ T ("T extends S"), the sum S + T on the
intersection of the domains, the graph, closedness (LinearPMap.IsClosed), closability and the
closure (LinearPMap.IsClosable, LinearPMap.closure). The graph lies in the plain product
H × H: every use of it in the section is topological, so the inner product of the blueprint's
product Hilbert space is not needed (the remark on the Lean formalization in
def:product-hilbert-space).
A bounded operator B becomes a partial map with domain all of H as
(B : H →ₗ[ℂ] H).toPMap ⊤.
Density of the domain is not part of the type. It is the predicate HasDenseDomain T, carried as a
hypothesis wherever the blueprint needs it. Symmetry (IsSymmetric) assumes no density, so it
applies to extensions not yet known to be densely defined (the blueprint records this in the proof
of
lmm:self-adjoint-maximally-symmetric).
3.2.2. The adjoint is Mathlib's, with its convention🔗
The adjoint is Mathlib's LinearPMap.adjoint, written T†. Its domain is
LinearPMap.adjointDomain, the vectors \varphi for which \psi \mapsto \langle \varphi, T\psi \rangle
is continuous on the domain of T, which is the blueprint's boundedness condition. Mathlib defines
T† for every T: when the domain of T is not dense, T† keeps this domain but is the zero map
on it. The blueprint's adjoint exists only for densely defined operators, so every theorem about
the action of T† assumes HasDenseDomain T.
Self-adjointness is Mathlib's IsSelfAdjoint for the star operation T \mapsto T^* on
H →ₗ.[ℂ] H, so IsSelfAdjoint T means T† = T, domains included. It implies a dense domain
(IsSelfAdjoint.dense_domain), which is why theorems about self-adjoint operators, such as the
spectral theorem, carry no separate density hypothesis.
3.2.3. The resolvent is a predicate🔗
For a bounded operator, \lambda is in the resolvent set when A - \lambda\mathbf{1} is a unit
of the algebra H →L[ℂ] H. Partial maps form no ring, so the library spells out the bounded
inverse of T - \lambda\mathbf{1} as the predicate IsResolvent T lam B on a bounded B. The resolvent set and the
spectrum are pmapResolventSet T and pmapSpectrum T; the prefix keeps them apart from Mathlib's
resolventSet and spectrum, with which they agree on bounded operators
(pmapSpectrum_toPMap_top). The operator T - \lambda\mathbf{1} is subSmul T lam (λ is a
Lean keyword). The sign is the blueprint's: B is (T - \lambda\mathbf{1})^{-1}, the negative of
Mathlib's resolvent.
3.2.4. The integral of an unbounded function🔗
For a measurable f that may be unbounded, the library follows the blueprint
(prpstn:hall-10.2):
-
The domain W_f is integralDomain μ f, the \psi with MemLp f 2 (μ.assoc ψ), Mathlib's
"square-integrable for \mu_\psi".
-
On W_f, Q_f(\psi) = \int f \, d\mu_\psi is a quadratic form on a subspace
(integralForm, IsQuadraticFormOn).
-
(\int f \, d\mu)\psi is the unique \chi with L_f(\varphi, \psi) = \langle \varphi, \chi \rangle
for all \varphi in the dense subspace W_f, where L_f is the polarization of Q_f.
The action, integralApply μ f, is chosen from this existence-and-uniqueness statement and is
guarded: it is 0 when f is not measurable or no unique \chi exists. The guard makes
pmapIntegral μ f a partial linear map for every f, linear without a hypothesis, and so every
theorem about its values assumes Measurable f, as theorems about the bounded integral assume
f ∈ BddMeasurable X.
The blueprint proves that \int f \, d\mu is self-adjoint for real f
(prpstn:hall-10.3)
by decomposing H into the spectral subspaces where n - 1 \le |f| < n, on which the operator is
bounded, and applying its result on direct sums. The Lean proof avoids direct sums:
\int f \, d\mu is symmetric, and for non-real c the bounded integral of (f - c)^{-1} is
a right inverse of \int f \, d\mu - c\mathbf{1}, so the latter maps onto H; a symmetric
operator with this property is self-adjoint (formalization note of prpstn:hall-10.3). The
direct-sum results, isEssentiallySelfAdjoint_of_isDirectSumOperator and its internal form, are formalised in their
own right; no proof outside their file uses them. The external direct sum is Mathlib's lp G 2.
3.2.5. Normal operators and the abstract calculus🔗
The Cayley transform of a self-adjoint operator is unitary, hence normal, but in general not self-adjoint, so the
route to the unbounded theorem needs the spectral theorem for bounded normal operators. Normality
is Mathlib's IsStarNormal, and the continuous functional calculus normalCalculus is Mathlib's
cfcHom, as realCalculus is in the bounded case; the library adds the blueprint's
characterisation by polynomials in A and A^*. It proves the two-variable spectral mapping
theorem from Mathlib's spectral mapping theorem for the continuous functional calculus, not by
the blueprint's almost-eigenvector argument (formalization note of
thrm:hall-10.23);
the almost-eigenvector lemmas are formalised separately.
The passage from a continuous calculus to a projection-valued measure is done once, abstractly, as
in the blueprint. IsAbstractCalculus Φ lists the five properties of a map
\Phi : C(X, \mathbb{C}) \to \mathcal{B}(H) on a compact metric space X. The measures
\mu_\psi come from Mathlib's Riesz–Markov–Kakutani theorem, the extended calculus
\tilde\Phi(f) for bounded measurable f from bounded quadratic forms, and the
projection-valued measure abstractPVM sends E to \tilde\Phi(1_E). The spectral theorem for
a bounded normal operator is abstractPVM of normalCalculus. The bounded self-adjoint theorem of
Section 10.2 is proved there by its own route and is not rederived from abstractPVM.
The library proves the unbounded spectral theorem as the blueprint does, through the Cayley
transform, which turns the unbounded problem into a bounded one. For self-adjoint A,
exists_isCayleyTransform gives a unitary U with U - \mathbf{1} injective with range
\mathrm{Dom}(A), and A = i(U + \mathbf{1})(U - \mathbf{1})^{-1} on \mathrm{Dom}(A). The spectral
measure \mu^U lives on \sigma(U), inside the unit circle, and gives no mass to the point
1. With D(u) = i(u + 1)/(u - 1) the inverse of the Cayley map,
A = \int D \, d\mu^U, and \mu^A(E) = \mu^U(D^{-1}(E)) is a projection-valued measure on
\mathbb{R} with A = \int \lambda \, d\mu^A.
Three choices differ from the blueprint's text; the blueprint records only the second:
-
cayleyPVM composes with D directly. The blueprint restricts \mu^U to the
circle without 1 and transports it along the Cayley map; the two constructions it uses,
restrictPVM and mapPVM, are formalised but not used.
-
For uniqueness, a second measure \nu with A = \int \lambda \, d\nu is carried to the
circle along the Cayley map and compared there with \mu^U
(eq_of_integral_id_eq_ambient). The blueprint transports \nu along the
bijection onto the circle without 1; the library pushes it forward to the whole circle
(pushforwardPVM), which needs no bijectivity (formalization note after the proof
of thrm:hall-10.4).
-
The blueprint assumes H \neq \{0\}. Some intermediate lemmas carry Nontrivial H; the
spectral theorem treats H = \{0\} separately and has no such hypothesis.
The spectral measure lives on \mathbb{R}, as in the blueprint, not on the spectrum as in the
bounded case; that it is concentrated on \sigma(A) is a separate theorem.
3.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 unbounded operators, ↑ is a coercion (a vector of a domain regarded as a vector of
H, a partial map applied as a function, a real number regarded as complex), and
fun x => ↑x is the function \lambda on \mathbb{R}. For the declarations not shown here,
see the
API documentation
and the files listed at the end of the chapter.
3.3.1. Domains, adjoints and self-adjointness🔗
Blueprint: def:hall-3.1, def:hall-9.1, prpstn:adjoint-well-defined,
def:hall-9.2, def:hall-9.3, prpstn:hall-9.4, def:hall-9.5,
def:positive-unbounded-operator, def:hall-9.6, def:hall-9.7,
def:closed-linear-map-on-a-subspace, prpstn:hall-9.8,
prpstn:hall-9.10, prpstn:hall-9.11,
def:kernel-of-an-unbounded-operator, def:range-of-an-unbounded-operator,
prpstn:hall-9.12, prpstn:hall-9.13.
🔗def
The domain of a partially defined linear map T on H is dense: the condition that makes T an
unbounded operator.
Position, momentum and most Hamiltonians of quantum mechanics cannot be defined on every vector
of H, only on a subspace of it. An unbounded operator is therefore a pair: a subspace Dom(T) of
H, its domain, and a linear map T : Dom(T) → H, with Dom(T) dense in H. "Unbounded" means "not
necessarily bounded": a bounded operator defined on all of H is a special case. Density of
Dom(T) is what makes the adjoint T* well defined (existsUnique_adjoint_apply).
Implementation note: the pair (Dom(T), T) is Mathlib's LinearPMap, written H →ₗ.[ℂ] H, with
domain T.domain. Density is not part of the type: it is this predicate, carried as an explicit
hypothesis wherever the blueprint requires a dense domain. A self-adjoint operator has dense
domain automatically (Mathlib's IsSelfAdjoint.dense_domain).
Blueprint: def:hall-3.1
🔗def
An operator T is symmetric if ⟨φ, Tψ⟩ = ⟨Tφ, ψ⟩ for all φ and ψ in its domain.
This is the condition physicists usually call "Hermitian": it makes every expectation value
⟨ψ, Tψ⟩ real. For an unbounded operator it is weaker than self-adjointness. A densely defined T
is symmetric exactly when T* extends T (isSymmetric_iff_le_adjoint), while self-adjointness
asks T* = T, including equal domains. The reality of the spectrum (pmapSpectrum_subset_real)
and the spectral theorem need self-adjointness, so the gap between the two notions matters.
Implementation note: no density of T.domain is assumed; the blueprint's operators have dense
domain, supplied separately by HasDenseDomain. The predicate is Mathlib's
LinearPMap.IsFormalAdjoint of T with itself, with the sides of the equation swapped
(isSymmetric_iff_isFormalAdjoint). Self-adjointness is Mathlib's IsSelfAdjoint for the star
operation T ↦ T† on H →ₗ.[ℂ] H, so it means T† = T (LinearPMap.isSelfAdjoint_def).
Blueprint: def:hall-9.2
🔗def
An operator A is positive if it is symmetric and ⟨ψ, Aψ⟩ ≥ 0 for every ψ in its domain.
For a symmetric A the expectation value ⟨ψ, Aψ⟩ is real, so the condition says that every
expectation value is non-negative. This is the notion in which the positive-energy condition of
the Haag–Kastler axioms is phrased: a one-parameter unitary group has positive energy when its
generator is positive (Physicslib4.AQFT.IsPositiveEnergy). For a bounded operator on all of H
it agrees with the usual positivity (isPositive_toPMap_iff).
Implementation note: the condition is stated as 0 ≤ Re⟨ψ, Aψ⟩, the form of Mathlib's
ContinuousLinearMap.IsPositive. Symmetry is meant in the density-free sense of IsSymmetric.
Blueprint: def:positive-unbounded-operator
🔗structure
An operator T is essentially self-adjoint if it is symmetric and closable, and its closure is
self-adjoint.
In practice an observable is often first written down on a convenient small domain, for example
the momentum operator −i d/dx on smooth compactly supported wave functions. There it is
symmetric but not self-adjoint. Essential self-adjointness says that the domain is nevertheless
big enough: the closure T^(cl) is self-adjoint, and it is the only self-adjoint extension of T
(existsUnique_isSelfAdjoint_extension). A densely defined symmetric T is essentially
self-adjoint exactly when T − i𝟙 and T + i𝟙 have dense ranges
(isEssentiallySelfAdjoint_iff_dense_range).
Implementation note: the closure is Mathlib's LinearPMap.closure, and self-adjointness is
T.closure† = T.closure. The three conditions are kept as separate fields, as in the blueprint,
although closability follows from symmetry for densely defined T (isClosable_of_isSymmetric).
Blueprint: def:hall-9.7
Fields
isSymmetric : IsSymmetric T
T is symmetric: ⟨φ, Tψ⟩ = ⟨Tφ, ψ⟩ on Dom(T).
isClosable : T.IsClosable
T is closable: the closure of its graph in H × H is the graph of an operator.
isSelfAdjoint_closure : IsSelfAdjoint T.closure
The closure T^(cl) of T is self-adjoint.
An essentially self-adjoint operator has exactly one self-adjoint extension, its closure
(eq_closure_of_isSelfAdjoint_of_le):
open Physicslib4 Spectral Unbounded in
Physicslib4.Spectral.Unbounded.existsUnique_isSelfAdjoint_extension.{u_1} {H : Type u_1} [NormedAddCommGroup H]
[InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (h : IsEssentiallySelfAdjoint T) :
∃! B, IsSelfAdjoint B ∧ T ≤ B#check existsUnique_isSelfAdjoint_extension
Physicslib4.Spectral.Unbounded.existsUnique_isSelfAdjoint_extension.{u_1} {H : Type u_1} [NormedAddCommGroup H]
[InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (h : IsEssentiallySelfAdjoint T) :
∃! B, IsSelfAdjoint B ∧ T ≤ B
Here B ranges over H →ₗ.[ℂ] H, and T ≤ B says that B extends T. The adjoint is well
defined (existsUnique_adjoint_apply);
a densely defined T is symmetric exactly when T \le T^*
(isSymmetric_iff_le_adjoint),
and then closable
(isClosable_of_isSymmetric),
with (T^{\mathrm{cl}})^* = T^*
(adjoint_closure_eq_adjoint).
The sequential description of closedness is
isClosed_iff_forall_tendsto,
and \mathrm{Range}(T)^\perp = \mathrm{Ker}(T^*) is
orthogonal_range_eq_ker_adjoint,
with the kernel and range of a partial map defined as subspaces of H
(ker, range).
A self-adjoint operator plus a bounded self-adjoint one is self-adjoint on the same domain
(isSelfAdjoint_add_of_isSelfAdjoint).
3.3.2. The spectrum and essential self-adjointness🔗
Blueprint: def:hall-9.16, lmm:uniqueness-of-resolvent,
lmm:spectrum-notions-agree, thrm:hall-9.17, thrm:hall-9.21.
🔗def
The operator T − λ𝟙 for a complex number λ, with domain Dom(T) and action ψ ↦ Tψ − λψ.
Since λ𝟙 is defined on all of H, the difference is defined exactly where T is. The resolvent
set and spectrum of T are defined through the invertibility of T − λ𝟙 (IsResolvent), and
the ranges of T − i𝟙 and T + i𝟙 decide essential self-adjointness.
Implementation note: T + i𝟙 is subSmul T (-Complex.I). The parameter is named lam because
λ is reserved in Lean. Domain and action are subSmul_domain and subSmul_apply, both by
definition.
Blueprint: def:hall-3.1
🔗structure
A bounded operator B is a two-sided inverse of T − λ𝟙: it maps H into Dom(T), and
(T − λ𝟙)B = 𝟙 on H and B(T − λ𝟙) = 𝟙 on Dom(T).
For a bounded operator, λ is in the resolvent set when T − λ𝟙 has a bounded inverse. For an
unbounded T the operator T − λ𝟙 is defined only on Dom(T), so "bounded inverse" has to be
spelled out: B is defined and bounded on all of H, takes its values in Dom(T), and undoes
T − λ𝟙 from both sides. Such a B is unique when it exists (existsUnique_isResolvent) and is
written (T − λ𝟙)⁻¹. For a self-adjoint T and non-real λ it exists
(mem_pmapResolventSet_of_im_ne_zero, whose proof bounds its norm by 1/|Im λ|).
Implementation note: the inverse is a predicate on a candidate B rather than an inverse in a
ring, because Mathlib gives the partial maps H →ₗ.[ℂ] H no ring structure. The sign follows
the blueprint, B = (T − λ𝟙)⁻¹; Mathlib's resolvent for bounded operators inverts λ𝟙 − A
instead, the negative, which is why pmapResolventSet_toPMap_top passes through −B.
Blueprint: def:hall-9.16
Fields
mem_domain : ∀ (ψ : H), B ψ ∈ T.domain
B maps every vector of H into Dom(T).
rightInverse : ∀ (ψ : H), ↑T ⟨B ψ, ⋯⟩ - lam • B ψ = ψ
B is a right inverse: (T − λ𝟙)Bψ = ψ for every ψ in H.
leftInverse : ∀ (ψ : ↥T.domain), B (↑T ψ - lam • ↑ψ) = ↑ψ
B is a left inverse on the domain: B(T − λ𝟙)ψ = ψ for every ψ in Dom(T).
🔗def
The spectrum σ(T) of an operator T: the complex numbers λ for which T − λ𝟙 has no bounded
inverse defined on all of H.
For a self-adjoint observable, σ(T) is the set of values a measurement can return. Besides
eigenvalues it can contain continuous spectrum, such as all of ℝ for the momentum operator on
L²(ℝ): there T − λ𝟙 is injective, but its inverse is not bounded and defined on all of H.
The spectrum of a self-adjoint operator is real (pmapSpectrum_subset_real), and for a bounded
operator on all of H it is the usual spectrum (pmapSpectrum_toPMap_top).
Implementation note: the complement of pmapResolventSet; the prefix pmap separates it from
Mathlib's spectrum.
Blueprint: def:hall-9.16
The spectrum of a self-adjoint operator is real:
open Physicslib4 Spectral Unbounded in
Physicslib4.Spectral.Unbounded.pmapSpectrum_subset_real.{u_1} {H : Type u_1} [NormedAddCommGroup H]
[InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hsa : IsSelfAdjoint T) : pmapSpectrum T ⊆ {z | z.im = 0}#check pmapSpectrum_subset_real
Physicslib4.Spectral.Unbounded.pmapSpectrum_subset_real.{u_1} {H : Type u_1} [NormedAddCommGroup H]
[InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hsa : IsSelfAdjoint T) : pmapSpectrum T ⊆ {z | z.im = 0}
The inverse of T - \lambda\mathbf{1} is unique
(existsUnique_isResolvent),
the two notions of spectrum agree on bounded operators
(pmapSpectrum_toPMap_top),
and non-real \lambda are in the resolvent set of a self-adjoint operator
(mem_pmapResolventSet_of_im_ne_zero).
The criterion for essential self-adjointness, with subSmul T Complex.I the operator
T - i\mathbf{1} and subSmul T (-Complex.I) the operator T + i\mathbf{1}:
open Physicslib4 Spectral Unbounded in
Physicslib4.Spectral.Unbounded.isEssentiallySelfAdjoint_iff_dense_range.{u_1} {H : Type u_1} [NormedAddCommGroup H]
[InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hT : HasDenseDomain T) (hsym : IsSymmetric T) :
IsEssentiallySelfAdjoint T ↔ Dense ↑(range (subSmul T Complex.I)) ∧ Dense ↑(range (subSmul T (-Complex.I)))#check isEssentiallySelfAdjoint_iff_dense_range
Physicslib4.Spectral.Unbounded.isEssentiallySelfAdjoint_iff_dense_range.{u_1} {H : Type u_1} [NormedAddCommGroup H]
[InnerProductSpace ℂ H] [CompleteSpace H] {T : H →ₗ.[ℂ] H} (hT : HasDenseDomain T) (hsym : IsSymmetric T) :
IsEssentiallySelfAdjoint T ↔ Dense ↑(range (subSmul T Complex.I)) ∧ Dense ↑(range (subSmul T (-Complex.I)))
3.3.3. Direct sums🔗
Blueprint: lmm:finite-direct-sum-dense, def:internal-orthogonal-decomposition,
lmm:internal-decomposition-unitary, prpstn:hall-9.26,
prpstn:hall-9.26-internal.
🔗structure
An operator T on an external direct sum acts componentwise by a family of bounded operators
Aᵢ: T is symmetric, its domain contains every vector with finitely many nonzero components,
and on such vectors (Tψ)ᵢ = Aᵢψᵢ.
This fixes T only on the finite direct sum, a dense subspace; T may be defined on more. When
every Aᵢ is self-adjoint, T is essentially self-adjoint, and its closure and its adjoint are the
same operator ψ ↦ (Aᵢψᵢ) on the domain V of directSumDomain
(isEssentiallySelfAdjoint_of_isDirectSumOperator, closure_apply_eq_of_isDirectSumOperator,
adjoint_apply_eq_of_isDirectSumOperator). So the componentwise operator has exactly one
self-adjoint version, whichever dense domain it is first written on.
Implementation note: the structure is a predicate on a given partial linear map T on
lp G 2, rather than a construction of T, matching the blueprint's "suppose A is a symmetric
operator ...".
Blueprint: prpstn:hall-9.26
Fields
isSymmetric : IsSymmetric T
The operator T is symmetric.
memDomain : ∀ (f : ↥(lp G 2)), {i | ↑f i ≠ 0}.Finite → f ∈ T.domain
Every vector with finitely many nonzero components lies in the domain of T.
apply_eq : ∀ (f : ↥(lp G 2)) (hf : {i | ↑f i ≠ 0}.Finite) (i : ι), ↑(↑T ⟨f, ⋯⟩) i = (A i) (↑f i)
On a vector ψ with finitely many nonzero components, (Tψ)ᵢ = Aᵢψᵢ for every i.
The componentwise operator is essentially self-adjoint:
open Physicslib4 Spectral Unbounded in
Physicslib4.Spectral.Unbounded.isEssentiallySelfAdjoint_of_isDirectSumOperator.{u_2, u_3} {ι : Type u_2}
{G : ι → Type u_3} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace ℂ (G i)]
[∀ (i : ι), CompleteSpace (G i)] {A : (i : ι) → G i →L[ℂ] G i} {T : ↥(lp G 2) →ₗ.[ℂ] ↥(lp G 2)}
(hA : ∀ (i : ι), IsSelfAdjoint (A i)) (hT : IsDirectSumOperator A T) : IsEssentiallySelfAdjoint T#check isEssentiallySelfAdjoint_of_isDirectSumOperator
Physicslib4.Spectral.Unbounded.isEssentiallySelfAdjoint_of_isDirectSumOperator.{u_2, u_3} {ι : Type u_2}
{G : ι → Type u_3} [(i : ι) → NormedAddCommGroup (G i)] [(i : ι) → InnerProductSpace ℂ (G i)]
[∀ (i : ι), CompleteSpace (G i)] {A : (i : ι) → G i →L[ℂ] G i} {T : ↥(lp G 2) →ₗ.[ℂ] ↥(lp G 2)}
(hA : ∀ (i : ι), IsSelfAdjoint (A i)) (hT : IsDirectSumOperator A T) : IsEssentiallySelfAdjoint T
Its closure and its adjoint have the maximal domain
directSumDomain
(domain_closure_eq_directSumDomain).
The internal form, for an
IsInternalOrthogonalDecomposition
of H into closed subspaces, is
isEssentiallySelfAdjoint_of_isInternalDirectSumOperator;
such a decomposition makes H unitarily the external direct sum of its summands
(isHilbertSum_of_isInternalOrthogonalDecomposition,
in Mathlib's language of IsHilbertSum).
3.3.4. Integration against a projection-valued measure🔗
Blueprint: def:hall-quadratic-form-on-a-subspace, prpstn:hall-10.2,
prpstn:hall-10.1, prpstn:coincidence-with-the-bounded-integral,
lmm:truncations-converge, prpstn:hall-10.3.
🔗def
The domain W_f = {ψ ∈ H : ∫ |f|² dμ_ψ < ∞} of the integral of a function f against a
projection-valued measure μ.
Here μ_ψ(E) = ⟨ψ, μ(E)ψ⟩ is the measure of ψ, a probability distribution when ‖ψ‖ = 1. If μ is
the spectral measure of an observable A, the integral of f plays the role of f(A), and W_f is
the set of ψ on which it is defined; there ‖(∫ f dμ)ψ‖² = ∫ |f|² dμ_ψ (norm_sq_pmapIntegral).
For f(λ) = λ the condition says that the distribution of measured values of A in the state ψ
has a finite second moment ∫ λ² dμ_ψ. For bounded measurable f, W_f = H
(integralDomain_eq_top_of_bddMeasurable); for measurable f, W_f is dense
(dense_integralDomain).
Implementation note: membership is Mathlib's MemLp f 2 (μ.assoc ψ) (mem_integralDomain),
which also asks f to be almost everywhere strongly measurable for μ_ψ; for measurable f this
holds automatically and the condition is ∫ |f|² dμ_ψ < ∞. The domain is a submodule because
μ_(φ+ψ) ≤ 2(μ_φ + μ_ψ) (assoc_add_le) and μ_(cψ) = |c|²μ_ψ (assoc_smul).
Blueprint: prpstn:hall-10.2
🔗def
The action ψ ↦ (∫ f dμ)ψ of the integral on W_f: the unique vector χ with
L_f(φ, ψ) = ⟨φ, χ⟩ for every φ in W_f.
Here L_f is the polarization of Q_f, so χ is fixed by its matrix elements against the dense
subspace W_f. For measurable f such a χ exists and is unique (existsUnique_repr_integralForm):
it is the limit of the bounded integrals of the truncations f·1_(|f| < n)
(tendsto_integral_truncation).
Implementation note: the value is 0 when f is not measurable or no unique χ exists. The
measurability guard makes pmapIntegral linear by a direct argument, without a hypothesis;
every result about the values of pmapIntegral assumes f measurable.
Blueprint: prpstn:hall-10.1
🔗def
The integral ∫ f dμ of a possibly unbounded function f against a projection-valued measure μ,
as an unbounded operator with domain W_f.
The unbounded spectral theorem writes a self-adjoint A as A = ∫ λ dμ(λ) for a unique μ
(existsUnique_spectralMeasure_unbounded), and the functional calculus f(A) is ∫ f dμ for that
μ (functionalCalculus). For measurable f the integral is characterised by
⟨ψ, (∫ f dμ)ψ⟩ = ∫ f dμ_ψ on W_f (inner_self_pmapIntegral), and any operator with domain W_f
satisfying this identity equals it (eq_pmapIntegral_of_inner_self). It obeys
‖(∫ f dμ)ψ‖² = ∫ |f|² dμ_ψ (norm_sq_pmapIntegral), agrees with the bounded integral
ProjectionValuedMeasure.integral for bounded measurable f (pmapIntegral_of_bddMeasurable),
and is self-adjoint for real-valued measurable f (isSelfAdjoint_pmapIntegral_of_real).
Implementation note: a LinearPMap with domain integralDomain μ f and action
integralApply μ f, which is 0 for non-measurable f.
Blueprint: prpstn:hall-10.1
The integral is determined by its expectation values: an operator with domain W_f and
\langle \psi, A\psi \rangle = \int f \, d\mu_\psi is \int f \, d\mu
(eq_pmapIntegral_of_inner_self).
For bounded measurable f it is the bounded integral, defined on all of H:
open Physicslib4 Spectral Unbounded in
Physicslib4.Spectral.Unbounded.pmapIntegral_of_bddMeasurable.{u_1, u_2} {X : Type u_1} [MeasurableSpace X]
{H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H)
{f : X → ℂ} (hf : f ∈ BddMeasurable X) : pmapIntegral μ f = (↑(μ.integral f)).toPMap ⊤#check pmapIntegral_of_bddMeasurable
Physicslib4.Spectral.Unbounded.pmapIntegral_of_bddMeasurable.{u_1, u_2} {X : Type u_1} [MeasurableSpace X]
{H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H)
{f : X → ℂ} (hf : f ∈ BddMeasurable X) : pmapIntegral μ f = (↑(μ.integral f)).toPMap ⊤
The headline result of the subsection, the self-adjointness of \int f \, d\mu for real f,
proved without direct sums (see Design):
open Physicslib4 Spectral Unbounded in
Physicslib4.Spectral.Unbounded.isSelfAdjoint_pmapIntegral_of_real.{u_1, u_2} {X : Type u_1} [MeasurableSpace X]
{H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H)
{f : X → ℂ} (hf : Measurable f) (hreal : ∀ (x : X), (f x).im = 0) : IsSelfAdjoint (pmapIntegral μ f)#check isSelfAdjoint_pmapIntegral_of_real
Physicslib4.Spectral.Unbounded.isSelfAdjoint_pmapIntegral_of_real.{u_1, u_2} {X : Type u_1} [MeasurableSpace X]
{H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure X H)
{f : X → ℂ} (hf : Measurable f) (hreal : ∀ (x : X), (f x).im = 0) : IsSelfAdjoint (pmapIntegral μ f)
The density of W_f is
dense_integralDomain, the
representation of the polarization of Q_f
existsUnique_repr_integralForm,
and the forms on a subspace are
IsQuadraticFormOn and
IsBoundedQuadraticFormOn.
The truncations f \cdot 1_{|f| < n} give (\int f \, d\mu)\psi as a limit of bounded integrals
(tendsto_integral_truncation).
3.3.5. Bounded normal operators🔗
Blueprint: def:hall-10.19, lmm:polynomials-in-normal-are-normal,
def:hall-7.14,
def:hall-10.24, lmm:hall-10.25 to lmm:hall-10.27,
thrm:hall-10.23, crllr:norm-of-polynomial-in-a-astar,
thrm:continuous-functional-calculus-normal.
🔗def
The operator p(A, A*) obtained by substituting a bounded operator A and its adjoint into a
polynomial in two variables.
A polynomial p(λ, λ̄) = Σ a(kl) λᵏ λ̄ˡ in a complex variable and its conjugate becomes the bounded
operator p(A, A*) = Σ a(kl) Aᵏ (A*)ˡ, with all powers of A written to the left of the powers of
A*. For a normal A (one that commutes with its adjoint) the ordering does not matter, and
p(A, A*) is again normal and commutes with A and A* (isStarNormal_mvApply,
commute_mvApply). These are the operators from which the continuous functional calculus of a
normal operator is built.
Implementation note: the polynomial is an MvPolynomial (Fin 2) ℂ, whose first variable
stands for λ and second for λ̄. The definition is the sum over the coefficients, so it needs no
commutativity of A and A* and makes sense for every bounded A; normality is used only in the
theorems about it.
Blueprint: lmm:polynomials-in-normal-are-normal
The two-variable spectral mapping theorem, with mvEvalConj p the function
\lambda \mapsto p(\lambda, \bar\lambda):
open Physicslib4 Spectral Unbounded in
Physicslib4.Spectral.Unbounded.spectrum_mvApply.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
[CompleteSpace H] {A : H →L[ℂ] H} [IsStarNormal A] (p : MvPolynomial (Fin 2) ℂ) :
spectrum ℂ (mvApply A p) = mvEvalConj p '' spectrum ℂ A#check spectrum_mvApply
Physicslib4.Spectral.Unbounded.spectrum_mvApply.{u_1} {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
[CompleteSpace H] {A : H →L[ℂ] H} [IsStarNormal A] (p : MvPolynomial (Fin 2) ℂ) :
spectrum ℂ (mvApply A p) = mvEvalConj p '' spectrum ℂ A
🔗def
The continuous functional calculus f ↦ f(A) of a bounded normal operator A, for continuous
complex functions f on the spectrum of A.
A bounded operator A is normal when it commutes with its adjoint, A A* = A* A; self-adjoint
and unitary operators are the main examples. For such A every continuous f on σ(A) defines a
bounded operator f(A). The map f ↦ f(A) is linear and multiplicative, sends f̄ to f(A)*, is
isometric (‖f(A)‖ = sup |f| on σ(A)), and sends 1 to 𝟙 and λ ↦ λ to A (normalCalculus_mul,
normalCalculus_star, norm_normalCalculus, normalCalculus_one_and_id). It is the unique
bounded linear map extending p ↦ p(A, A*) (existsUnique_normalCalculus).
Implementation note: the definition is Mathlib's continuous functional calculus cfcHom for
the predicate IsStarNormal, available because Mathlib makes H →L[ℂ] H a C*-algebra. It is a
star-algebra homomorphism, so linearity, multiplicativity and the adjoint property hold by
construction. Mathlib's construction replaces the blueprint's density argument through the
two-variable spectral mapping theorem; existsUnique_normalCalculus connects the two.
Blueprint: thrm:continuous-functional-calculus-normal
The characterisation is
existsUnique_normalCalculus,
and the norm of p(A, A^*) is
norm_mvApply. The almost eigenvectors of the
blueprint's own proof are
IsAlmostEigenvector, with
mem_spectrum_iff_forall_isAlmostEigenvector,
and the spectral subspaces
spectralSubspace.
3.3.6. The abstract functional calculus🔗
Blueprint: def:abstract-continuous-functional-calculus,
def:abstract-associated-measures, prpstn:abstract-extended-forms-are-bounded,
def:abstract-extended-calculus, thrm:abstract-calculus-yields-pvm,
thrm:hall-10.20.
🔗structure
A map Φ from continuous complex functions on a compact metric space X to bounded operators on
H is an abstract continuous functional calculus: it is linear and multiplicative, sends f̄ to
Φ(f)*, is isometric for the supremum norm, and sends the constant 1 to 𝟙.
These are the properties of f ↦ f(A) for a bounded normal operator A on X = σ(A)
(normalCalculus), with the operator itself forgotten. From such a Φ alone the file builds a
projection-valued measure on X whose integrals reproduce Φ (abstractPVM), so the passage from
a continuous functional calculus to a spectral measure is carried out once, in general. The
spectral theorem for bounded normal operators (existsUnique_spectralMeasure_normal) is its
special case Φ = normalCalculus.
Implementation note: the five properties are separate fields on an unbundled map rather than a
bundled star-algebra homomorphism, as in the blueprint. X carries its Borel σ-algebra
(BorelSpace X).
Blueprint: def:abstract-continuous-functional-calculus
Fields
map_smul_add : ∀ (α β : ℂ) (f g : C(X, ℂ)), Φ (α • f + β • g) = α • Φ f + β • Φ g
Φ is linear: Φ(αf + βg) = αΦ(f) + βΦ(g).
map_mul : ∀ (f g : C(X, ℂ)), Φ (f * g) = Φ f * Φ g
Φ is multiplicative: Φ(fg) = Φ(f)Φ(g).
map_star : ∀ (f : C(X, ℂ)), Φ (star f) = ContinuousLinearMap.adjoint (Φ f)
Φ sends the complex conjugate f̄ to the adjoint Φ(f)*.
norm_map : ∀ (f : C(X, ℂ)), ‖Φ f‖ = ‖f‖
Φ is isometric: ‖Φ(f)‖ = sup |f| over X.
map_one : Φ 1 = 1
Φ sends the constant function 1 to the identity 𝟙.
🔗def
The projection-valued measure on X defined by an abstract continuous functional calculus Φ:
each measurable set E goes to the projection Φ̃(1(E)), the extended calculus of its indicator
function.
Φ̃(1(E)) is a projection because 1(E)² = 1(E) and 1(E) is real. Countable additivity is a
consequence of the convergence of ⟨φ, Φ̃(fₙ)ψ⟩ along bounded pointwise convergent sequences fₙ
(tendsto_inner_extendedCalculus), applied to the indicators of the remainders of a disjoint
union. Its integral is the extended calculus: ∫ f dμ = Φ̃(f) for bounded measurable f, and so
∫ f dμ = Φ(f) for continuous f (abstractPVM_integral, abstractPVM_integral_continuous). For
Φ the functional calculus of a normal operator A, this is the spectral measure of A.
Implementation note: the value on a non-measurable set is 0, as the structure
ProjectionValuedMeasure requires; it holds because extendedCalculus is 0 on functions that
are not bounded and measurable.
Blueprint: thrm:abstract-calculus-yields-pvm
The measures \mu_\psi and the extended calculus are
abstractMeasure and
extendedCalculus; the latter, like the
bounded integral, is 0 on functions that are not bounded and measurable. The spectral theorem
for bounded normal operators:
open Physicslib4 Spectral Unbounded in
Physicslib4.Spectral.Unbounded.existsUnique_spectralMeasure_normal.{u_1} {H : Type u_1} [NormedAddCommGroup H]
[InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsStarNormal A) :
∃! μ, (μ.integral fun lam => ↑lam) = A#check existsUnique_spectralMeasure_normal
Physicslib4.Spectral.Unbounded.existsUnique_spectralMeasure_normal.{u_1} {H : Type u_1} [NormedAddCommGroup H]
[InnerProductSpace ℂ H] [CompleteSpace H] {A : H →L[ℂ] H} (hA : IsStarNormal A) :
∃! μ, (μ.integral fun lam => ↑lam) = A
Here μ ranges over ProjectionValuedMeasure (spectrum ℂ A) H, and the integrand is
\lambda on the complex spectrum. It has the form of the bounded self-adjoint theorem of the
bounded chapter, with spectrum ℂ A in place of spectrum ℝ A.
The ambient form of uniqueness, for a measure on a larger compact set such as the unit circle, is
eq_of_integral_id_eq_ambient.
3.3.7. The Cayley transform🔗
Blueprint: lmm:unitary-is-normal, lmm:cayley-map, thrm:hall-10.28,
lmm:cayley-spectral-mapping, lmm:borel-bijection-transports-pvm,
lmm:cayley-omits-one, prpstn:hall-10.29, thrm:hall-10.30.
🔗def
The Cayley map C(x) = (x + i)/(x − i), which sends the real line onto the unit circle with the
point 1 removed.
It is the scalar version of the Cayley transform: substituting a self-adjoint operator A for x
gives the unitary operator U = (A + i𝟙)(A − i𝟙)⁻¹. Since |x + i| = |x − i| for real x, C(x) has
modulus 1, and C(x) = 1 is impossible; as x runs from −∞ to +∞, C(x) goes once around the
circle, starting and ending at 1. C is continuous (continuous_cayleyMap) and bijective onto
unitCircleMinusOne (bijOn_cayleyMap), with inverse cayleyInv.
Blueprint: lmm:cayley-map
The existence theorem
exists_isCayleyTransform gives,
besides IsCayleyTransform A B U: U is unitary, U - \mathbf{1} is injective with
range \mathrm{Dom}(A), A(U - \mathbf{1})\chi = i(U + \mathbf{1})\chi, and
U - \mathbf{1} = 2iB. The Cayley map sends \sigma(A) onto \sigma(U) \setminus \{1\}
(mem_spectrum_iff_cayleyMap_mem_spectrum,
cayleyMap_image_spectrum),
the spectral measure of U gives no mass to 1
(spectralMeasure_singleton_one_eq_zero),
and A = \int D \, d\mu^U
(pmapIntegral_cayleyInv_eq,
with D the function cayleyInv).
🔗def
The projection-valued measure on ℝ obtained from a projection-valued measure μ(U) on the
spectrum of a unitary U through the inverse Cayley map: a Borel set E goes to μ(U)(C(E)).
When U is the Cayley transform of a self-adjoint A and μ(U) its spectral measure, this is the
spectral measure of A: ∫ λ dμ(λ) = A (pmapIntegral_cayleyPVM_id). The point 1 of the circle,
which corresponds to no real number, carries no mass (spectralMeasure_singleton_one_eq_zero),
so nothing of μ(U) is lost.
Implementation note: C(E) is written as the set of u in σ(U) with D(u) in E, using
cayleyInv; the two agree on the unit circle minus 1. Non-measurable E are sent to 0, as a
projection-valued measure requires; the preimage of a non-Borel set under D can still carry
mass. The blueprint builds the measure by restriction and transport (restrictPVM,
mapPVM); this definition composes with D directly.
Blueprint: thrm:hall-10.30
The existence half of the spectral theorem:
open Physicslib4 Spectral Unbounded in
Physicslib4.Spectral.Unbounded.pmapIntegral_cayleyPVM_id.{u_1} {H : Type u_1} [NormedAddCommGroup H]
[InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) {B U : H →L[ℂ] H}
(hU : IsCayleyTransform A B U) {μU : ProjectionValuedMeasure (↑(spectrum ℂ U)) H}
(hμU : (μU.integral fun u => ↑u) = U) : (pmapIntegral (cayleyPVM μU) fun x => ↑x) = A#check pmapIntegral_cayleyPVM_id
Physicslib4.Spectral.Unbounded.pmapIntegral_cayleyPVM_id.{u_1} {H : Type u_1} [NormedAddCommGroup H]
[InnerProductSpace ℂ H] [CompleteSpace H] [Nontrivial H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) {B U : H →L[ℂ] H}
(hU : IsCayleyTransform A B U) {μU : ProjectionValuedMeasure (↑(spectrum ℂ U)) H}
(hμU : (μU.integral fun u => ↑u) = U) : (pmapIntegral (cayleyPVM μU) fun x => ↑x) = A
The blueprint's restriction and transport of projection-valued measures are
restrictPVM and
mapPVM; the pushforward used for uniqueness is
pushforwardPVM.
3.3.8. The spectral theorem and the functional calculus🔗
Blueprint: thrm:hall-10.4, def:spectral-measure, def:hall-10.5,
lmm:functional-calculus-bounded.
The headline theorem of the section:
open Physicslib4 Spectral Unbounded in
Physicslib4.Spectral.Unbounded.existsUnique_spectralMeasure_unbounded.{u_1} {H : Type u_1} [NormedAddCommGroup H]
[InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) :
∃! μ, (pmapIntegral μ fun x => ↑x) = A#check existsUnique_spectralMeasure_unbounded
Physicslib4.Spectral.Unbounded.existsUnique_spectralMeasure_unbounded.{u_1} {H : Type u_1} [NormedAddCommGroup H]
[InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) :
∃! μ, (pmapIntegral μ fun x => ↑x) = A
Here μ ranges over ProjectionValuedMeasure ℝ H. The equation is between partial maps, so it
includes \mathrm{Dom}(A) = W_\lambda, the vectors with \int \lambda^2 \, d\mu_\psi < \infty
(domain_eq_integralDomain_spectralMeasure).
The measure is concentrated on the spectrum:
open Physicslib4 Spectral Unbounded in
Physicslib4.Spectral.Unbounded.spectralMeasure_concentrated.{u_1} {H : Type u_1} [NormedAddCommGroup H]
[InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) {μ : ProjectionValuedMeasure ℝ H}
(hμ : (pmapIntegral μ fun x => ↑x) = A) :
μ {x | ↑x ∉ pmapSpectrum A} = 0 ∧ ∀ (E : Set ℝ), MeasurableSet E → μ E = μ (E ∩ {x | ↑x ∈ pmapSpectrum A})#check spectralMeasure_concentrated
Physicslib4.Spectral.Unbounded.spectralMeasure_concentrated.{u_1} {H : Type u_1} [NormedAddCommGroup H]
[InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) {μ : ProjectionValuedMeasure ℝ H}
(hμ : (pmapIntegral μ fun x => ↑x) = A) :
μ {x | ↑x ∉ pmapSpectrum A} = 0 ∧ ∀ (E : Set ℝ), MeasurableSet E → μ E = μ (E ∩ {x | ↑x ∈ pmapSpectrum A})
🔗def
The spectral measure μ(A) of a self-adjoint operator A: the unique projection-valued measure on
the Borel sets of ℝ with ∫ λ dμ(A)(λ) = A.
For a Borel set E, μ(A)(E) is the projection onto the states in which a measurement of A gives
a value in E with certainty, and E ↦ ⟨ψ, μ(A)(E)ψ⟩ is the probability distribution of A in the
unit vector ψ. Its defining property is pmapIntegral_spectralMeasure, its uniqueness
eq_spectralMeasure_of_pmapIntegral, and Dom(A) is the set of ψ with ∫ λ² finite against that
distribution (domain_eq_integralDomain_spectralMeasure).
Implementation note: the measure is the one supplied by the spectral theorem
existsUnique_spectralMeasure_unbounded, extracted with Exists.choose; by uniqueness no
choice is involved in its value.
Blueprint: def:spectral-measure
🔗def
The functional calculus of a self-adjoint operator A: the operator f(A) = ∫ f(λ) dμ(A)(λ) for a
measurable function f : ℝ → ℂ, possibly unbounded, with domain the vectors ψ for which
∫ |f|² is finite against the spectral distribution of ψ.
This gives a meaning to any measurable function of an observable: the Hamiltonian Ĥ gives the
time evolution e^(−itĤ), a position operator gives the projections onto regions of space, and
so on. When f(λ) = λ one recovers A itself (functionalCalculus_id). A bounded f gives a
bounded operator defined on all of H, equal to the bounded integral of f against μ(A)
(functionalCalculus_of_bddMeasurable); this is the case of the unitary group e^(itA) of
Stone's theorem.
Implementation note: the operator is pmapIntegral for spectralMeasure, with domain
integralDomain (functionalCalculus_domain). Measurability of f is not part of the
definition; the results about f(A) assume it where they need it. The properties proved for
pmapIntegral transfer to it through this definition.
Blueprint: def:hall-10.5
Since f(A) is by definition pmapIntegral for the spectral measure, the theorems of the
integration subsection apply to it: for example, f(A) is self-adjoint for real measurable
f by isSelfAdjoint_pmapIntegral_of_real. For bounded measurable f, f(A) is bounded
and defined everywhere. The prefix Unbounded. below distinguishes the declarations from their
bounded namesakes of the bounded chapter:
open Physicslib4 Spectral Unbounded in
Physicslib4.Spectral.Unbounded.functionalCalculus_of_bddMeasurable.{u_1} {H : Type u_1} [NormedAddCommGroup H]
[InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) {f : ℝ → ℂ}
(hf : f ∈ BddMeasurable ℝ) :
(Unbounded.functionalCalculus hA f).domain = ⊤ ∧
Unbounded.functionalCalculus hA f = (↑((Unbounded.spectralMeasure hA).integral f)).toPMap ⊤#check functionalCalculus_of_bddMeasurable
Physicslib4.Spectral.Unbounded.functionalCalculus_of_bddMeasurable.{u_1} {H : Type u_1} [NormedAddCommGroup H]
[InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) {f : ℝ → ℂ}
(hf : f ∈ BddMeasurable ℝ) :
(Unbounded.functionalCalculus hA f).domain = ⊤ ∧
Unbounded.functionalCalculus hA f = (↑((Unbounded.spectralMeasure hA).integral f)).toPMap ⊤
The unitary group e^{itA} of Stone's theorem is of this kind.