Lemma 3.5 — sums and products of spectral integrals

Proved

TeschlQM.Spectral.spectralIntegral_add_mul

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$ , let $f, g$ be Borel functions and $\alpha, \beta \in \mathbb{C}$ . Then

\alpha P(f) + \beta P(g) \subseteq P(\alpha f + \beta g), \qquad \mathfrak D(\alpha P(f) + \beta P(g)) = \mathfrak D_{|f|+|g|} \qquad (3.38)

and

P(f)P(g) \subseteq P(fg), \qquad \mathfrak D(P(f)P(g)) = \mathfrak D_g \cap \mathfrak D_{fg} \qquad (3.39).

Here $\alpha P(f) + \beta P(g)$ has domain $\mathfrak D(P(f)) \cap \mathfrak D(P(g))$ , $P(f)P(g)$ has domain $\{\psi \in \mathfrak D(P(g)) \mid P(g)\psi \in \mathfrak D(P(f))\}$ , and $S \subseteq T$ means that $T$ extends $S$ .

Formalization Note. Sum and scalar multiple are Mathlib's LinearPMap operations (the domain of a sum is the intersection of domains, and $\alpha T$ has the domain of $T$ also for $\alpha = 0$ , as for operators in the book), and $\subseteq$ is the order ≤ on LinearPMaps. Mathlib has no composition of arbitrary partially defined operators, so (3.39) is written out: a vector lies in the natural domain of $P(f)P(g)$ iff it lies in $\mathfrak D_g \cap \mathfrak D_{fg}$ , and for every such vector $\psi$ one has $\psi \in \mathfrak D(P(fg))$ and $P(f)(P(g)\psi) = P(fg)\psi$ .

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. 94, Lemma 3.5. For Borel functions `f, g` and `α, β ∈ ℂ`:
(3.38) `αP(f) + βP(g) ⊆ P(αf + βg)` with `𝔇(αP(f) + βP(g)) = 𝔇_{|f|+|g|}`, and
(3.39) `P(f)P(g) ⊆ P(fg)` with `𝔇(P(f)P(g)) = 𝔇_g ∩ 𝔇_{fg}`, where `P(f)P(g)` has the natural
domain `{ψ ∈ 𝔇(P(g)) | P(g)ψ ∈ 𝔇(P(f))}`. -/
theorem spectralIntegral_add_mul {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (P : Set ℝ → (H →L[ℂ] H)) (hP : TeschlQM.Shared.IsProjValuedMeasure P) (f g : ℝ → ℂ)
    (hf : Measurable f) (hg : Measurable g) (α β : ℂ) :
    α • spectralIntegral P f + β • spectralIntegral P g ≤ spectralIntegral P (α • f + β • g) ∧
    ((α • spectralIntegral P f + β • spectralIntegral P g).domain : Set H) =
      spectralDomain P (fun x => ((‖f x‖ + ‖g x‖ : ℝ) : ℂ)) ∧
    (∀ ψ : H, (∃ hψ : ψ ∈ (spectralIntegral P g).domain,
        spectralIntegral P g ⟨ψ, hψ⟩ ∈ (spectralIntegral P f).domain) ↔
      ψ ∈ spectralDomain P g ∩ spectralDomain P (f * g)) ∧
    (∀ (ψ : (spectralIntegral P g).domain)
        (h : spectralIntegral P g ψ ∈ (spectralIntegral P f).domain),
      ∃ h' : (ψ : H) ∈ (spectralIntegral P (f * g)).domain,
        spectralIntegral P f ⟨spectralIntegral P g ψ, h⟩ =
          spectralIntegral P (f * g) ⟨ψ, h'⟩) := by sorry

end TeschlQM.Spectral

Source

Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, p. 94, Lemma 3.5

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, g : \mathbb{R} \to \mathbb{C}$ are Borel measurable, not assumed bounded.
$\alpha, \beta \in \mathbb{C}$ are arbitrary.
$P(h)$ denotes the imported partially defined operator spectralIntegral P h, with domain $\mathfrak{D}(P(h))$ .
$\mathfrak{D}_h$ denotes the imported set spectralDomain P h.
$fg$ , $\alpha f + \beta g$ and $|f| + |g|$ are pointwise, with $|f|+|g|$ viewed as a complex-valued function.

For partially defined operators, the operations are Mathlib's:

$\alpha P(f)$ keeps the domain of $P(f)$ , even when $\alpha = 0$ .
A sum is defined on the intersection of the two domains.

So $\alpha P(f) + \beta P(g)$ has domain $\mathfrak{D}(P(f)) \cap \mathfrak{D}(P(g))$ for all $\alpha, \beta$ . " $S \le T$ " means that $T$ extends $S$ : $\mathfrak{D}(S) \subseteq \mathfrak{D}(T)$ and $S\psi = T\psi$ on $\mathfrak{D}(S)$ .

Conclusion. The theorem asserts all four of the following:

$P(\alpha f + \beta g)$ extends $\alpha P(f) + \beta P(g)$ .
The domain of $\alpha P(f) + \beta P(g)$ equals, as a set, $\mathfrak{D}_{|f|+|g|}$ .
For every $\psi \in H$ :

\big(\psi \in \mathfrak{D}(P(g)) \text{ and } P(g)\psi \in \mathfrak{D}(P(f))\big) \iff \psi \in \mathfrak{D}_g \cap \mathfrak{D}_{fg}.

For every $\psi \in \mathfrak{D}(P(g))$ with $P(g)\psi \in \mathfrak{D}(P(f))$ , we have $\psi \in \mathfrak{D}(P(fg))$ and

P(f)\big(P(g)\psi\big) = P(fg)\psi.

Degenerate cases.

When $\alpha = \beta = 0$ , (1) says that $P(0)$ extends the zero map on $\mathfrak{D}(P(f)) \cap \mathfrak{D}(P(g))$ . Part (2) still identifies that intersection with $\mathfrak{D}_{|f|+|g|}$ , independent of $\alpha$ and $\beta$ .
If $H = \{0\}$ , all domains are $\{0\}$ and every part holds trivially.
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