TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck 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.

Finite Naimark isometric compression

Statement

Let $H$ be a nonzero finite-dimensional complex inner-product space, let $Ω$ be a finite nonempty set, and let $(E_{a})_{a \in Ω}$ be a finite POVM on $H$ . Put $r = ∣ Ω ∣$ , fix any bijection $j : Ω \to {0, \dots, r - 1}$ , and let $R = C^{r}$ with standard orthonormal basis $e_{0}, \dots, e_{r - 1}$ ; write $∣ a ⟩ = e_{j (a)}$ . Define

$V x : = \sum_{a \in Ω} E_{a}^{1 / 2} x \otimes ∣ a ⟩, Q_{a} : = I_{H} \otimes ∣ a ⟩ ⟨ a ∣ .$

Then $V^{*} V = I_{H}$ , the family $(Q_{a})_{a \in Ω}$ is a finite projective measurement on $H \otimes R$ , and $V^{*} Q_{a} V = E_{a}$ for every $a$ . For every density operator $ρ$ on $H$ , $V ρ V^{*}$ is a density operator on $H \otimes R$ and

${tr}_{H \otimes R} (V ρ V^{*} Q_{a}) = {tr}_{H} (ρ E_{a}) .$

The result holds for every finite enumeration $j$ and asserts an algebraic compression, not a physical realization.

Facts & Assumptions

Given: A nonzero finite-dimensional complex-inner-product space $H$ , a finite nonempty outcome set $Ω$ , a finite POVM $(E_{a})$ on $H$ , any enumeration $j$ of $Ω$ , and a density operator $ρ$ on $H$ .

[F1]

Finite POVMs and their outcome law: each $E_{a}$ is nonnegative and $\sum_{a} E_{a} = I_{H}$ .

[F2]

Finite projective measurements: a projective measurement is a finite family of pairwise orthogonal self-adjoint projections summing to the identity.

[F3]

Density operator: on nonzero finite-dimensional $H$ , a density operator is nonnegative and has trace one.

[F4]

Finite registers and their ordered computational bases: for $r \geq 1$ , the register $C^{r}$ has its standard ordered orthonormal basis.

[F5]

Ordered tensor registers, their inner product, and wire permutations: after specifying ordered orthonormal bases for the factors, their tensor register has the product inner product, with its factors in the declared order.

[F6]

The product basis is orthonormal and tensor dimensions multiply: product vectors from specified orthonormal bases of the factors form an orthonormal basis and tensor dimensions multiply.

[F7]

Dirac Notation Conversion: the root pairing is linear in its first argument and $∣ u ⟩ ⟨ v ∣$ sends $z$ to $⟨ z, v ⟩ u$ .

[F8]

Non-negative and positive operators: nonnegative means self-adjoint with $⟨ T x, x ⟩ \geq 0$ for every vector $x$ .

[F9]

A non-negative operator has a unique non-negative square root: each nonnegative $E_{a}$ has a unique nonnegative square root $M_{a}$ satisfying $M_{a}^{2} = E_{a}$ .

[F10]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ : $T^{*}$ satisfies $⟨ T x, y ⟩ = ⟨ x, T^{*} y ⟩$ under the root convention.

[F11]

Every linear map between finite-dimensional inner product spaces has a unique adjoint: every linear map between finite-dimensional inner-product spaces has a unique adjoint.

[F12]

For $A \in M_{m \times n} (F)$ and $B \in M_{n \times m} (F)$ , $tr (A B) = tr (B A)$ : traces of compatible rectangular products satisfy $tr (A B) = tr (B A)$ .

[F13]

Real and complex inner-product spaces and their induced length: complex inner products are positive definite and linear in the first argument.

[F14]

The basis-independent trace of an endomorphism of a finite-dimensional vector space: endomorphism trace is the matrix trace in any ordered basis and is basis-independent.

[F15]

Tensor products of finitely many linear maps: tensor maps are the unique linear maps satisfying their elementary-tensor formula.

[F16]

Projective measurement outcome weights are probabilities: for a density operator and a finite projective measurement, the outcome weight at $a$ is $tr (ρ P_{a})$ .

[F17]

Gram–Schmidt turns every finite independent list into an orthonormal list with the same successive spans: Gram–Schmidt turns a finite linearly independent list, in particular a basis, into an orthonormal list with the same span.

[F18]

Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis: finite-dimensional means having a finite basis; since $H$ is nonzero, its basis is nonempty.

Proof

1.1givenF2F4F5F6F7F10F11F13F15F17F18

Choose a finite basis of $H$ , which exists by [F18] and is linearly independent by the basis definition, and apply [F17] to obtain an orthonormal basis of $H$ . With the standard orthonormal basis of $R$ from [F4], [F6] gives an orthonormal product basis of $H \otimes R$ . For elementary tensors, [F7] and the tensor-map formula [F15] give $Q_{a} (x \otimes e_{c}) = δ_{j (a), c} x \otimes e_{j (a)}$ . Therefore $Q_{a}^{2} = Q_{a}$ , $Q_{a} Q_{b} = 0$ when $a \neq b$ , and $\sum_{a} Q_{a} = I$ on every product-basis vector; equality on that basis gives these operator identities. For elementary tensors $x \otimes e_{c}, y \otimes e_{d}$ , orthonormality and the product inner product give $⟨ Q_{a} (x \otimes e_{c}), y \otimes e_{d} ⟩ = δ_{j (a), c} δ_{j (a), d} ⟨ x, y ⟩ = ⟨ x \otimes e_{c}, Q_{a} (y \otimes e_{d}) ⟩$ . Sesquilinearity and spanning by [F6] extend this identity to all vectors, so uniqueness of adjoints [F11] gives $Q_{a}^{*} = Q_{a}$ . By [F2], $(Q_{a})$ is a projective measurement.

1.2givenF1F4F5F8F9F10F11F13F15

Put $M_{a} = E_{a}^{1 / 2}$ using [F9]. Each summand $x \mapsto M_{a} x \otimes e_{j (a)}$ is linear by [F15], so $V$ is linear. For $x, y \in H$ , orthogonality of the register labels and the product inner product give $⟨ V x, V y ⟩ = \sum_{a} ⟨ M_{a} x, M_{a} y ⟩ = ⟨ x, (\sum_{a} M_{a}^{*} M_{a}) y ⟩ = ⟨ x, y ⟩$ , because $M_{a}$ is self-adjoint by [F8]–[F9], so $M_{a}^{*} M_{a} = E_{a}$ , and [F1] gives $\sum_{a} E_{a} = I_{H}$ . The adjoint identities [F10]–[F11] also give $⟨ V x, V y ⟩ = ⟨ x, V^{*} V y ⟩$ . For fixed $y$ , set $x = (V^{*} V - I_{H}) y$ ; then $∥ x ∥^{2} = 0$ , so positive definiteness [F13] implies $(V^{*} V - I_{H}) y = 0$ . Since $y$ was arbitrary, $V^{*} V = I_{H}$ .

2.1givenF5F8F9F10F13step 1.1

Fix $b \in Ω$ . Step 1.1's action formula and the definition of $V$ give $Q_{b} V x = M_{b} x \otimes e_{j (b)}$ . For all $x, y \in H$ , the adjoint identity [F10], conjugate symmetry [F13], and product inner product [F5] yield $⟨ V^{*} Q_{b} V x, y ⟩ = ⟨ Q_{b} V x, V y ⟩ = ⟨ M_{b} x, M_{b} y ⟩ = ⟨ x, E_{b} y ⟩$ , where the last equality uses self-adjointness from [F8]–[F9], which gives $M_{b}^{*} M_{b} = E_{b}$ . If $T = V^{*} Q_{b} V - E_{b}$ , then $⟨ T x, y ⟩ = 0$ for every $x, y$ . Taking $y = T x$ gives $∥ T x ∥^{2} = 0$ , so [F13] implies $T x = 0$ for every $x$ ; hence $V^{*} Q_{b} V = E_{b}$ .

2.2givenF3F4F6F8F10F12F13F14F18step 1.1step 1.2

For all $z, w \in H \otimes R$ , the adjoint identities [F10] and self-adjointness of $ρ$ from [F3], [F8] give $⟨ V ρ V^{*} z, w ⟩ = ⟨ ρ V^{*} z, V^{*} w ⟩ = ⟨ V^{*} z, ρ V^{*} w ⟩ = ⟨ z, V ρ V^{*} w ⟩$ , where the last equality follows from [F10] and conjugate symmetry [F13]. Thus $V ρ V^{*}$ is self-adjoint. Also, for every $z$ , $⟨ V ρ V^{*} z, z ⟩ = ⟨ ρ V^{*} z, V^{*} z ⟩ \geq 0$ by [F3], [F8] and [F10], so it is nonnegative by [F8]. Also $\dim (H \otimes R) = r \dim H > 0$ by [F4] and [F6], since $H$ is nonzero by [F18] and $r \geq 1$ . In bases, rectangular trace cyclicity [F12] and [F14] give $tr (V ρ V^{*}) = tr (V^{*} V ρ) = tr (ρ) = 1$ by step 1.2 and [F3]. Therefore $V ρ V^{*}$ is a density operator on the nonzero space $H \otimes R$ .

3.1givenF1F12F14F16step 1.1step 2.1step 2.2∎

Step 1.1 proves $(Q_{a})$ is a projective measurement and step 2.2 proves $V ρ V^{*}$ is a density operator. Thus [F16] identifies its $b$ -outcome weight as $tr (V ρ V^{*} Q_{b})$ . Rectangular trace cyclicity [F12] and [F14] rewrite this as $tr (V^{*} Q_{b} V ρ)$ ; step 2.1 makes that $tr (E_{b} ρ) = tr (ρ E_{b})$ , using [F12] once more on $H$ . The final expression is the original POVM weight by [F1], proving the claimed equality.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

66 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

John Watrous, The Theory of Quantum Information (2018), §2.3.2, Theorem 2.42 (standard reference, not scraped)
John Preskill, Quantum Computation, Chapter 3: Foundations II: Measurement and Evolution, §3.1.2 (standard reference, not scraped)