The Exercise

Alice and Bob share a quantum system $AB$ in a state $\rho$, from which they will draw a secret key. An eavesdropper, Eve, holds a second system $E$, and $AB$ and $E$ together are in a pure state. Each value $x$ of the key occurs with probability $p_x$ and leaves Eve’s system in a state $\sigma_x$. Eve then measures $E$ in any way she likes and records the outcome $y$. The exercise is to show that the mutual information between the key and her outcome is at most the von Neumann entropy of $\rho$, whatever her measurement.^✦

Systems and States

A quantum system $Q$ is a physical system whose state space is a finite dimensional complex Hilbert space.^✦ The composite system $Q \otimes R$ of two quantum systems $Q$ and $R$ is the system whose state space is the tensor product of the state spaces of $Q$ and $R$.^✦ Alice and Bob’s system $AB$ counts as a single quantum system, and the whole is $AB \otimes E$.

A state $\omega$ of $Q$ is a positive operator of unit trace on the state space of $Q$.^✦ A pure state $|\psi\rangle$ of $Q$ is a unit vector in the state space of $Q$^✦, and the state it determines is the projector $|\psi\rangle\langle\psi|$ onto that vector.^✦

The reduced states of a state $\omega$ of the composite system $Q \otimes R$ are its partial traces $\operatorname{Tr}_R\,\omega$, a state of $Q$^✦, and $\operatorname{Tr}_Q\,\omega$, a state of $R$.^✦ For a pure state $|\psi\rangle$ of $AB \otimes E$ they are the state of Alice and Bob and the state of Eve, $$\rho = \operatorname{Tr}_E\,|\psi\rangle\langle\psi|, \qquad \rho_E = \operatorname{Tr}_{AB}\,|\psi\rangle\langle\psi| .$$(1)

The mixture of states $\sigma_x$ of $Q$, indexed by $x$ in a finite set, with weights $p_x \ge 0$ that sum to one, is the state $\sum_x p_x \sigma_x$ of $Q$.^✦ Averaged over the key, Eve’s state is such a mixture: $$\rho_E = \sum_x p_x\,\sigma_x .$$(2)

The von Neumann entropy of a state $\omega$ of $Q$ is $$S(\omega) = -\operatorname{tr}(\omega \log \omega),$$(3)^✦ The logarithm is natural, so entropies are in nats.

Eve’s Measurement

A measurement on a quantum system $Q$ with a finite set of outcomes is a family of measurement operators $M_y$ on the state space of $Q$, one for each outcome $y$, that satisfy the completeness relation $$\sum_y M_y^\dagger M_y = I .$$(4)^✦ The operators $M_y^\dagger M_y$ form the positive operator valued measure (POVM) of the measurement^✦, and on a state $\omega$ of $Q$ the outcome $y$ occurs with the probability given by the Born rule, $$p(y) = \operatorname{Tr}(M_y\,\omega\,M_y^\dagger) = \operatorname{Tr}(M_y^\dagger M_y\,\omega) .$$(5)^✦

Eve measures $E$ with operators $M_y$, so key and outcome have the joint distribution $$p(x,y) = p_x \operatorname{Tr}(M_y\,\sigma_x\,M_y^\dagger),$$(6) and $H(K:E)$ is the Shannon mutual information between $x$ and $y$ under it.

The Claim

What Is Checked

The claim is stated over a pure state of the composite system $AB \otimes E$ and its two reduced states (1), a mixture of states of $E$, a measurement on $E$ with its outcome probabilities (5), and the von Neumann entropy (3).

The library proves that these constructions give states and a POVM: the projector $|\psi\rangle\langle\psi|$ onto a unit vector is a density operator, and so are the partial traces of a density operator and a convex combination of density operators with nonnegative weights summing to one; the operators $M_y^\dagger M_y$ are positive and sum to the identity.