Lean, informalized

Nielsen & Chuang · Chapter 2, Introduction to quantum mechanics · p. 93

Exercise 2.64 - A measurement in which every outcome but one names the state with certainty

Telling linearly independent states apart with certainty.

Hover over a blue or green term in the text, or a node in the graph, to find it in the other. Select it to read its declaration both in Lean and in words.

The Exercise

Bob is handed a quantum system in one of the pure states |ψ1⟩,…,|ψm⟩|\psi_1\rangle, \dots, |\psi_m\rangle, without being told which; the vectors are linearly independent. He is to build a measurement, a positive operator valued measure (POVM) with elements E1,…,Em+1E_1, \dots, E_{m+1}, such that whenever an outcome i≤mi \le m occurs he knows for certain that he was given |ψi⟩|\psi_i\rangle. Each outcome i≤mi \le m must also occur with positive probability when the state is |ψi⟩|\psi_i\rangle.

A Quantum System

A quantum system SS is described by its state space ℋS\mathcal{H}_S, a finite dimensional complex Hilbert space.✦ A state ρ\rho of SS is a positive operator of unit trace on ℋS\mathcal{H}_S.✦ A pure state ψ\psi of SS is a unit vector |ψ⟩|\psi\rangle in ℋS\mathcal{H}_S, determined physically up to a global phase.✦ The state of SS given by a pure state ψ\psi is the rank one projector |ψ⟩⟨ψ||\psi\rangle\langle\psi| onto |ψ⟩|\psi\rangle.✦

The Discriminating Measurement

The discriminating POVM of pure states ψ1,…,ψm\psi_1, \dots, \psi_m of SS is a POVM on ℋS\mathcal{H}_S built from their vectors alone: positive operators E1,…,EmE_1, \dots, E_m, one for each state of the family, and one more, Em+1E_{m+1}, which together resolve the identity, ∑i=1mEi+Em+1=I.\sum_{i=1}^{m} E_i + E_{m+1} = I.(1)✦ Made on a state ρ\rho of SS, the measurement gives outcome ii with probability tr⁡(Eiρ)\operatorname{tr}(E_i\rho); on the state |ψj⟩⟨ψj||\psi_j\rangle\langle\psi_j| this is ⟨ψj|Ei|ψj⟩\langle\psi_j|E_i|\psi_j\rangle.

The Claim

Theorem 1. Let ψ1,…,ψm\psi_1, \dots, \psi_m be pure states of a quantum system SS, and let E1,…,Em+1E_1, \dots, E_{m+1} be their discriminating POVM. An outcome i≤mi \le m never occurs on the state of ψj\psi_j when j≠ij \neq i: ⟨ψj|Ei|ψj⟩=0(1≤i,j≤m,j≠i).\langle\psi_j|E_i|\psi_j\rangle = 0 \qquad (1 \le i, j \le m,\ j \neq i).(2)✦ If moreover the vectors |ψ1⟩,…,|ψm⟩|\psi_1\rangle, \dots, |\psi_m\rangle are linearly independent, every outcome i≤mi \le m occurs with positive probability on the state of ψi\psi_i: ⟨ψi|Ei|ψi⟩>0(1≤i≤m).\langle\psi_i|E_i|\psi_i\rangle > 0 \qquad (1 \le i \le m).(3)✦

What Is Checked

The claim is stated over the discriminating POVM (1) of the pure states ψ1,…,ψm\psi_1, \dots, \psi_m, and over the states |ψj⟩⟨ψj||\psi_j\rangle\langle\psi_j| on which it is measured. The library proves that the projector onto a unit vector is positive with unit trace, so that each |ψj⟩⟨ψj||\psi_j\rangle\langle\psi_j| is a state of SS.