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.
Projection valued measure
Definition
Assume Countable Choice. Let be a measurable space (Measurable spaces and measurable sets, Sigma-algebras) and let be a complex Hilbert space (Hilbert space). A projection valued measure (PVM) on is a map
such that:
- is an orthogonal projection for every , that is, a bounded operator with ; there is no finite-dimensional restriction;
- and ;
- for all ;
- for every pairwise disjoint sequence in with union and every , the series converges in norm to , that is
Clause 4 is strong countable additivity. A PVM is called regular when is a locally compact Hausdorff space (Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space), the -algebra is the Borel -algebra, and every one of the finite positive measures
is a regular Borel measure (Regular Borel measure on an LCH space). Inner products are linear in the first variable and conjugate-linear in the second (Real and complex inner-product spaces and their induced length); this fixed convention is the one used for every pairing on this page.
Well-definedness: the projection clause. The conditions are simultaneously meaningful and describe exactly the Hilbert orthogonal projections, with no hidden finite-dimensional hypothesis. Indeed, for a bounded with the range is a linear subspace, and for one has , so ; conversely for , so , while for gives (Hilbert-adjoint identities, Real and complex inner-product spaces and their induced length). Hence is closed, and the two defining properties , of The Hilbert orthogonal projection onto a closed subspace show that is the Hilbert orthogonal projection onto a closed subspace, and conversely every such is idempotent and self-adjoint by Hilbert projections are linear, self-adjoint and contractive and Orthogonal decomposition by a closed subspace. Finally is contractive: from and Cauchy–Schwarz, , so for all , and is a nonnegative real number.
Well-definedness: the regularity clause. For an orthogonal projection value the pairing is a nonnegative real number and , so every is a finite nonnegative set function and the regularity requirement is a meaningful condition on it; that each is genuinely a countably additive measure of total mass , and that the polarized pairings are finite complex measures, is proved as Scalar and complex measures from a pvm before either is used.
Depends on
Hilbert space
Measurable spaces and measurable sets
Sigma-algebras
Real and complex inner-product spaces and their induced length
Hilbert-adjoint identities
The Hilbert orthogonal projection onto a closed subspace
Hilbert projections are linear, self-adjoint and contractive
Orthogonal decomposition by a closed subspace
Regular Borel measure on an LCH space
Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space
The Axiom of Countable Choice ()