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.
Integral of a measurable function against a projection-valued measure
Definition
Assume Countable Choice. Let be a projection valued measure on the measurable space acting on the complex Hilbert space (Projection valued measure), and let be -measurable. Put where the scalar measures are those of Scalar and complex measures from a pvm, and for set For , the bounded integrals are those of Bounded borel pvm integral, and the limit is taken in the norm of . For , define to be the unique operator on for every bounded measurable . Then is the zero measure, , and . Thus this case is defined directly without applying a theorem requiring a nonzero space.
Well-definedness. is a linear subspace: the estimate for scalar measures and follow from and . Writing the sets are measurable, so is bounded and measurable. For , The integral of the right side against tends to zero by Dominated convergence, with the integrable majorant and pointwise limit zero since is finite-valued. Linearity of the bounded calculus (Pvm integral is a star homomorphism) and its quadratic identity give These clauses hold directly on the zero space as well. Hence the truncation vectors are Cauchy and converge uniquely by Hilbert-space completeness (Hilbert space). The limit is linear in because every truncation operator is linear and addition and scalar multiplication are norm-continuous. Countable Choice is inherited from the bounded PVM suppliers; no further choice is needed to take these specified limits.
Finally, if two -measurable functions agree outside a measurable set with , then for every . Thus the integrals of and agree, so their domains agree. At every truncation level their bounded truncations agree outside ; the quadratic identity applied to the difference gives equal truncation vectors for every . Taking limits gives on their common domain.
Depends on
Used by
- Unitary groups converge under strong resolvent convergence Corollary
- Pure point, absolutely continuous and singular continuous spectral subspaces Definition
- Multiplication operators: domain, spectral measure and spectrum Example
- A self-adjoint operator generates a strongly continuous unitary group Lemma
- Spectral form domain and core of a semibounded operator Lemma
- The unbounded PVM integral is densely defined, closed and normal Lemma
- Canonical decomposition into pure point, absolutely continuous and singular continuous parts Theorem
- Spectral theorem for unbounded self-adjoint operators (PVM form) Theorem
- Unbounded Borel functional calculus: domains, products, spectral mapping Theorem
Dependency tree · two levels
50 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, second edition (standard reference, not scraped)
- Theo Buehler and Dietmar A. Salamon, Functional Analysis (standard reference, not scraped)