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.1A2A3A4A8

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.

2.1step 1.1A1A2algebra

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.

3.1step 1.1step 2.1A1A3A4A5algebra

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.

3.2step 1.1step 2.1A1A2A3A4A5algebra

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.

4.1step 1.1step 3.2A2A3A7algebra

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.

5.1step 2.1step 3.1step 3.2step 4.1A6∎

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.

Simple pvm integral is representation independent

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources