Lean, informalized

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

Exercise 9.1 - The classical trace distance, and its value on two pairs of probability distributions

The trace distance between two pairs of distributions.

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

The exercise asks for the trace distance between two probability distributions on two outcomes, (1,0)(1,0) and (12,12)(\frac12,\frac12), and between two on three outcomes, (12,13,16)(\frac12,\frac13,\frac16) and (34,18,18)(\frac34,\frac18,\frac18). The first pair compares a coin that always lands heads with a fair coin. The library defines the trace distance and states its value on each pair.

The Trace Distance

The trace distance D(px,qx)D(p_x,q_x) between two real functions pxp_x and qxq_x of an outcome xx ranging over a finite set is the real number D(px,qx)=12∑x|px−qx|.D(p_x,q_x) = \frac12 \sum_x \lvert p_x - q_x \rvert .(1)✦

The Claim

Theorem 1. For the deterministic distribution and the uniform distribution on two outcomes, D((1,0),(12,12))=12,D\bigl((1,0),(\tfrac12,\tfrac12)\bigr) = \frac12 ,(2)✦ and for two distributions on three outcomes, D((12,13,16),(34,18,18))=14.D\bigl((\tfrac12,\tfrac13,\tfrac16),(\tfrac34,\tfrac18,\tfrac18)\bigr) = \frac14 .(3)✦

What Is Checked

The claim is stated over a single construction, the trace distance (1), taken between the four distributions of the exercise. The library proves its two values, (2) on two outcomes and (3) on three.