LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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 effects and instruments: normalization and non-determination of the update

Statement

Let $H$ be a finite-dimensional complex Hilbert space of dimension $d \geq 1$ (Hilbert space), with adjoints as in The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ and the finite trace as in The basis-independent trace of an endomorphism of a finite-dimensional vector space. Recall that an endomorphism $F$ is an effect when $F \geq 0$ and $I - F \geq 0$ , i.e. $0 \leq F \leq I$ in the quadratic-form order (Non-negative and positive operators).

(a) Definitions. A finite POVM is a finite family $(F_{a})_{a = 1}^{p}$ , $p \geq 1$ , of effects with $\sum_{a} F_{a} = I$ . An instrument here is a finite family $(M_{a, r})_{1 \leq a \leq p, 1 \leq r \leq q_{a}}$ of endomorphisms of $H$ , where each $q_{a}$ is a non-negative integer; its outcome operators and update maps are $F_{a} : = \sum_{r} M_{a, r}^{*} M_{a, r}$ and $I_{a} : End (H) \to End (H)$ , $I_{a} (R) : = \sum_{r} M_{a, r} R M_{a, r}^{*}$ , with empty sums equal to zero. It is normalized when $\sum_{a, r} M_{a, r}^{*} M_{a, r} = I$ . For a normalized instrument the $F_{a}$ are its outcome effects, as proved in (b); without normalization they need not be effects.

(b) If $(F_{a})$ is a finite POVM and $ρ$ a density operator (Density operators and scalar spectral probability) then $p_{a} : = tr (ρ F_{a}) \geq 0$ and $\sum_{a} p_{a} = 1$ . If $(M_{a, r})$ is a normalized instrument then the $F_{a}$ form a finite POVM, $tr I_{a} (ρ) = p_{a}$ , each $I_{a} (ρ)$ is non-negative, and whenever $p_{a} > 0$ the normalized update $I_{a} (ρ) / p_{a}$ is a density operator.

(c) Ideal Lüders case. For an orthogonal projection $P$ (The orthogonal projection $P_{W} v$ is the $W$ -component in $V = W \oplus W^{⊥}$ ) put $M_{0} = P$ , $M_{1} = I - P$ . Then $\sum_{j} M_{j}^{*} M_{j} = P + (I - P) = I$ , the effects are $F_{0} = P$ , $F_{1} = I - P$ , and $I_{j} (ρ) = P ρ P$ or $(I - P) ρ (I - P)$ .

(d) Non-determination. Effects alone do not determine the update: there are two normalized instruments on $C^{2}$ with the same outcome effects $F_{0} = diag (1, 0)$ , $F_{1} = diag (0, 1)$ whose updates differ on the same input.

Facts & Assumptions

Given: A finite-dimensional complex Hilbert space $H$ ; a density operator $ρ$ ; a finite POVM $(F_{a})$ ; a normalized instrument $(M_{a, r})$ ; an orthogonal projection $P$ .

[F2]

A self-adjoint endomorphism $T$ is non-negative exactly when $⟨ T v, v ⟩ \geq 0$ for all $v$ (Non-negative and positive operators); its eigenvalues are then non-negative by evaluation on eigenvectors. For non-negative $ρ$ , [F3] gives $(M ρ M^{*})^{*} = M ρ M^{*}$ , and the adjoint identity gives $⟨ M ρ M^{*} x, x ⟩ = ⟨ ρ M^{*} x, M^{*} x ⟩ \geq 0$ , so $M ρ M^{*}$ is non-negative.

[F3]

For endomorphisms $S, T$ of a finite-dimensional space, $tr (S T) = tr (T S)$ (For $A \in M_{m \times n} (F)$ and $B \in M_{n \times m} (F)$ , $tr (A B) = tr (B A)$ , The basis-independent trace of an endomorphism of a finite-dimensional vector space). The finite adjoint identities are justified directly: choose an orthonormal basis, available by applying Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely to $I$ . If $A = (a_{i j})$ is an operator matrix, then $A^{*} = {\overline{A}}^{T}$ satisfies the defining identity of The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ by expanding the two inner products in coordinates. Uniqueness follows because two adjoints $B, C$ give $⟨ x, (B - C) y ⟩ = 0$ for all $x, y$ , hence $(B - C) y = 0$ . Matrix conjugation and transposition now give $M^{* *} = M$ , $(A B)^{*} = B^{*} A^{*}$ and $(A + B)^{*} = A^{*} + B^{*}$ . Thus these finite identities require no Countable Choice; the general Hilbert-space theorem Hilbert-adjoint identities is not invoked.

[F4]

A density operator means a self-adjoint positive trace-class $ρ$ with trace $1$ (Density operators and scalar spectral probability), where positive means non-negative as in that supplier. Write $T_{u, v} x : = ⟨ x, v ⟩ u$ , with the inner product linear in its first argument, as in the same supplier. In the finite-dimensional $H$ used here, the finite-dimensional spectral theorem (Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely) gives an orthonormal eigenbasis $u_{1}, \dots, u_{d}$ for the self-adjoint, hence normal, $ρ$ . Put $w_{n} : = ⟨ ρ u_{n}, u_{n} ⟩ \geq 0$ by [F2]. The finite trace (The basis-independent trace of an endomorphism of a finite-dimensional vector space) gives $\sum_{n = 1}^{d} w_{n} = tr ρ = 1$ , and expansion in this basis gives $ρ = \sum_{n = 1}^{d} w_{n} T_{u_{n}, u_{n}}$ . This finite argument uses no Countable Choice and does not invoke the general density expansion.

[F5]

An endomorphism $U$ with $U^{*} U = I$ is a linear isometry; every orthogonal projection $P$ satisfies $P^{2} = P = P^{*}$ (Linear isometries, and orthogonal or unitary operators on finite-dimensional inner product spaces, The orthogonal projection $P_{W} v$ is the $W$ -component in $V = W \oplus W^{⊥}$ ).

Proof

1.1givenF2F3F4algebra

[POVM probabilities] By the finite-dimensional argument in [F4], $ρ = \sum_{n = 1}^{d} w_{n} T_{u_{n}, u_{n}}$ with $(u_{n})$ orthonormal and $\sum_{n} w_{n} = 1$ . Then $p_{a} = tr (ρ F_{a}) = \sum_{n} w_{n} ⟨ F_{a} u_{n}, u_{n} ⟩$ by linearity of the finite trace [F3], and each term is non-negative because $F_{a} \geq 0$ [F2]; hence $p_{a} \geq 0$ . Summing over $a$ and using linearity, $\sum_{a} p_{a} = \sum_{n} w_{n} ⟨ (\sum_{a} F_{a}) u_{n}, u_{n} ⟩ = \sum_{n} w_{n} = 1$ .

1.2givenF3F5algebra

[Lüders instance] For $M_{0} = P$ and $M_{1} = I - P$ with $P^{2} = P = P^{*}$ [F5], $M_{0}^{*} M_{0} = P^{2} = P$ and $M_{1}^{*} M_{1} = (I - P)^{2} = I - P$ , so $\sum_{j} M_{j}^{*} M_{j} = I$ and the effects are $F_{0} = P$ , $F_{1} = I - P$ ; the updates are $I_{0} (ρ) = P ρ P$ , $I_{1} (ρ) = (I - P) ρ (I - P)$ .

2.1step 1.1F2F3F4algebra

[Update traces and positivity] Let $F_{a} = \sum_{r} M_{a, r}^{*} M_{a, r}$ . Then $tr I_{a} (ρ) = \sum_{r} tr (M_{a, r} ρ M_{a, r}^{*}) = \sum_{r} tr (ρ M_{a, r}^{*} M_{a, r}) = tr (ρ F_{a}) = p_{a}$ , by cyclicity [F3]. For each $r$ , $(M_{a, r} ρ M_{a, r}^{*})^{*} = M_{a, r} ρ M_{a, r}^{*}$ because $ρ = ρ^{*}$ ; hence $I_{a} (ρ)$ is self-adjoint. For $x \in H$ , $⟨ I_{a} (ρ) x, x ⟩ = \sum_{r} ⟨ M_{a, r} ρ M_{a, r}^{*} x, x ⟩ = \sum_{r} ⟨ ρ (M_{a, r}^{*} x), M_{a, r}^{*} x ⟩ \geq 0$ because $ρ \geq 0$ ; thus $I_{a} (ρ) \geq 0$ . If $p_{a} > 0$ , then $I_{a} (ρ) / p_{a}$ has trace $1$ and is positive, hence is a density operator in the sense of [F4]. The effects of a normalized instrument form a POVM: each $M_{a, r}^{*} M_{a, r}$ is non-negative, and both $F_{a}$ and $I - F_{a} = \sum_{(b, r) : b \neq a} M_{b, r}^{*} M_{b, r}$ are non-negative, so $0 \leq F_{a} \leq I$ . This is (b).

3.1step 2.1F3F5algebra∎

[Two instruments with equal effects] On $H = C^{2}$ with orthonormal basis $(e_{1}, e_{2})$ let $F_{0} = T_{e_{1}, e_{1}}$ , $F_{1} = T_{e_{2}, e_{2}}$ and let $σ$ be the swap $σ e_{1} = e_{2}$ , $σ e_{2} = e_{1}$ , so that $σ^{*} σ = I$ by [F5]. Instrument A: $M_{0, 1} : = F_{0}$ , $M_{1, 1} : = F_{1}$ . Instrument B: $M_{0, 1} : = σ F_{0}$ , $M_{1, 1} : = F_{1}$ . Both are normalized: $F_{0}^{*} F_{0} + F_{1}^{*} F_{1} = F_{0} + F_{1} = I$ , and $(σ F_{0})^{*} (σ F_{0}) = F_{0} σ^{*} σ F_{0} = F_{0}^{2} = F_{0}$ , so $F_{1} + F_{0} = I$ . Their effect families coincide, but their updates differ on $ρ = \frac{1}{2} I$ : $I_{0}^{A} (ρ) = \frac{1}{2} F_{0} = \frac{1}{2} diag (1, 0)$ while $I_{0}^{B} (ρ) = \frac{1}{2} σ F_{0} σ = \frac{1}{2} diag (0, 1)$ , by $σ T_{e_{1}, e_{1}} σ = T_{σ e_{1}, σ e_{1}} = T_{e_{2}, e_{2}}$ . This is (d).

Finite effects and instruments: normalization and non-determination of the update

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources