Theorem 3.7 — Spectral theorem for unbounded self-adjoint operators

Proved

TeschlQM.Spectral.spectral_theorem

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-analysisp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1self-adjoint-operatorsspectral-theory

Let $\mathfrak H$ be a complex Hilbert space and let $A$ be a self-adjoint operator in $\mathfrak H$ (densely defined, with $A^* = A$ , domains included). Then there is a unique projection-valued measure $P_A$ on the Borel sets of $\mathbb{R}$ such that

A = \int_{\mathbb{R}} \lambda\, dP_A(\lambda) \qquad (3.49),

that is, $A$ equals the spectral integral $P_A(f)$ of the function $f(\lambda) = \lambda$ : $\mathfrak D(A) = \{\psi \mid \int \lambda^2\, d\mu_\psi(\lambda) < \infty\}$ and $\langle\psi, A\psi\rangle = \int \lambda\, d\mu_\psi(\lambda)$ on it, where $\mu_\psi$ are the spectral measures of $P_A$ .

The theorem converts every self-adjoint operator into a multiplication by the identity function against a projection-valued measure; it is what gives meaning to $f(A) = P_A(f)$ , to the unitary group $e^{-itA}$ and to the spectral projections $P_A(\Omega)$ used throughout quantum mechanics.

Formalization Note. $A$ is a LinearPMap H →ₗ.[ℂ] H and self-adjointness is Mathlib's IsSelfAdjoint A (which includes density of the domain). The equality in (3.49) is equality of LinearPMaps, domains included, with spectralIntegral. Existence and uniqueness are both asserted; uniqueness says any projection-valued measure $Q$ with $A = \int \lambda\, dQ(\lambda)$ agrees with $P_A$ on every Borel set. The only hypothesis is self-adjointness; the Hilbert space is not assumed separable (the result and the book's proof do not need it).

Preamble

import Mathlib
import Definitions.Def_TeschlQM_Shared_IsProjValuedMeasure
import Definitions.Def_TeschlQM_Spectral_spectralIntegral

open MeasureTheory
open scoped ENNReal InnerProductSpace

Formal statement

namespace TeschlQM.Spectral

/-- Teschl, p. 96, Theorem 3.7 (Spectral theorem). To every self-adjoint operator `A` there
corresponds a unique projection-valued measure `P_A` such that `A = ∫_ℝ λ dP_A(λ)` (3.49), the
equality being one of operators, domains included. Uniqueness is among projection-valued
measures, which are determined by their values on Borel sets. -/
theorem spectral_theorem {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (A : H →ₗ.[ℂ] H) (hA : IsSelfAdjoint A) :
    ∃ P : Set ℝ → (H →L[ℂ] H), TeschlQM.Shared.IsProjValuedMeasure P ∧
      A = spectralIntegral P (fun x => (x : ℂ)) ∧
      ∀ Q : Set ℝ → (H →L[ℂ] H), TeschlQM.Shared.IsProjValuedMeasure Q →
        A = spectralIntegral Q (fun x => (x : ℂ)) →
        ∀ Ω : Set ℝ, MeasurableSet Ω → Q Ω = P Ω := by sorry

end TeschlQM.Spectral

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 96, Theorem 3.7

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $H$ be any complex inner product space ( $\langle\cdot,\cdot\rangle$ over $\mathbb{C}$ ) that is complete in the induced norm, i.e. a complex Hilbert space. No separability or dimension assumption is made. Let $A$ be a partially defined $\mathbb{C}$ -linear operator on $H$ . That is, $A$ consists of a linear subspace $\mathcal{D}(A) \subseteq H$ , its domain, which is not assumed dense or closed, together with a linear map $\mathcal{D}(A) \to H$ . The hypothesis is that $A$ is self-adjoint in Mathlib's sense for partially defined operators, $A^* = A$ . This is an equality of partial operators, so the domains agree, $\mathcal{D}(A^*) = \mathcal{D}(A)$ , and the two maps agree on that common domain.

Here $A^*$ is Mathlib's adjoint. Its domain is the set of $y \in H$ for which $x \mapsto \langle y, Ax\rangle$ is continuous on $\mathcal{D}(A)$ . On that domain it acts as the usual adjoint when $\mathcal{D}(A)$ is dense. When $\mathcal{D}(A)$ is not dense, Mathlib defines it to be the zero map.

The statement uses two definitions from this bundle whose bodies are not supplied to this read-back, so their content cannot be unfolded here:

a predicate $\mathrm{IsProjValuedMeasure}(P)$ on functions $P$ from subsets of $\mathbb{R}$ to bounded operators;
an operation $\mathrm{spectralIntegral}(P, f)$ that takes such a $P$ and a function $f : \mathbb{R} \to \mathbb{C}$ and returns a partially defined linear operator on $H$ .

Whatever properties these names suggest, the read-back can only say that the statement holds with respect to whatever those definitions actually say.

With that understood, the statement asserts that there exists a function

P : \mathcal{P}(\mathbb{R}) \to \mathcal{B}(H),

assigning a bounded (continuous) $\mathbb{C}$ -linear operator on $H$ to every subset of $\mathbb{R}$ , measurable or not, such that all three of the following hold:

$\mathrm{IsProjValuedMeasure}(P)$ holds.
The following is an equality of partial operators, so both the domains and the values coincide:

A = \mathrm{spectralIntegral}\big(P,\ x \mapsto x\big),

where $x \mapsto x$ is the identity function $\mathbb{R} \to \mathbb{C}$ , $x \mapsto x + 0i$ . 3. Uniqueness on measurable sets. Let $Q : \mathcal{P}(\mathbb{R}) \to \mathcal{B}(H)$ be any other function such that $\mathrm{IsProjValuedMeasure}(Q)$ holds and $A = \mathrm{spectralIntegral}(Q, x \mapsto x)$ , again as partial operators. Then

Q(\Omega) = P(\Omega) \quad \text{for every Borel-measurable } \Omega \subseteq \mathbb{R}.

The measurable structure is the standard Borel $\sigma$ -algebra on $\mathbb{R}$ . Nothing is asserted about $Q(\Omega)$ versus $P(\Omega)$ for non-measurable $\Omega$ , unless the unseen predicate $\mathrm{IsProjValuedMeasure}$ itself constrains those values.

The conclusion is thus an existence claim together with agreement on Borel sets. It does not assert that $P$ is unique as a function on all of $\mathcal{P}(\mathbb{R})$ .

Degenerate cases. The self-adjointness hypothesis is satisfiable in every such $H$ ; for example, the zero operator with domain $H$ satisfies it. Under Mathlib's convention above, it cannot be satisfied by an operator with non-dense domain. Such an $A$ would have to equal the zero map on its domain. But the adjoint of a zero map has all of $H$ as its domain, which would force $\mathcal{D}(A) = H$ , and $H$ is dense. So the theorem is never vacuous, and every $A$ it covers is densely defined.

If $H = \{0\}$ , every bounded operator is $0$ , so every $P$ and $Q$ is the constant zero map and the uniqueness clause holds trivially. Existence then amounts to the constant zero function satisfying $\mathrm{IsProjValuedMeasure}$ , with $\mathrm{spectralIntegral}$ of it returning the zero operator on $\{0\}$ . Whether that holds depends on the unseen definitions.

The integrand $x \mapsto x$ is unbounded on $\mathbb{R}$ . Whatever domain or default value $\mathrm{spectralIntegral}$ assigns to unbounded or non-integrable integrands is exactly what the equalities in items 2 and 3 compare against $A$ . This read-back cannot state what that is.

Human review

Endorsed by Shuze Chen · Oct 2, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 2, 2026
Confirmed by the mission captain (proposal self-audit).

View graph