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.
Borel functional calculus for a bounded normal operator
Definition
Assume AC. Let be a bounded normal operator on a nonzero complex Hilbert space and let be its spectral projection valued measure on the Borel -algebra of , the unique regular projection valued measure with (Spectral theorem for bounded normal operators pvm form). For a bounded Borel function , that is a bounded -measurable function on the Borel -algebra of (A measurable function between measurable spaces), define the Borel functional calculus of at by
the bounded Borel integral of against from Bounded borel pvm integral. The map from bounded Borel functions on to is the bounded Borel functional calculus of .
Well-definedness and consistency. The operator is well defined because the spectral projection valued measure of is unique: if were another regular projection valued measure with , then . The construction agrees with the continuous calculus on continuous functions, for , by the displayed clause of the spectral theorem. It inherits the algebraic behaviour of the projection valued measure integral: is complex-linear in , unital with , multiplicative, star-preserving with , norm bounded by , strongly continuous for bounded Borel when pointwise -almost everywhere and , as supplied by Pvm integral is a star homomorphism. In particular for every Borel set , and the norm of is the -essential supremum of (Bounded borel pvm integral).
Commutation. Every bounded commuting with and commutes with every . Write for the continuous calculus. The construction in Continuous functional calculus produces a regular PVM provides finite regular complex measures with and for continuous ; its PVM is the present by uniqueness. The continuous commutant property (Continuous functional calculus properties) and the defining adjoint identity (The Hilbert-space adjoint of a bounded operator) give Uniqueness of the finite regular complex representing measure on the compact spectrum, where , gives (The bounded complex dual of C_0(X) is regular complex measures). For bounded Borel , the bounded-integral pairing identity therefore yields Testing the difference against itself proves . These properties are collected in Borel functional calculus for bounded normal operators.
Depends on
- Continuous functional calculus produces a regular PVM
- Continuous functional calculus properties
- The bounded complex dual of C_0(X) is regular complex measures
- The Hilbert-space adjoint of a bounded operator
- Spectral theorem for bounded normal operators pvm form
- Bounded borel pvm integral
- Pvm integral is a star homomorphism
- A measurable function between measurable spaces
- Projection valued measure
- The Axiom of Choice
Used by
- Spectral projections and resolution of the identity Corollary
- A normal operator need not have any eigenvectors Counterexample
- Continuous functional calculus cannot produce every spectral projection Counterexample
- Borel functional calculus defines a discontinuous characteristic function Example
- Pvm of a diagonal normal operator Example
- Pvm of a multiplication operator Example
- Sign and positive negative parts of a self adjoint operator Example
- Spectral projection of an isolated eigenvalue agrees with the riesz projection Example
- Borel functional calculus for bounded normal operators Theorem
- Cyclic spectral representation Theorem
- Stone resolvent formula for spectral projections Theorem
Dependency tree · two levels
62 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, Definition 5.75, printed pp.291–293 (standard reference, not scraped)
- Dana P. Williams, Lecture Notes on the Spectral Theorem, Theorem 5.6, pp.17–20 (standard reference, not scraped)