The Exercise

Alice picks a message $x$ from a finite set, each $x$ with probability $p_x$, and encodes it in $n$ qubits by preparing them in a state $\rho_x$. She sends the qubits to Bob, who performs a measurement on them and obtains one of $r$ outcomes $y$. Message and outcome are then correlated random variables $X$ and $Y$, and their mutual information $H(X:Y)$ is what Bob learns about the message. The exercise is to show that he never learns more than $n$ bits, whatever states Alice prepares and whatever measurement he makes.^✦ It is a consequence of the Holevo bound.

A Quantum System

A quantum system $S$ is a physical system whose state space is a finite dimensional complex Hilbert space $\mathcal{H}_S$.^✦ The qubit $Q$ is the two level system, the system whose state space is $\mathbb{C}^2$.^✦ For finitely many systems $S_i$, the composite system $\bigotimes_i S_i$ is the system whose state space is the tensor product $\bigotimes_i \mathcal{H}_{S_i}$^✦, and the tensor power $S^{\otimes n}$ of a system $S$ is the composite of $n$ copies of $S$.^✦ Alice’s $n$ qubits form the system $Q^{\otimes n}$, with state space $$\mathcal{H}_{Q^{\otimes n}} = (\mathbb{C}^2)^{\otimes n}.$$(1)

A state $\rho$ of $S$ is a positive operator of unit trace on $\mathcal{H}_S$.^✦ Each $\rho_x$ is a state of $Q^{\otimes n}$.

A measurement $M$ on $S$ with a finite set of outcomes is a family of operators $M_y$ on $\mathcal{H}_S$, one for each outcome $y$, satisfying the completeness relation $$\sum_y M_y^\dagger M_y = I,$$(2)^✦ where $I$ is the identity on $\mathcal{H}_S$. The positive operator valued measure (POVM) of $M$ is the family of operators $E_y = M_y^\dagger M_y$ on $\mathcal{H}_S$, the effects of the outcomes.^✦ The probability of the outcome $y$ when $M$ is performed on a state $\rho$ of $S$ is given by the Born rule, $$p(y \mid \rho) = \operatorname{Tr}(M_y \rho M_y^\dagger) = \operatorname{Tr}(E_y \rho).$$(3)^✦

The Claim

The message $X$ and the outcome $Y$ have the joint distribution $$p(x, y) = p_x \operatorname{Tr}(E_y \rho_x).$$(4) $H(X:Y)$ is the mutual information of this distribution, with logarithms to base $e$; $n$ bits are then $n \log 2$.

What Is Checked

The claim is stated over the system $Q^{\otimes n}$ of $n$ qubits, the tensor power of the qubit, over states of that system, and over a measurement on it.

The library proves that the effects $E_y$ of a measurement are positive, so that they form a POVM. It proves also that a composite of finitely many systems has a finite dimensional state space, since the products of basis vectors of the factors form a basis of the tensor product; $Q^{\otimes n}$ is thus a quantum system.