Corollary 3.9 — $P_A(\sigma(A)) = \mathbb{I}$ and $P_A(\mathbb{R}\cap\rho(A)) = 0$

Proved

TeschlQM.Spectral.projection_spectrum

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 ( $A = \int_{\mathbb{R}} \lambda\, dP_A(\lambda)$ ). Then

P_A(\sigma(A)) = \mathbb{I} \qquad\text{and}\qquad P_A(\mathbb{R} \cap \rho(A)) = 0 \qquad (3.54).

Consequently $P_A(f) = P_A(\chi_{\sigma(A)} f)$ : functions of $A$ only depend on the values of $f$ on the spectrum.

Formalization Note. As in Theorem 3.8, $P_A$ is a projection-valued measure P with A = spectralIntegral P (fun x => x). The sets $\sigma(A)$ and $\mathbb{R} \cap \rho(A)$ are subsets of $\mathbb{C}$ ; they enter as the real sets $\{x \in \mathbb{R} \mid x \in \sigma(A)\}$ and $\{x \in \mathbb{R} \mid x \in \rho(A)\}$ (both Borel, since $\sigma(A)$ is closed).

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, Corollary 3.9. Let `A` be self-adjoint and `P_A` its projection-valued
measure (`A = ∫_ℝ λ dP_A(λ)`). Then `P_A(σ(A)) = 𝕀` and `P_A(ℝ ∩ ρ(A)) = 0` (3.54), where the
subsets `σ(A)` and `ℝ ∩ ρ(A)` of `ℂ` are read as subsets of `ℝ`. -/
theorem projection_spectrum {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 : ℂ))) :
    P {x : ℝ | (x : ℂ) ∈ spectrum A} = 1 ∧
      P {x : ℝ | (x : ℂ) ∈ resolventSet A} = 0 := by sorry

end TeschlQM.Spectral

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 97, Corollary 3.9

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$ as partially defined operators.
$P$ maps every subset of $\mathbb{R}$ to a bounded operator on $H$ and satisfies the imported predicate IsProjValuedMeasure, whose content is not shown.
It is assumed that $A$ equals the imported spectralIntegral P of the function $x \mapsto x$ viewed as complex-valued.
$\sigma(A)$ and $\rho(A)$ denote the imported spectrum A and resolventSet A, subsets of $\mathbb{C}$ .

Conclusion. The theorem asserts both of the following:

P\big(\{x \in \mathbb{R} : x \in \sigma(A)\}\big) = I \qquad\text{and}\qquad P\big(\{x \in \mathbb{R} : x \in \rho(A)\}\big) = 0,

where $I$ is the identity operator on $H$ . The sets are the real points of $\sigma(A)$ and of $\rho(A)$ respectively. The statement does not itself assert that these sets are Borel.

Degenerate cases.

If $H = \{0\}$ , then $I = 0$ and both equalities hold trivially.
If the hypotheses (self-adjointness, the representation of $A$ , and IsProjValuedMeasure P) cannot hold simultaneously, the theorem is vacuous; the content of the imported 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

Corollary 3.9 — PA(σ(A))=IP_A(\sigma(A)) = \mathbb{I}PA​(σ(A))=I and PA(R∩ρ(A))=0P_A(\mathbb{R}\cap\rho(A)) = 0PA​(R∩ρ(A))=0

Corollary 3.9 — $P_A(\sigma(A)) = \mathbb{I}$ and $P_A(\mathbb{R}\cap\rho(A)) = 0$