Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 2026-09-22
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 (X,Σ) be a measurable space, let H be a nonzero complex Hilbert space, let E be a projection valued measure on (X,Σ), and let f:XC be bounded and Σ-measurable (A measurable function between measurable spaces). Then:

  1. there is a unique operator ΦE(f)B(H) with ΦE(f)x,y=fdEx,y(x,yH), and for every sequence (sn) of complex simple functions with fsn0 one has ΦE(f)sndE0: the integral is obtained from uniform simple approximations and is independent of the approximating sequence;
  2. ΦE(f)f, and for every xH ΦE(f)x,x=fdEx,ΦE(f)x2=f2dEx;
  3. the exact norm is the E-essential supremum fE,:=sup{f,Ex: xH, x=1},ΦE(f)=fE,, where f,Ex denotes the essential supremum of the real measurable function f with respect to the finite measure Ex (The essential supremum of a measurable function with respect to a measure).

Facts & Assumptions

[A1]

For a complex simple function s the operator sdE satisfies (sdE)x,y=sdEx,y, (sdE)x2=s2dEx and sdEmaxss; the construction is linear on simple functions presented over a common refinement (Simple pvm integral is representation independent).

[A2]

Ex,y is a finite complex measure on (X,Σ) with Ex,y(X)xy, the integral gdEx,y of a bounded measurable g satisfies gdEx,ygEx,y(X) (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|)).

[A3]

Ex(B)=E(B)x,x=E(B)x2 is a positive measure with Ex(X)=x2. Moreover, if E(A)y=y, then E(XA)y=E(XA)E(A)y=E()y=0, so Ey(XA)=0 (Scalar and complex measures from a pvm, Projection valued measure).

[A4]

B(H) is complete for the operator norm (If (Y) is Banach then (\mathcal B(X,Y)) is Banach, Hilbert space).

[A5]

A bounded measurable complex function is integrable against every finite measure and dominated convergence holds: if gng pointwise and gnC with C integrable, then gndμgdμ (Dominated convergence).

[A6]

For a finite measure μ, g,μ is the least essential bound of g: gg,μ μ-almost everywhere, and if gM almost everywhere then g,μM; if g,μ>c then μ({g>c})>0 (The essential supremum is attained as the least essential bound, The essential supremum of a measurable function with respect to a measure).

[A7]

A complex simple function is a finite linear combination of indicators of pairwise disjoint measurable sets; for a measurable f and ε>0 the square [M,M]2 containing the range of a bounded f can be cut into finitely many Borel squares of diameter <ε whose inverse images refine to a disjoint measurable cover of X (Complex simple functions as finite sums of measurable indicators, A measurable function between measurable spaces).

[A8]

Countable Choice is the declared standing hypothesis of this block of the page (The Axiom of Countable Choice (ACω)).

Proof

technique · direct

Given: A measurable space (X,Σ), a nonzero complex Hilbert space H, a projection valued measure E on (X,Σ), and a bounded measurable f:XC with M:=f<+.

1.1

Uniform simple approximation: for each n0 choose finitely many pairwise disjoint measurable sets D1,,Dr covering X and complex numbers ci with fci1/(n+1) on Di (cut a square containing the range of f into finitely many squares of diameter <1/(n+1) and take inverse images), so sn:=ici1Di is a complex simple function with fsn1/(n+1).

A7
1.2

Difference of simple integrals: if s,t are complex simple functions, presenting both over the common refinement of their disjoint normal forms gives (st)dE=sdEtdE, hence sdEtdEst; in particular the sequence sndE is Cauchy, since sndEsmdEsnsm1n+1+1m+1.

A1
2.1

By completeness of B(H) the sequence sndE has a norm limit ΦE(f), and for any other uniformly approximating sequence (tn) one has sndEtndEsntn0, so the limit does not depend on the sequence; the same argument applies to the difference of two candidate limits.

step 1.2A4
3.1

Pairing identity: for all x,yH, ΦE(f)x,y=limn(sndE)x,y=limnsndEx,y=fdEx,y, because (snf)dEx,ysnfEx,y(X)1n+1xy0.

step 2.1A1A2
4.1

Norm identities: ΦE(f)x2=limn(sndE)x2=limnsn2dEx=f2dEx by dominated convergence applied to the finite measure Ex with the constant dominating function (M+1)2, since snf and snM+1; taking y=x in the pairing identity gives ΦE(f)x,x=fdEx.

step 1.1step 2.1step 3.1A1A3A5
4.2

Norm bound and uniqueness: ΦE(f)x,yfxy by the pairing identity just proved and the variation bound, so ΦE(f)f; and any operator T with Tx,y=fdEx,y for all x,y equals ΦE(f), since TΦE(f) has all pairings zero, whence (TΦE(f))x=0 for every x by positive definiteness of the pairing.

step 3.1A2
5.1

Upper bound for the norm: for x0 one has Ex=x2Ex/x and hence f,Ex=f,Ex/x, so ΦE(f)x2=f2dExf,Ex2x2fE,2x2 by the least-essential-bound property; therefore ΦE(f)fE,.

step 4.1A3A6
5.2

Lower bound for the norm: write a=fE,. If a=0, the lower bound follows from nonnegativity of the operator norm. If a>0, given 0c<a choose a unit vector x with f,Ex>c, so A:={f>c} satisfies Ex(A)>0 by the least-essential-bound property; put y:=E(A)x0, so Ey(XA)=0 and hence ΦE(f)y2=f2dEyc2Ey(X)=c2y2, giving ΦE(f)c; since 0c<a was arbitrary, ΦE(f)fE,.

step 4.1A3A6
6.1

The integral ΦE(f) is well defined, obtained from uniform simple approximations, satisfies the pairing and quadratic identities and the bound ΦE(f)f, and its exact norm is the E-essential supremum fE,.

step 2.1step 3.1step 4.1step 4.2step 5.1step 5.2A8

Depends on

Used by

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