Lean, informalized

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

Exercise 9.4 - The classical trace distance of two distributions is the largest gap between the probabilities they give one event

Trace distance as the largest difference on one event.

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

Two probability distributions pxp_x and qxq_x are given on the same finite set of outcomes xx. A subset SS of the outcomes is an event, and each distribution gives it the sum of the probabilities of its outcomes, p(S)=∑x∈Spx,q(S)=∑x∈Sqx.p(S) = \sum_{x \in S} p_x, \qquad q(S) = \sum_{x \in S} q_x.(1) The exercise asks to show that the trace distance D(px,qx)D(p_x, q_x) of the two distributions, half the sum of the absolute differences of their values, is the largest difference between the probabilities they give to a single event.

The Classical Trace Distance

The classical trace distance D(px,qx)D(p_x, q_x) of two real functions pp and qq on a finite index set is D(px,qx)=12∑x|px−qx|.D(p_x, q_x) = \frac{1}{2} \sum_x |p_x - q_x|.(2)✦ For two probability distributions it is the trace distance of the exercise.

The Claim

Theorem 1. Let pp and qq be real functions on a finite index set whose values have the same sum, ∑xpx=∑xqx\sum_x p_x = \sum_x q_x, and let p(S)p(S) and q(S)q(S) be their sums (1) over a subset SS. Then D(px,qx)=maxS|p(S)−q(S)|,D(p_x, q_x) = \max_S \, |p(S) - q(S)|,(3)✦ the maximum taken over all subsets SS of the index set.

Two probability distributions satisfy the hypothesis, both totals being one, and for them the theorem is the exercise.

What Is Checked

The claim is stated over the classical trace distance (2) of two real functions on a finite index set and over their sums on the subsets of that set. What the library proves about these constructions is the identity (3) itself, on every finite index set.