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.
Spectral projections and resolution of the identity
Statement
Assume AC. Let be a bounded normal operator on a nonzero complex Hilbert space , with spectral projection valued measure on and Borel calculus . For every Borel set , use the zero-extension convention
Then:
- every spectral projection reduces : it commutes with and , so its range and its kernel are invariant under and ;
- for every : the eigenspace of at is the range of the spectral projection of the singleton , and it is nonzero precisely when ;
- if is self-adjoint, then , , is an increasing family of orthogonal projections which is strongly right continuous, in the strong operator topology, and , strongly.
Facts & Assumptions
The Borel calculus satisfies , , is bounded by , and ; in particular satisfies , , and finite additivity on disjoint measurable sets. Uniformly bounded Borel functions converging pointwise have strongly convergent calculus images (Borel functional calculus for bounded normal operators, Borel functional calculus for a bounded normal operator, Projection valued measure).
and for bounded Borel , with and a finite regular complex measure and a positive measure of mass ; two finite regular complex measures with equal integrals against all continuous functions are equal (Borel functional calculus for a bounded normal operator, The bounded complex dual of C_0(X) is regular complex measures, Scalar and complex measures from a pvm, Borel functional calculus for bounded normal operators).
For normal and continuous one has whenever (Continuous functional calculus properties).
For self-adjoint one has , and , so (Spectrum of a self adjoint operator is real, Self adjoint norm and spectrum extrema).
The adjoint product rule and involution and the definition of the spectrum via (Hilbert-adjoint identities, Spectrum and resolvent of a bounded operator, Self-adjoint, positive, unitary and normal operators).
AC is the declared choice hypothesis of this page from the construction item onward (The Axiom of Choice).
Proof
Given: A nonzero complex Hilbert space , a bounded normal operator with spectral PVM and Borel calculus , a Borel set and a scalar .
commutes with and : and is self-adjoint, so taking adjoints gives ; hence and are invariant under and .
Eigenvectors of spectral projections: if then , so .
For self-adjoint define for real ; for the set is contained in , so , and is the image of an indicator and therefore an orthogonal projection: is increasing in the projection order.
Conversely, suppose . For the identity holds by linearity, with no point evaluation. For , the operator has nonzero kernel and is not invertible, so . Thus evaluation at and the Dirac measure on are defined. This Dirac measure is regular: a set containing contains the compact singleton, and a set omitting it has the open superset of zero mass. Now for every continuous one has , so the positive measure and the mass are finite regular measures with equal integrals against all continuous functions and hence are equal; therefore , which gives and, since , the identity ; with the preceding step this proves .
Strong right continuity: fix and put for . The Borel indicators of are bounded by one and converge pointwise to zero. Hence converges strongly to zero. For , the norm-square formula for indicators gives . This proves the full right-hand strong limit as , for every .
Limits at infinity: since , for the set is empty and , while for it is all of and ; hence the strong limits at the two infinities are and .
The spectral projections reduce , the eigenspace at is exactly , and for self-adjoint the family is increasing, strongly right continuous, with strong limits and at the two infinities.
Depends on
- Borel functional calculus for bounded normal operators
- Borel functional calculus for a bounded normal operator
- The bounded complex dual of C_0(X) is regular complex measures
- Continuous functional calculus properties
- Spectrum of a self adjoint operator is real
- Self adjoint norm and spectrum extrema
- Projection valued measure
- Scalar and complex measures from a pvm
- Self-adjoint, positive, unitary and normal operators
- Hilbert-adjoint identities
- Spectrum and resolvent of a bounded operator
- The Axiom of Choice
Used by
Dependency tree · two levels
60 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
- Theo Bühler and Dietmar Salamon, Functional Analysis, Theorem 5.81, printed pp.293–296 (standard reference, not scraped)
- Gerald Teschl, Mathematical Methods in Quantum Mechanics, 2nd ed., §4.1 and §6.3, printed pp.113–115 and 173–177 (standard reference, not scraped)