How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Stone resolvent formula for spectral projections
Statement
Assume AC. Let be a bounded self-adjoint operator on a nonzero complex Hilbert space with spectral projection valued measure on the compact set , and let be real. For every Borel set , write . Then, with the resolvents defined for by Spectrum and resolvent of a bounded operator and the integral of a continuous -valued function understood in the Bochner sense (Bochner-integrable function),
in the strong operator topology as . In particular, if then the limit is the spectral projection , and the half-masses at and appear exactly when these points are atoms of the spectrum.
Facts & Assumptions
For the function is bounded and Borel on , with , and its Borel calculus value satisfies : indeed and by linearity and multiplicativity of the Borel calculus (Borel functional calculus for bounded normal operators, Borel functional calculus for a bounded normal operator).
for self-adjoint , so the functions are defined on the spectrum (Spectrum of a self adjoint operator is real).
A continuous function on the compact interval with values in the Banach space is Bochner integrable, and a bounded linear map satisfies (Bochner integrability criterion, Bounded linear maps commute with Bochner integration).
The Borel calculus is a unital star-homomorphism: , and uniformly bounded pointwise -almost everywhere convergence implies strong convergence (Pvm integral is a star homomorphism, Projection valued measure).
AC is the declared choice hypothesis of this page from the construction item onward (The Axiom of Choice).
Proof
Given: A bounded self-adjoint operator with spectral PVM on , real numbers , and .
Resolvent identity: since , the function is bounded Borel for and (A1) identifies , so the integrand is a continuous -valued function on the compact interval and the Bochner integral converges.
Scalar kernel: for real and one computes , hence the bounded Borel function equals , with and, for every real , as .
The operator integral is the calculus value of the kernel: by linearity of and commutation of the bounded linear map with Bochner integration, .
Strong limit: and pointwise, so the strong-convergence clause of the calculus gives in the strong operator topology.
Therefore the resolvent expression converges strongly to as ; if the endpoint atoms vanish and the limit is the open-interval spectral projection .
Depends on
- Borel functional calculus for bounded normal operators
- Borel functional calculus for a bounded normal operator
- Pvm integral is a star homomorphism
- Bounded borel pvm integral
- Bounded linear maps commute with Bochner integration
- Bochner-integrable function
- Bochner integrability criterion
- Spectrum of a self adjoint operator is real
- Spectrum and resolvent of a bounded operator
- Projection valued measure
- The Axiom of Choice
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
59 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Gerald Teschl, Mathematical Methods in Quantum Mechanics, 2nd ed., Theorem 4.3, printed pp.113–115 (standard reference, not scraped)
- Theo Bühler and Dietmar Salamon, Functional Analysis, Lemma 5.79, printed pp.285–288 (standard reference, not scraped)