Theorem 3.1 — the bounded functional calculus of a projection-valued measure

Proved

TeschlQM.Spectral.bounded_functional_calculus

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

functional-analysisfunctional-calculusp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1spectral-theory

Let $P$ be a projection-valued measure on a complex Hilbert space $\mathfrak H$ , and for a bounded Borel function $f \in B(\mathbb{R})$ let $P(f) = \int_{\mathbb{R}} f(\lambda)\,dP(\lambda) \in \mathfrak L(\mathfrak H)$ . Then the map

P : B(\mathbb{R}) \to \mathfrak L(\mathfrak H), \qquad f \mapsto \int_{\mathbb{R}} f(\lambda)\, dP(\lambda)

is a $C^*$ -algebra homomorphism of norm one: $P(1) = \mathbb{I}$ , $P(f+g) = P(f) + P(g)$ , $P(cf) = cP(f)$ , $P(fg) = P(f)P(g)$ , $P(f^*) = P(f)^*$ and $\|P(f)\| \le \sup_{\lambda} |f(\lambda)|$ for all $f, g \in B(\mathbb{R})$ , $c \in \mathbb{C}$ . Moreover, for $f, g \in B(\mathbb{R})$ and $\varphi, \psi \in \mathfrak H$ ,

\langle P(g)\varphi, P(f)\psi\rangle = \int_{\mathbb{R}} g^*(\lambda) f(\lambda)\, d\mu_{\varphi,\psi}(\lambda) \qquad (3.21).

Finally, if $f_n \in B(\mathbb{R})$ , $f_n(x) \to f(x)$ for every $x$ , and $\sup_{\lambda\in\mathbb{R}} |f_n(\lambda)|$ is bounded in $n$ , then $P(f_n)\psi \to P(f)\psi$ for every $\psi \in \mathfrak H$ (strong convergence).

This is the functional calculus for bounded functions on which the unbounded calculus and the spectral theorem are built.

Formalization Note. $f^*$ is the pointwise complex conjugate (star f), $P(f)^*$ the Hilbert-space adjoint (star on H →L[ℂ] H). The sup norm $\sup_\lambda |f(\lambda)|$ is the real supremum ⨆ x, ‖f x‖, which is the true supremum since $f$ is bounded. "Norm one" is the bound $\|P(f)\| \le \|f\|_\infty$ together with $P(1) = \mathbb{I}$ , which has norm one when $\mathfrak H \ne \{0\}$ . The integral against $\mu_{\varphi,\psi}$ is spectralForm, the polarization (3.15) of four spectral-measure integrals. In the convergence clause the limit $f$ is not assumed measurable or bounded: both follow from the hypotheses.

Preamble

import Mathlib
import Definitions.Def_TeschlQM_Shared_IsProjValuedMeasure
import Definitions.Def_TeschlQM_Spectral_spectralMeasure
import Definitions.Def_TeschlQM_Spectral_boundedSpectralIntegral

open MeasureTheory
open scoped ENNReal InnerProductSpace

Formal statement

namespace TeschlQM.Spectral

/-- Teschl, p. 90, Theorem 3.1. For a projection-valued measure `P`, the map
`f ↦ P(f) = ∫_ℝ f(λ) dP(λ)` from the bounded Borel functions `B(ℝ)` (sup norm) to `𝔏(H)` is a
unital C*-algebra homomorphism (linear, multiplicative, `P(f*) = P(f)*`) of norm one
(`‖P(f)‖ ≤ sup_λ |f(λ)|`, attained at `f = 1` when `H ≠ 0`), satisfies (3.21)
`⟨P(g)φ, P(f)ψ⟩ = ∫ g* f dμ_{φ,ψ}`, and `P(fₙ) → P(f)` strongly whenever `fₙ → f` pointwise
with `sup_λ |fₙ(λ)|` bounded in `n`. -/
theorem bounded_functional_calculus {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (P : Set ℝ → (H →L[ℂ] H)) (hP : TeschlQM.Shared.IsProjValuedMeasure P) :
    boundedSpectralIntegral P 1 = 1 ∧
    (∀ f g : ℝ → ℂ, IsBoundedBorel f → IsBoundedBorel g →
      boundedSpectralIntegral P (f + g) =
          boundedSpectralIntegral P f + boundedSpectralIntegral P g ∧
      boundedSpectralIntegral P (f * g) =
          boundedSpectralIntegral P f * boundedSpectralIntegral P g) ∧
    (∀ (c : ℂ) (f : ℝ → ℂ), IsBoundedBorel f →
      boundedSpectralIntegral P (c • f) = c • boundedSpectralIntegral P f) ∧
    (∀ f : ℝ → ℂ, IsBoundedBorel f →
      boundedSpectralIntegral P (star f) = star (boundedSpectralIntegral P f)) ∧
    (∀ f : ℝ → ℂ, IsBoundedBorel f → ‖boundedSpectralIntegral P f‖ ≤ ⨆ x, ‖f x‖) ∧
    (∀ f g : ℝ → ℂ, IsBoundedBorel f → IsBoundedBorel g → ∀ φ ψ : H,
      ⟪boundedSpectralIntegral P g φ, boundedSpectralIntegral P f ψ⟫_ℂ =
        spectralForm P φ ψ (star g * f)) ∧
    (∀ (fs : ℕ → ℝ → ℂ) (f : ℝ → ℂ), (∀ n, IsBoundedBorel (fs n)) →
      (∀ x, Filter.Tendsto (fun n => fs n x) Filter.atTop (nhds (f x))) →
      (∃ C : ℝ, ∀ n x, ‖fs n x‖ ≤ C) →
      ∀ ψ : H, Filter.Tendsto (fun n => boundedSpectralIntegral P (fs n) ψ) Filter.atTop
        (nhds (boundedSpectralIntegral P f ψ))) := by sorry

end TeschlQM.Spectral

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 90, Theorem 3.1

Read-back

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

Setting.

$H$ is a complex Hilbert space, possibly $\{0\}$ , with inner product linear in the second argument and conjugate-linear in the first.
$P$ maps subsets of $\mathbb{R}$ to bounded operators on $H$ and satisfies the imported predicate IsProjValuedMeasure, whose content is not shown here.
$\mathcal{P}(f)$ denotes boundedSpectralIntegral P f, a bounded operator on $H$ , and "bounded Borel" denotes the predicate IsBoundedBorel. Both come from an imported file.
$\mathcal{S}_P(\varphi,\psi;h)$ denotes the imported spectralForm P φ ψ h.
For functions, $f+g$ , $fg$ and $cf$ are pointwise, and $\bar f$ is the pointwise complex conjugate. For operators, $T^*$ is the Hilbert-space adjoint and $ST$ is composition.

Conclusion. The theorem asserts all seven of the following:

$\mathcal{P}(\mathbf 1) = I$ , where $\mathbf 1$ is the constant function $1$ and $I$ is the identity operator. This part carries no hypothesis on $f$ .
For all bounded Borel $f, g$ :

\mathcal{P}(f+g) = \mathcal{P}(f) + \mathcal{P}(g) \quad\text{and}\quad \mathcal{P}(fg) = \mathcal{P}(f)\,\mathcal{P}(g).

For all $c \in \mathbb{C}$ and bounded Borel $f$ : $\mathcal{P}(cf) = c\,\mathcal{P}(f)$ .
For every bounded Borel $f$ : $\mathcal{P}(\bar f) = \mathcal{P}(f)^*$ .
For every bounded Borel $f$ , the operator norm satisfies

\|\mathcal{P}(f)\| \le \sup_{x\in\mathbb{R}} |f(x)|.

Only this inequality is asserted; the theorem does not assert that it is attained for any $f$ . 6. For all bounded Borel $f, g$ and all $\varphi, \psi \in H$ :

\langle \mathcal{P}(g)\varphi,\; \mathcal{P}(f)\psi\rangle = \mathcal{S}_P(\varphi,\psi;\bar g f).

Let $(f_n)_{n\in\mathbb{N}}$ be a sequence with the following properties:
- each $f_n$ is bounded Borel;
- $f_n(x) \to f(x)$ for every $x \in \mathbb{R}$ ;
- there is a single real $C$ with $|f_n(x)| \le C$ for all $n$ and $x$ .
Then for every $\psi \in H$ , $\mathcal{P}(f_n)\psi \to \mathcal{P}(f)\psi$ in the norm of $H$ . The limit $f$ is not separately assumed bounded Borel. As a pointwise limit of measurable functions bounded by $C$ , it is automatically measurable and bounded by $C$ .

Degenerate cases.

The supremum in (5) is taken over the nonempty set $\mathbb{R}$ . It is finite for bounded $f$ , so the default value for unbounded suprema does not arise under the hypothesis.
If $H = \{0\}$ , every operator equals both $0$ and $I$ , and every conclusion holds trivially.
The strength of the whole theorem depends on the imported hypothesis IsProjValuedMeasure, whose content is not shown. If it were unsatisfiable, all seven conclusions 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