LemmaStatement: 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.

Simple pvm integral is representation independent

Statement

Assume Countable Choice. Let $(X, Σ)$ be a measurable space, let $H$ be a complex Hilbert space, let $E$ be a projection valued measure on $(X, Σ)$ , and let $s : X \to C$ be a complex simple function. Then:

the operator $\int s d E$ of Integral of a simple function against a pvm is independent of the disjoint normal form of $s$ ;
for all $x, y \in H$ , $⟨ (\int s d E) x, y ⟩ = \int s d E_{x, y}$ , the scalar integral against the complex measure $E_{x, y}$ ;
for every $x \in H$ , $∥ (\int s d E) x ∥^{2} = \int ∣ s ∣^{2} d E_{x}$ , and $∥ \int s d E ∥ \leq M_{s}$ .

Here $M_{s} : = \max ({0} \cup {∣ s (t) ∣ : t \in X})$ ; thus $M_{s} = \max_{t \in X} ∣ s (t) ∣$ when $X \neq \emptyset$ , and $M_{s} = 0$ when $X = \emptyset$ .

Facts & Assumptions

[A1]

For a disjoint normal form $s = \sum_{j = 1}^{m} a_{j} 1_{B_{j}}$ with $B_{1}, \dots, B_{m}$ pairwise disjoint and covering $X$ , the integral is $\int s d E = \sum_{j} a_{j} E (B_{j})$ (Integral of a simple function against a pvm).

[A2]

$E (\emptyset) = 0$ , $E (X) = I$ , $E (B \cap C) = E (B) E (C)$ , each $E (B)$ satisfies $E (B)^{2} = E (B) = E (B)^{*}$ and is contractive, and for pairwise disjoint $(D_{n})$ with union $D$ one has $E (D) x = \sum_{n} E (D_{n}) x$ in norm (Projection valued measure).

[A3]

$E_{x, y} (B) = ⟨ E (B) x, y ⟩$ is a finite complex measure, $E_{x} (B) = ⟨ E (B) x, x ⟩ = ∥ E (B) x ∥^{2}$ is a positive measure of mass $∥ x ∥^{2}$ , $∣ E_{x, y} ∣ (X) \leq ∥ x ∥ ∥ y ∥$ , and $E_{y, x} = \overline{E_{x, y}}$ (Scalar and complex measures from a pvm).

[A4]

For a complex measure $ν$ and a complex simple function whose nonzero level sets have finite total variation, presented over the nonzero level sets, the scalar simple integral is $\int s d ν = \sum_{j} c_{j} ν (E_{j})$ , and the value is unchanged by deleting empty level sets (The simple integral against a signed or complex measure, Complex simple functions as finite sums of measurable indicators).

[A5]

The pairing is linear in the first argument and conjugate-linear in the second, so $⟨ \sum_{j} z_{j}, y ⟩ = \sum_{j} ⟨ z_{j}, y ⟩$ and $⟨ z, w ⟩ = \overline{⟨ w, z ⟩}$ (Real and complex inner-product spaces and their induced length). The adjoint identity is $⟨ P u, v ⟩ = ⟨ u, P^{*} v ⟩$ (The Hilbert-space adjoint of a bounded operator).

[A6]

Countable Choice is the declared standing hypothesis of this block of the page (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[A7]

The operator norm is the unit-ball supremum (The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

[A8]

Total variation is the supremum of the nonnegative sums over countable measurable partitions (The total variation |nu|(E) from countable measurable partitions).

Proof

technique · direct

Given: A measurable space $(X, Σ)$ , a complex Hilbert space $H$ , a projection valued measure $E$ , a complex simple function $s$ with two disjoint normal forms $s = \sum_{j = 1}^{m} a_{j} 1_{B_{j}} = \sum_{k = 1}^{n} b_{k} 1_{C_{k}}$ covering $X$ , and vectors $x, y \in H$ .

1.1

Finite additivity follows by padding a finite disjoint family with empty sets in strong countable additivity. The scalar measures also have finite additivity. Every measurable subset has finite $∣ E_{x, y} ∣$ -variation: a countable partition of that subset extends to one of $X$ by adding its complement, so its sum is at most $∣ E_{x, y} ∣ (X) \leq ∥ x ∥ ∥ y ∥$ . In particular the scalar simple integrals below are defined; for $E_{x} = E_{x, x}$ the same argument applies.

A2A3A4A8

2.1

The intersections $B_{j} \cap C_{k}$ form a disjoint cover of $X$ . If an intersection is nonempty then $a_{j} = b_{k}$ , and if empty its projection value is zero. Finite additivity therefore gives $\sum_{j} a_{j} E (B_{j}) = \sum_{j, k} a_{j} E (B_{j} \cap C_{k}) = \sum_{j, k} b_{k} E (B_{j} \cap C_{k}) = \sum_{k} b_{k} E (C_{k})$ . This proves representation independence.

step 1.1A1A2algebra

3.1

Expanding the pairing gives $⟨ (\int s d E) x, y ⟩ = \sum_{j} a_{j} E_{x, y} (B_{j})$ . Discard empty cells and regroup the remaining indices by $c \in s (X)$ . Finite additivity gives $\sum_{j} a_{j} E_{x, y} (B_{j}) = \sum_{c \in s (X)} c E_{x, y} (s^{- 1} ({c})) = \int s d E_{x, y}$ , where the zero-value term is zero. If $X$ is empty all cells and sums contribute zero.

step 1.1step 2.1A1A3A4A5algebra

3.2

The adjoint identity and the projection rules give $⟨ E (B_{j}) x, E (B_{k}) x ⟩ = ⟨ E (B_{k})^{*} E (B_{j}) x, x ⟩ = ⟨ E (B_{k} \cap B_{j}) x, x ⟩$ . Thus expansion of the squared norm leaves only diagonal terms: $∥ (\int s d E) x ∥^{2} = \sum_{j} ∣ a_{j} ∣^{2} E_{x} (B_{j})$ . Regrouping the nonempty cells by the value $d = ∣ a_{j} ∣^{2}$ , finite additivity identifies this sum with $\sum_{d \in ∣ s ∣^{2} (X)} d E_{x} ((∣ s ∣^{2})^{- 1} ({d})) = \int ∣ s ∣^{2} d E_{x}$ ; the zero term vanishes.

step 1.1step 2.1A1A2A3A4A5algebra

4.1

Empty cells contribute zero to the sum in step 3.2. On every nonempty $B_{j}$ , $∣ a_{j} ∣ \leq M_{s}$ because $a_{j}$ is a value of $s$ . Positivity and finite additivity give $∥ (\int s d E) x ∥^{2} \leq M_{s}^{2} \sum_{j} E_{x} (B_{j}) = M_{s}^{2} ∥ x ∥^{2}$ . Taking nonnegative square roots and then the unit-ball supremum gives $∥ \int s d E ∥ \leq M_{s}$ . When $X = \emptyset$ , all projection values are zero and the integral is zero, so the same bound with $M_{s} = 0$ holds.

step 1.1step 3.2A2A3A7algebra

5.1

The integral is independent of the presentation, has the asserted scalar pairings and squared-norm identity, and satisfies the stated bound, including the empty-space case.

step 2.1step 3.1step 3.2step 4.1A6∎

Depends on

Used by

Bounded borel pvm integral Theorem
Pvm integral is a star homomorphism Theorem

Dependency tree · two levels

38 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, §5.6.2 and Lemma 5.77, printed pp.277–281 (standard reference, not scraped)
Dana P. Williams, Lecture Notes on the Spectral Theorem, Proposition 5.3, pp.17–18 (standard reference, not scraped)