Theorem 3.2 — $P(f)$ is normal and $P(f)^* = P(f^*)$

Proved

TeschlQM.Spectral.spectralIntegral_normal

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

functional-analysisp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1spectral-theoryunbounded-operators

Let $P$ be a projection-valued measure on a complex Hilbert space $\mathfrak H$ and let $f : \mathbb{R} \to \mathbb{C}$ be a Borel function. Then the operator

P(f) = \int_{\mathbb{R}} f(\lambda)\, dP(\lambda), \qquad \mathfrak D(P(f)) = \mathfrak D_f \qquad (3.28),

exists (it has domain $\mathfrak D_f$ and satisfies $\langle\psi, P(f)\psi\rangle = \int f\, d\mu_\psi$ on it), is normal, and satisfies

P(f)^* = P(f^*) \qquad (3.29),

where $f^*$ is the complex conjugate function.

In particular, for real-valued $f$ the operator $P(f)$ is self-adjoint; for $f(\lambda) = \lambda$ this is the self-adjoint operator $\int \lambda\, dP(\lambda)$ that the spectral theorem inverts.

Formalization Note. $P(f)$ is spectralIntegral P f, a LinearPMap; the first conjunct says it has the defining properties (domain $\mathfrak D_f$ , quadratic form (3.17)). Normality (IsNormalOperator) includes density of $\mathfrak D_f$ , without which the adjoint in (3.29) would be Mathlib's junk adjoint. (3.29) is an equality of LinearPMaps, domains included.

Preamble

import Mathlib
import Definitions.Def_TeschlQM_Shared_IsProjValuedMeasure
import Definitions.Def_TeschlQM_Spectral_spectralIntegral
import Definitions.Def_TeschlQM_Spectral_IsNormalOperator

open MeasureTheory
open scoped ENNReal InnerProductSpace

Formal statement

namespace TeschlQM.Spectral

/-- Teschl, p. 92, Theorem 3.2. For a projection-valued measure `P` and any Borel function `f`,
the operator `P(f) = ∫_ℝ f(λ) dP(λ)` with `𝔇(P(f)) = 𝔇_f` (3.28) is normal and satisfies
`P(f)* = P(f*)` (3.29). -/
theorem spectralIntegral_normal {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (P : Set ℝ → (H →L[ℂ] H)) (hP : TeschlQM.Shared.IsProjValuedMeasure P) (f : ℝ → ℂ) (hf : Measurable f) :
    IsSpectralIntegral P f (spectralIntegral P f) ∧
    IsNormalOperator (spectralIntegral P f) ∧
    (spectralIntegral P f).adjoint = spectralIntegral P (star f) := by sorry

end TeschlQM.Spectral

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 92, Theorem 3.2

Read-back

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

Setting.

$H$ is a complex Hilbert space, possibly $\{0\}$ .
$P$ maps subsets of $\mathbb{R}$ to bounded operators on $H$ and satisfies the imported predicate IsProjValuedMeasure, whose content is not shown.
$f : \mathbb{R} \to \mathbb{C}$ is Borel measurable. It is not assumed bounded.
$P(f)$ denotes the partially defined operator spectralIntegral P f from an imported file.
$\bar f$ is the pointwise complex conjugate of $f$ .

Conclusion. The theorem asserts all three of the following:

The imported predicate IsSpectralIntegral P f holds for the operator $P(f)$ .
$P(f)$ satisfies the imported predicate IsNormalOperator.
The adjoint of $P(f)$ equals $P(\bar f)$ as partially defined operators: they have the same domain and agree on it. Here "adjoint" is Mathlib's adjoint of a partially defined operator, a default value if the domain is not dense.

The meaning of the three imported notions is given by definitions not included in this text.

Degenerate cases.

If $f$ is constant, the conclusions still apply, with no boundedness distinction.
If $H = \{0\}$ , all operators coincide, and the conclusions reduce to whatever the imported predicates say about the zero operator on $\{0\}$ .
If IsProjValuedMeasure were unsatisfiable, the theorem would be vacuous.

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

Theorem 3.2 — P(f)P(f)P(f) is normal and P(f)∗=P(f∗)P(f)^* = P(f^*)P(f)∗=P(f∗)

Theorem 3.2 — $P(f)$ is normal and $P(f)^* = P(f^*)$