Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablePipeline-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.

Integral of a measurable function against a projection-valued measure

Definition

Assume Countable Choice. Let E be a projection valued measure on the measurable space (X,Σ) acting on the complex Hilbert space H (Projection valued measure), and let f:XC be Σ-measurable. Put D(f(E)):={xH:Xf2dEx<},Ex(B)=E(B)x,x, where the scalar measures Ex are those of Scalar and complex measures from a pvm, and for xD(f(E)) set f(E)x:=limnΦE(f1{fn})x, For H{0}, the bounded integrals ΦE are those of Bounded borel pvm integral, and the limit is taken in the norm of H. For H={0}, define ΦE(g) to be the unique operator on H for every bounded measurable g. Then E0 is the zero measure, D(f(E))=H, and f(E)0=0. Thus this case is defined directly without applying a theorem requiring a nonzero space.

Well-definedness. D(f(E)) is a linear subspace: the estimate Ex+y2Ex+2Ey for scalar measures and Eαx=α2Ex follow from E(B)(x+y)22E(B)x2+2E(B)y2 and E(B)αx2=α2E(B)x2. Writing fn:=f1{fn} the sets {fn} are measurable, so fn is bounded and measurable. For m,nN, fnfm2f21{f>N}. The integral of the right side against Ex tends to zero by Dominated convergence, with the integrable majorant f2 and pointwise limit zero since f is finite-valued. Linearity of the bounded calculus (Pvm integral is a star homomorphism) and its quadratic identity give ΦE(fn)xΦE(fm)x2=fnfm2dEx. 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 x 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 f,g agree outside a measurable set N with E(N)=0, then Ex(N)=E(N)x2=0 for every x. Thus the integrals of f2 and g2 agree, so their domains agree. At every truncation level their bounded truncations agree outside N; the quadratic identity applied to the difference gives equal truncation vectors for every x. Taking limits gives f(E)x=g(E)x on their common domain.

Depends on

Used by

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