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.

Scalar and complex measures from a pvm

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 for $x, y \in H$ define

$E_{x} (B) : = ⟨ E (B) x, x ⟩, E_{x, y} (B) : = ⟨ E (B) x, y ⟩ (B \in Σ) .$

Then:

$E_{x}$ is a positive measure on $(X, Σ)$ with $E_{x} (X) = ∥ x ∥^{2}$ and $0 \leq E_{x} (B) \leq ∥ x ∥^{2}$ for every $B$ ;
$E_{x, y}$ is a finite complex measure on $(X, Σ)$ , the map $(x, y) \mapsto E_{x, y}$ is linear in $x$ and conjugate-linear in $y$ , and $E_{y, x} = \overline{E_{x, y}}$ , meaning $E_{y, x} (B) = \overline{E_{x, y} (B)}$ for every $B$ ;
$∣ E_{x, y} ∣ (X) \leq ∥ x ∥ ∥ y ∥$ , so $∣ E_{x, y} (B) ∣ \leq ∥ x ∥ ∥ y ∥$ for every $B$ , and the polarization identity $E_{x, y} = \frac{1}{4} \sum_{k = 0}^{3} i^{k} E_{x + i^{k} y}$ holds as an identity of complex measures, where $i^{k}$ are the fourth roots of unity $1, i, - 1, - i$ .

Facts & Assumptions

[A1]

Projection values satisfy $P^{2} = P = P^{*}$ , $⟨ P x, x ⟩ = ∥ P x ∥^{2} \geq 0$ and $∥ P x ∥ \leq ∥ x ∥$ (Projection valued measure, Hilbert projections are linear, self-adjoint and contractive).

[A2]

$E (\emptyset) = 0$ , $E (X) = I$ , $E (B \cap C) = E (B) E (C)$ , and for every pairwise disjoint sequence $(B_{n})$ with union $B$ one has $E (B) x = \lim_{N} \sum_{n \leq N} E (B_{n}) x$ in norm (Projection valued measure).

[A3]

$⟨ S u, v ⟩ = ⟨ u, S^{*} v ⟩$ for all $u, v$ , and for self-adjoint $S$ one has $⟨ S u, v ⟩ = ⟨ u, S v ⟩$ and $⟨ S u, v ⟩ = \overline{⟨ S v, u ⟩}$ (The Hilbert-space adjoint of a bounded operator, Real and complex inner-product spaces and their induced length).

[A4]

Cauchy–Schwarz gives $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ (Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs).

[A5]

A measure is a $[0, + \infty]$ -valued countably additive set function vanishing at $\emptyset$ (Measures on sigma-algebras); a complex measure is a $C$ -valued countably additive set function vanishing at $\emptyset$ (A complex measure is a finite-valued countably additive set function); its total variation is the supremum of $\sum_{n} ∣ ν (E_{n}) ∣$ over countable measurable partitions (The total variation |nu|(E) from countable measurable partitions).

[A6]

The pairing is linear in the first argument, conjugate-linear in the second, and $∥ u ∥^{2} = ⟨ u, u ⟩$ (Real and complex inner-product spaces and their induced length).

[A7]

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

Proof

technique · direct

Given: A measurable space $(X, Σ)$ , a complex Hilbert space $H$ , a projection valued measure $E$ on it, vectors $x, y \in H$ , and a pairwise disjoint sequence $(B_{n}) \subseteq Σ$ with union $B$ .

1.1

$E_{x}$ is countably additive and vanishes at $\emptyset$ : using strong additivity, $E_{x} (B) = ⟨ \lim_{N} \sum_{n \leq N} E (B_{n}) x, x ⟩ = \lim_{N} \sum_{n \leq N} ⟨ E (B_{n}) x, x ⟩ = \sum_{n} E_{x} (B_{n})$ , with the limit pulled through the linear functional $⟨ \cdot, x ⟩$ , continuous since $∣ ⟨ v, x ⟩ - ⟨ w, x ⟩ ∣ \leq ∥ v - w ∥ ∥ x ∥$ , while $E_{x} (\emptyset) = ⟨ 0, x ⟩ = 0$ and $E_{x} (X) = ⟨ x, x ⟩ = ∥ x ∥^{2}$ .

A2A4A6

1.2

$E_{x, y}$ is a finite complex measure and the map is linear in $x$ and conjugate-linear in $y$ : countable additivity holds by the same limit argument with the continuous functional $⟨ \cdot, y ⟩$ , $E_{x, y} (\emptyset) = 0$ , and $⟨ E (B) (x + u), y ⟩ = ⟨ E (B) x, y ⟩ + ⟨ E (B) u, y ⟩$ , $⟨ E (B) (λ x), y ⟩ = λ ⟨ E (B) x, y ⟩$ , $⟨ E (B) x, λ y ⟩ = \overline{λ} ⟨ E (B) x, y ⟩$ ; finiteness follows from $∣ E_{x, y} (B) ∣ = ∣ ⟨ E (B) x, y ⟩ ∣ \leq ∥ E (B) x ∥ ∥ y ∥ \leq ∥ x ∥ ∥ y ∥$ .

A1A2A3A4A5A6

1.3

Conjugate symmetry: $\overline{E_{x, y} (B)} = \overline{⟨ E (B) x, y ⟩} = ⟨ y, E (B) x ⟩ = ⟨ E (B) y, x ⟩ = E_{y, x} (B)$ , using that $E (B)$ is self-adjoint.

A1A3A6

1.4

Polarization: for fixed $B$ the form $Λ (u, v) : = ⟨ E (B) u, v ⟩$ is sesquilinear, so expanding the four terms gives $\frac{1}{4} \sum_{k = 0}^{3} i^{k} Λ (u + i^{k} v, u + i^{k} v) = Λ (u, v)$ for all $u, v$ (the $∣ u ∣^{2}$ and $∣ v ∣^{2}$ coefficients cancel and the mixed terms add to $4 Λ (u, v)$ ); reading the identity at $B$ and letting $B$ vary gives $E_{x, y} = \frac{1}{4} \sum_{k = 0}^{3} i^{k} E_{x + i^{k} y}$ .

A6algebra

2.1

$E_{x}$ is nonnegative and bounded by its total mass: $E_{x} (B) = ⟨ E (B) x, E (B) x ⟩ = ∥ E (B) x ∥^{2} \geq 0$ and $∥ E (B) x ∥ \leq ∥ x ∥$ , so $0 \leq E_{x} (B) \leq ∥ x ∥^{2}$ ; hence $E_{x}$ is a positive measure with $E_{x} (X) = ∥ x ∥^{2}$ .

step 1.1A1A5A6

3.1

Variation bound: let $(B_{j})_{j \geq 0}$ be a countable measurable partition of $X$ . For every $N$ , Cauchy--Schwarz gives $\sum_{j = 0}^{N} ∣ E_{x, y} (B_{j}) ∣ = \sum_{j = 0}^{N} ∣ ⟨ E (B_{j}) x, E (B_{j}) y ⟩ ∣ \leq (\sum_{j = 0}^{N} ∥ E (B_{j}) x ∥^{2})^{1 / 2} (\sum_{j = 0}^{N} ∥ E (B_{j}) y ∥^{2})^{1 / 2} \leq ∥ x ∥ ∥ y ∥$ . Indeed, orthogonality and strong additivity give $\sum_{j \geq 0} ∥ E (B_{j}) x ∥^{2} = \sum_{j \geq 0} ⟨ E (B_{j}) x, x ⟩ = E_{x} (X) = ∥ x ∥^{2}$ , because $E (B_{j})^{2} = E (B_{j}) = E (B_{j})^{*}$ and the $B_{j}$ partition $X$ ; the same holds with $y$ . Taking $N \to \infty$ yields $\sum_{j \geq 0} ∣ E_{x, y} (B_{j}) ∣ \leq ∥ x ∥ ∥ y ∥$ .

step 1.1step 2.1A1A2A3A4A5algebra

4.1

Hence every countable partition contributes at most $∥ x ∥ ∥ y ∥$ to the defining supremum of $∣ E_{x, y} ∣ (X)$ , so $∣ E_{x, y} ∣ (X) \leq ∥ x ∥ ∥ y ∥$ and $∣ E_{x, y} (B) ∣ \leq ∣ E_{x, y} ∣ (X) \leq ∥ x ∥ ∥ y ∥$ for every $B$ , since $(B, X ∖ B, \emptyset, \dots)$ is one of those countable partitions.

step 3.1A5

5.1

All asserted properties of $E_{x}$ , $E_{x, y}$ hold for arbitrary $x, y$ , so the scalar pairings of a projection valued measure are a positive measure of mass $∥ x ∥^{2}$ and a family of finite complex measures of variation at most $∥ x ∥ ∥ y ∥$ , conjugate symmetric and recovered by polarization.

step 1.1step 2.1step 1.2step 1.3step 4.1step 1.4A7∎

Depends on

Used by

Spectral projections and resolution of the identity Corollary
Unitary groups converge under strong resolvent convergence Corollary
Integral of a measurable function against a projection-valued measure Definition
Spectral multiplicity function in the separable case Definition
Pvm of a diagonal normal operator Example
Pvm of a multiplication operator Example
Simple pvm integral is representation independent Lemma
The unbounded PVM integral is densely defined, closed and normal Lemma
Bounded borel pvm integral Theorem
Continuous functional calculus under resolvent convergence Theorem
Cyclic spectral representation Theorem
Multiplication operator form of the bounded normal spectral theorem Theorem
Pvm integral is a star homomorphism Theorem
Support and uniqueness of the spectral measure Theorem
Unbounded Borel functional calculus: domains, products, spectral mapping Theorem

Dependency tree · two levels

42 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, Lemma 5.76, printed pp.276–277 (standard reference, not scraped)
Dana P. Williams, Lecture Notes on the Spectral Theorem, Definition 5.1 and Proposition 5.3, pp.15–18 (standard reference, not scraped)