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.
Bounded borel pvm integral
Statement
Assume Countable Choice. Let be a measurable space, let be a nonzero complex Hilbert space, let be a projection valued measure on , and let be bounded and -measurable (A measurable function between measurable spaces). Then:
- there is a unique operator with and for every sequence of complex simple functions with one has : the integral is obtained from uniform simple approximations and is independent of the approximating sequence;
- , and for every
- the exact norm is the -essential supremum where denotes the essential supremum of the real measurable function with respect to the finite measure (The essential supremum of a measurable function with respect to a measure).
Facts & Assumptions
For a complex simple function the operator satisfies , and ; the construction is linear on simple functions presented over a common refinement (Simple pvm integral is representation independent).
is a finite complex measure on with , the integral of a bounded measurable satisfies (Scalar and complex measures from a pvm, Integrals against signed or complex measures are bounded by total variation, Integration against a signed or complex measure, and the class L^1(nu) = L^1(|nu|)).
is a positive measure with . Moreover, if , then , so (Scalar and complex measures from a pvm, Projection valued measure).
is complete for the operator norm (If (Y) is Banach then (\mathcal B(X,Y)) is Banach, Hilbert space).
A bounded measurable complex function is integrable against every finite measure and dominated convergence holds: if pointwise and with integrable, then (Dominated convergence).
For a finite measure , is the least essential bound of : -almost everywhere, and if almost everywhere then ; if then (The essential supremum is attained as the least essential bound, The essential supremum of a measurable function with respect to a measure).
A complex simple function is a finite linear combination of indicators of pairwise disjoint measurable sets; for a measurable and the square containing the range of a bounded can be cut into finitely many Borel squares of diameter whose inverse images refine to a disjoint measurable cover of (Complex simple functions as finite sums of measurable indicators, A measurable function between measurable spaces).
Countable Choice is the declared standing hypothesis of this block of the page (The Axiom of Countable Choice ()).
Proof
Given: A measurable space , a nonzero complex Hilbert space , a projection valued measure on , and a bounded measurable with .
Uniform simple approximation: for each choose finitely many pairwise disjoint measurable sets covering and complex numbers with on (cut a square containing the range of into finitely many squares of diameter and take inverse images), so is a complex simple function with .
Difference of simple integrals: if are complex simple functions, presenting both over the common refinement of their disjoint normal forms gives , hence ; in particular the sequence is Cauchy, since .
By completeness of the sequence has a norm limit , and for any other uniformly approximating sequence one has , so the limit does not depend on the sequence; the same argument applies to the difference of two candidate limits.
Pairing identity: for all , , because .
Norm identities: by dominated convergence applied to the finite measure with the constant dominating function , since and ; taking in the pairing identity gives .
Norm bound and uniqueness: by the pairing identity just proved and the variation bound, so ; and any operator with for all equals , since has all pairings zero, whence for every by positive definiteness of the pairing.
Upper bound for the norm: for one has and hence , so by the least-essential-bound property; therefore .
Lower bound for the norm: write . If , the lower bound follows from nonnegativity of the operator norm. If , given choose a unit vector with , so satisfies by the least-essential-bound property; put , so and hence , giving ; since was arbitrary, .
The integral is well defined, obtained from uniform simple approximations, satisfies the pairing and quadratic identities and the bound , and its exact norm is the -essential supremum .
Depends on
- Simple pvm integral is representation independent
- Scalar and complex measures from a pvm
- Projection valued measure
- Hilbert space
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- If \(Y\) is Banach then \(\mathcal B(X,Y)\) is Banach
- Integrals against signed or complex measures are bounded by total variation
- Dominated convergence
- The essential supremum of a measurable function with respect to a measure
- The essential supremum is attained as the least essential bound
- A measurable function between measurable spaces
- Integration against a signed or complex measure, and the class L^1(nu) = L^1(|nu|)
- Complex simple functions as finite sums of measurable indicators
Used by
- Borel functional calculus for a bounded normal operator Definition
- Integral of a measurable function against a projection-valued measure Definition
- Relative compactness with respect to an operator Definition
- Multiplication operators: domain, spectral measure and spectrum Example
- Pvm of a diagonal normal operator Example
- Pvm of a multiplication operator Example
- Spectral projection of an isolated eigenvalue agrees with the riesz projection Example
- Continuous functional calculus produces a regular PVM Lemma
- The unbounded PVM integral is densely defined, closed and normal Lemma
- Borel functional calculus for bounded normal operators Theorem
- Canonical decomposition into pure point, absolutely continuous and singular continuous parts Theorem
- Continuous functional calculus under resolvent convergence Theorem
- Cyclic spectral representation Theorem
- Kato-Rellich theorem Theorem
- Pvm integral is a star homomorphism Theorem
- Spectral theorem for bounded normal operators pvm form Theorem
- Spectral theorem for unbounded self-adjoint operators (PVM form) Theorem
- Stone resolvent formula for spectral projections Theorem
- Unbounded Borel functional calculus: domains, products, spectral mapping Theorem
Dependency tree · two levels
55 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.73, printed pp.279–283 (standard reference, not scraped)
- Dana P. Williams, Lecture Notes on the Spectral Theorem, Lemma 5.3 and Proposition 5.3, pp.16–18 (standard reference, not scraped)