LemmaStatement: AI-adaptedProof: AI-adaptedprecheck pass

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.

Local PVM extension: tensoring a projection-valued measure with the identity

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H, K$ be nonzero complex Hilbert spaces (Hilbert space) and let $H \hat{\otimes} K$ be their completed tensor product with inclusion $κ$ (Hilbert tensor construction: inner product, completion and product bases). Let $(X, Σ)$ be a measurable space (Measurable spaces and measurable sets) and let $E$ be a projection valued measure on $(X, Σ)$ acting on $H$ (Projection valued measure). Define, for $B \in Σ$ , $F (B) : = E (B) \otimes I_{K} \in B (H \hat{\otimes} K),$ the bounded tensor operator of Bounded tensor maps: extension, norm estimate, adjoint and commutation clause (a). Then:

(a) $F$ is a projection valued measure on $(X, Σ)$ acting on $H \hat{\otimes} K$ ;

(b) for every bounded $Σ$ -measurable function $f : X \to C$ , writing $Φ_{F} (f) = \int f d F$ and $Φ_{E} (f) = \int f d E$ for the integrals of Bounded borel pvm integral, one has $Φ_{F} (f) = Φ_{E} (f) \otimes I_{K};$

(c) if $(S_{n})$ is a sequence of bounded operators on $H$ with $\sup_{n} ∥ S_{n} ∥ < + \infty$ and $S_{n} x \to S x$ for every $x \in H$ , then $(S_{n} \otimes I_{K}) z \to (S \otimes I_{K}) z$ for every $z \in H \hat{\otimes} K$ ;

(d) if $X$ is a locally compact Hausdorff space (Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space), $Σ$ its Borel $σ$ -algebra (The Borel sigma-algebra of a topological space) and $E$ regular in the sense of Projection valued measure, then $F$ is regular.

Clause (d) is what makes $F$ a regular projection valued measure on $R$ in the application to assigned sharp observables, so that the converse direction of the spectral theorem supplies a self-adjoint operator having $F$ as its spectral measure. No assertion is made about unbounded operators in this lemma itself.

Facts & Assumptions

Given: The Axiom of Countable Choice; nonzero complex Hilbert spaces $H, K$ ; the completed tensor product $H \hat{\otimes} K$ with inclusion $κ$ ; a measurable space $(X, Σ)$ ; a projection valued measure $E$ on $(X, Σ)$ ; the operators $S_{n}, S \in B (H)$ ; a bounded measurable $f : X \to C$ .

[F1]

Tensor-product maps. By Bounded tensor maps: extension, norm estimate, adjoint and commutation clauses (a)-(d), for all bounded $S \in B (H, H^{'})$ , $T \in B (K, K^{'})$ there is a unique bounded $S \otimes T$ with $(S \otimes T) κ (u \otimes v) = κ^{'} (S u \otimes T v)$ , satisfying $∥ S \otimes T ∥ \leq ∥ S ∥ ∥ T ∥$ (The operator norm as the least bound and as the unit-sphere or unit-ball supremum), $(S \otimes T)^{*} = S^{*} \otimes T^{*}$ and $(S \otimes T) (S^{'} \otimes T^{'}) = (S S^{'}) \otimes (T T^{'})$ ; the assignment is linear in each argument, and $κ [H ⊙ K]$ is dense in $H \hat{\otimes} K$ (Hilbert tensor construction: inner product, completion and product bases clause (c)).

[F2]

Projection valued measure. $E (B)$ is an orthogonal projection on $H$ for every $B \in Σ$ (The Hilbert orthogonal projection onto a closed subspace), $E (\emptyset) = 0$ , $E (X) = I$ , $E (B \cap C) = E (B) E (C)$ , and for pairwise disjoint $B_{n}$ with union $B$ one has $E (B) x = \sum_{n} E (B_{n}) x$ in norm for every $x \in H$ (Projection valued measure).

[F3]

Bounded PVM integral. For bounded measurable $f$ there is a unique bounded $Φ_{E} (f) = \int f d E$ with $⟨ Φ_{E} (f) x, y ⟩ = \int f d E_{x, y}$ ; for every sequence of complex simple functions $s_{n}$ with $∥ f - s_{n} ∥_{\infty} \to 0$ one has $∥ Φ_{E} (f) - \int s_{n} d E ∥ \to 0$ , and $∥ Φ_{E} (f) ∥ \leq ∥ f ∥_{\infty}$ (Bounded borel pvm integral).

[F4]

Regular projection valued measures. When $X$ is locally compact Hausdorff and $Σ$ its Borel $σ$ -algebra, $E$ is regular exactly when every finite positive measure $E_{x} (B) = ⟨ E (B) x, x ⟩$ is a regular Borel measure: Radon, meaning finite on compact sets, outer regular on Borel sets and inner regular on open sets (Radon measure on an LCH space), and inner regular on every Borel set (Regular Borel measure on an LCH space).

Proof

Proof technique: direct; first establish that the tensor family is a projection valued measure, including strong countable additivity; then use its bounded PVM integral, extend the simple-function identity by uniform approximation, and prove regularity of its scalar measures first on finite algebraic tensors and then on the completed product by density.

Given: The data of the statement and [F1]-[F4].

1.1F1algebrachoose

[Strong continuity of tensoring with the identity] Let $M : = \sup_{n} ∥ S_{n} ∥ < + \infty$ . Strong convergence gives $∥ S x ∥ = \lim_{n} ∥ S_{n} x ∥ \leq M ∥ x ∥$ for every $x \in H$ , so $∥ S ∥ \leq M$ . For $z \in H \hat{\otimes} K$ and $ε > 0$ , density [F1] gives a finite sum $z_{0} = κ (\sum_{i = 1}^{m} u_{i} \otimes v_{i})$ with $∥ z - z_{0} ∥ < ε / (4 M + 1)$ . By linearity and the norm estimate [F1], $∥ (S_{n} \otimes I) - (S \otimes I) ∥ \leq M + ∥ S ∥ \leq 2 M$ , and hence $∥ ((S_{n} \otimes I) - (S \otimes I)) (z - z_{0}) ∥ < ε / 2$ for every $n$ (also when $M = 0$ , when the left side is zero). On the finite sum, [F1] gives $∥ ((S_{n} \otimes I) - (S \otimes I)) z_{0} ∥ \leq \sum_{i = 1}^{m} ∥ (S_{n} - S) u_{i} ∥ ∥ v_{i} ∥ \to 0$ . This is less than $ε / 2$ for all large $n$ , and the triangle inequality proves (c).

1.2F1F2algebra

[Projection structure] For $B, C \in Σ$ one has $F (B)^{*} = (E (B) \otimes I)^{*} = E (B)^{*} \otimes I^{*} = E (B) \otimes I = F (B)$ and $F (B)^{2} = (E (B) \otimes I) (E (B) \otimes I) = E (B)^{2} \otimes I^{2} = E (B) \otimes I = F (B)$ , so $F (B)$ is an orthogonal projection; moreover $F (B \cap C) = (E (B) E (C)) \otimes I = (E (B) \otimes I) (E (C) \otimes I) = F (B) F (C)$ , $F (\emptyset) = 0 \otimes I = 0$ and $F (X) = I \otimes I = I$ .

2.1F1F2step 1.1step 1.2algebra

[Strong countable additivity] Let $(B_{n})$ be pairwise disjoint with union $B$ . For finite $N$ the multiplicativity of step 1.2 and $F (B_{i}) F (B_{j}) = F (B_{i} \cap B_{j}) = 0$ for $i \neq j$ give $\sum_{n \leq N} F (B_{n}) = F (⋃_{n \leq N} B_{n}) = E (⋃_{n \leq N} B_{n}) \otimes I$ . The orthogonal projections $E (⋃_{n \leq N} B_{n})$ are uniformly bounded by one and converge strongly to $E (B)$ by [F2], so step 1.1 gives $\sum_{n \leq N} F (B_{n}) \to F (B)$ strongly. Together with step 1.2, this proves (a), so $F$ is now a projection valued measure.

3.1F1F3step 2.1constructalgebra

[Integral identity] Since step 2.1 proves that $F$ is a projection valued measure, the bounded PVM integral theorem [F3] applies to both $E$ and $F$ . For a complex simple function $s = \sum_{k = 1}^{m} α_{k} 1_{B_{k}}$ with $B_{k} \in Σ$ pairwise disjoint, linearity of $S \mapsto S \otimes I$ and of the integral [F1, F3] give $Φ_{F} (s) = \sum_{k} α_{k} F (B_{k}) = \sum_{k} α_{k} (E (B_{k}) \otimes I) = (\sum_{k} α_{k} E (B_{k})) \otimes I = Φ_{E} (s) \otimes I$ . For bounded measurable $f$ choose simple $s_{n}$ with $∥ f - s_{n} ∥_{\infty} \leq 2^{- n}$ by partitioning a square containing the bounded range of $f$ into finitely many small squares; the norm bounds [F1, F3] give $∥ Φ_{F} (f) - Φ_{F} (s_{n}) ∥ \leq ∥ f - s_{n} ∥_{\infty} \to 0$ and $∥ Φ_{E} (f) \otimes I - Φ_{E} (s_{n}) \otimes I ∥ \leq ∥ f - s_{n} ∥_{\infty} \to 0$ , so uniqueness of limits yields $Φ_{F} (f) = Φ_{E} (f) \otimes I$ , which is (b).

3.2F1F4step 2.1algebrachoose

[Regularity on finite algebraic tensors] Assume $X$ locally compact Hausdorff with Borel $σ$ -algebra and $E$ regular, and let $z_{0} = κ (\sum_{i = 1}^{m} u_{i} \otimes v_{i})$ . Put $C : = \sum_{i = 1}^{m} ∥ v_{i} ∥^{2}$ . If $m = 0$ or $C = 0$ , then $z_{0} = 0$ , so $ν_{z_{0}}$ is the zero measure and is inner regular on every Borel set, taking the compact set $\emptyset$ . Otherwise $m \geq 1$ and $C > 0$ . For Borel $B$ , $F (B) z_{0} = κ (\sum_{i = 1}^{m} E (B) u_{i} \otimes v_{i})$ by [F1], so the Cauchy-Schwarz inequality for the Euclidean pairing gives $ν_{z_{0}} (B) : = ⟨ F (B) z_{0}, z_{0} ⟩ = ∥ \sum_{i} E (B) u_{i} \otimes v_{i} ∥^{2} \leq C \sum_{i} ⟨ E (B) u_{i}, u_{i} ⟩$ ; also $ν_{z_{0}} (X) = ∥ z_{0} ∥^{2} < + \infty$ . Given $ε > 0$ , each finite measure $⟨ E (\cdot) u_{i}, u_{i} ⟩$ is regular by [F4], so there are compact $K_{i} \subseteq B$ with $⟨ E (B ∖ K_{i}) u_{i}, u_{i} ⟩ < ε / (m C)$ ; for the compact $K = ⋃_{i} K_{i}$ one has $B ∖ K \subseteq B ∖ K_{i}$ and hence $ν_{z_{0}} (B) - ν_{z_{0}} (K) = ν_{z_{0}} (B ∖ K) \leq C \sum_{i} ⟨ E (B ∖ K_{i}) u_{i}, u_{i} ⟩ < ε$ . Thus $ν_{z_{0}}$ is inner regular on Borel sets.

4.1F1F4step 2.1step 3.2algebrachoose

[Regularity on the completed product] Keep the hypotheses of step 3.2 and let $z \in H \hat{\otimes} K$ , $B$ Borel, $ε > 0$ ; if $z = 0$ there is nothing to prove, so let $z \neq 0$ and choose $z_{0} = κ (\sum_{i} u_{i} \otimes v_{i})$ with $∥ z - z_{0} ∥ \leq \sqrt{ε} / 2$ by [F1], then a compact $K \subseteq B$ with $ν_{z_{0}} (B ∖ K) \leq ε / 4$ by step 3.2. Since $F$ is projection valued by step 2.1, $ν_{z} (B) - ν_{z} (K) = ∥ F (B ∖ K) z ∥^{2} \leq (∥ F (B ∖ K) (z - z_{0}) ∥ + ∥ F (B ∖ K) z_{0} ∥)^{2} \leq (\sqrt{ε} / 2 + \sqrt{ε} / 2)^{2} = ε$ , so $ν_{z}$ is inner regular on Borel sets; it is finite since $ν_{z} (X) = ∥ z ∥^{2} < + \infty$ . Inner regularity applied to the complement gives outer regularity: for Borel $E_{0}$ and $η > 0$ choose compact $L \subseteq X ∖ E_{0}$ with $ν_{z} (X ∖ E_{0}) - ν_{z} (L) < η$ , so the open $V = X ∖ L$ contains $E_{0}$ and $ν_{z} (V) < ν_{z} (E_{0}) + η$ . Hence every $F_{z}$ is a regular Borel measure and $F$ is regular, which is (d).

5.1step 1.1step 2.1step 3.1step 3.2step 4.1∎

[Assembly] Step 2.1 proves (a), step 3.1 proves (b), step 1.1 proves (c), and steps 3.2 and 4.1 prove (d).

Remarks

Use. The lemma is the mathematical core of the local readout of a subsystem quantity: on a composite $H \hat{\otimes} K$ , the outcome structure of a quantity of the first factor alone is $E (\cdot) \otimes I_{K}$ , and by clause (d) together with the converse direction of the spectral theorem it is the spectral measure of a self-adjoint operator on the composite. Nothing here is a physical statement about measurements; the physical reading is fixed on the composites page.
Countable Choice. The choice hypothesis enters through the tensor construction and is carried as stated; clause (c) additionally uses the density of the algebraic tensor product, which is part of that construction.

Local PVM extension: tensoring a projection-valued measure with the identity

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources