Theorem 3.8 — the spectrum in terms of spectral projections

Proved

TeschlQM.Spectral.spectrum_eq

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 $A$ be a self-adjoint operator in a complex Hilbert space $\mathfrak H$ and let $P_A$ be its projection-valued measure, the projection-valued measure with $A = \int_{\mathbb{R}} \lambda\, dP_A(\lambda)$ (unique by the spectral theorem). Then

\sigma(A) = \{\lambda \in \mathbb{R} \mid P_A((\lambda - \varepsilon, \lambda + \varepsilon)) \ne 0 \text{ for all } \varepsilon > 0\} \qquad (3.53).

Thus the spectrum is the support of the projection-valued measure; in particular it is real.

Formalization Note. $P_A$ enters as a projection-valued measure P with the hypothesis A = spectralIntegral P (fun x => x); by the uniqueness part of Theorem 3.7 this is exactly $P_A$ , so no generality is lost or gained. $\sigma(A)$ is the resolvent-based spectrum TeschlQM.Spectral.spectrum of p. 73 (a subset of $\mathbb{C}$ ), and the right-hand side is the image of the real set under $\mathbb{R} \hookrightarrow \mathbb{C}$ . The hypothesis IsSelfAdjoint A is the book's; it also follows from the other two.

Preamble

import Mathlib
import Definitions.Def_TeschlQM_Shared_IsProjValuedMeasure
import Definitions.Def_TeschlQM_Spectral_spectralIntegral
import Definitions.Def_TeschlQM_Spectral_spectrum

open MeasureTheory
open scoped ENNReal InnerProductSpace

Formal statement

namespace TeschlQM.Spectral

/-- Teschl, p. 97, Theorem 3.8. Let `A` be self-adjoint and `P_A` its projection-valued measure,
i.e. the projection-valued measure with `A = ∫_ℝ λ dP_A(λ)` (unique by Theorem 3.7). Then
`σ(A) = {λ ∈ ℝ | P_A((λ − ε, λ + ε)) ≠ 0 for all ε > 0}` (3.53). -/
theorem spectrum_eq {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (A : H →ₗ.[ℂ] H) (hA : IsSelfAdjoint A) (P : Set ℝ → (H →L[ℂ] H))
    (hP : TeschlQM.Shared.IsProjValuedMeasure P) (hAP : A = spectralIntegral P (fun x => (x : ℂ))) :
    spectrum A =
      (fun x : ℝ => (x : ℂ)) ''
        {x : ℝ | ∀ ε : ℝ, 0 < ε → P (Set.Ioo (x - ε) (x + ε)) ≠ 0} := by sorry

end TeschlQM.Spectral

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 97, Theorem 3.8

Read-back

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

Setting.

$H$ is a complex Hilbert space, possibly $\{0\}$ .
$A$ is a partially defined linear operator on $H$ that is self-adjoint in Mathlib's sense: $A^* = A$ , meaning the adjoint has the same domain and agrees with $A$ there.
$P$ maps subsets of $\mathbb{R}$ to bounded operators on $H$ and satisfies the imported predicate IsProjValuedMeasure, whose content is not shown.
It is assumed that $A$ equals, as a partially defined operator, the imported spectralIntegral P applied to the identity function $x \mapsto x$ viewed as complex-valued.
$\sigma(A)$ denotes the imported spectrum A, a subset of $\mathbb{C}$ .

Conclusion.

\sigma(A) = \big\{\, x \in \mathbb{R} \;:\; P\big((x-\varepsilon,\,x+\varepsilon)\big) \ne 0 \text{ for every real } \varepsilon > 0 \,\big\},

where the right-hand side, a set of reals, is viewed as a subset of $\mathbb{C}$ via $x \mapsto x + 0i$ .

In particular, the statement asserts that $\sigma(A)$ contains no non-real numbers. $P$ is evaluated here only on open intervals.

Degenerate cases.

If $H = \{0\}$ , every $P(\Omega)$ is the zero operator. The right-hand side is then empty, so the statement asserts $\sigma(A) = \emptyset$ .
The hypotheses $A^* = A$ and $A =$ spectralIntegral P (x ↦ x) are both imposed. If they cannot hold together with IsProjValuedMeasure P, the theorem is vacuous; the content of that predicate is not shown here.

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