Lean, informalized

Nielsen & Chuang · Chapter 9, Distance measures for quantum information · p. 405

Theorem 9.1 - No measurement separates two states by more than their trace distance, and one reaches it

Trace distance as the largest distance between measurement statistics.

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

A system is prepared in one of two states, ρ\rho or σ\sigma, and we may perform a single measurement on it. Outcome ii comes up with probability pip_i if the state is ρ\rho and with probability qiq_i if it is σ\sigma, and how far apart the two distributions lie depends on the measurement we choose. Theorem 9.1 says that the trace distance D(ρ,σ)D(\rho,\sigma) of the two states, half the trace norm of ρ−σ\rho - \sigma, is the most any measurement can achieve.

A Quantum System

A quantum system SS is a physical object whose state space is a finite dimensional complex Hilbert space.✦ A state ρ\rho of SS, pure or mixed, is a positive operator of unit trace on the state space of SS.✦

The trace distance D(ρ,σ)D(\rho,\sigma) between two states ρ\rho and σ\sigma of SS is half the trace norm of their difference, half the sum of the absolute values of the eigenvalues λk\lambda_k of ρ−σ\rho - \sigma: D(ρ,σ)=12tr⁡|ρ−σ|=12∑k|λk|.D(\rho,\sigma) = \tfrac12 \operatorname{tr}\lvert \rho - \sigma \rvert = \tfrac12 \sum_k \lvert \lambda_k \rvert .(1)✦

Measurement Statistics

A measurement MM on SS with a finite set of outcomes is a family of measurement operators MiM_i on the state space of SS, one for each outcome ii, satisfying the completeness relation ∑iMi†Mi=I.\sum_i M_i^\dagger M_i = I .(2)✦ The positive operator valued measure (POVM) of a measurement MM is the family of effects Ei=Mi†MiE_i = M_i^\dagger M_i, one for each outcome ii.✦

The probability of the outcome ii when MM is performed on a state ρ\rho is given by the Born rule, pi=tr⁡(MiρMi†)=tr⁡(Eiρ),p_i = \operatorname{tr}\bigl(M_i \rho M_i^\dagger\bigr) = \operatorname{tr}(E_i \rho) ,(3)✦ and the same measurement performed on σ\sigma gives qi=tr⁡(Eiσ)q_i = \operatorname{tr}(E_i \sigma).

The classical trace distance D(px,qx)D(p_x, q_x) of two real functions pp and qq on a finite set, two probability distributions for instance, is half the sum of the absolute differences of their values over the points xx of the set: D(px,qx)=12∑x|px−qx|.D(p_x, q_x) = \tfrac12 \sum_x \lvert p_x - q_x \rvert .(4)✦

The Claim

Theorem 1. Let ρ\rho and σ\sigma be states of a quantum system SS. For each measurement MM on SS with nn outcomes, nn any natural number, let pip_i and qiq_i be the probabilities (3) of the outcome ii on ρ\rho and on σ\sigma. Then the trace distance of the two states is the largest classical trace distance of such a pair of distributions, D(ρ,σ)=maxMD(pi,qi).D(\rho,\sigma) = \max_{M} D(p_i, q_i) .(5)✦

What Is Checked

The claim is stated over two states ρ\rho and σ\sigma of a quantum system SS and their trace distance (1), and over the measurements on SS with finitely many outcomes, whose Born probabilities (3) on the two states are compared by the classical trace distance (4).

Of these constructions, the library proves that the effects Ei=Mi†MiE_i = M_i^\dagger M_i of a measurement are positive operators summing to the identity, by (2), so that they form a POVM, and that the Born probabilities of a state under it form a probability distribution on the outcomes.