The Exercise

Let $H$ and $K$ be Hermitian operators on the same state space of dimension $d$, written as $d \times d$ matrices. Choose unitaries $U_1, \dots, U_m$ and probabilities $p_1, \dots, p_m$, conjugate $K$ by each unitary and average with those weights. When $K$ is a density operator, the average $\sum_j p_j U_j K U_j^\dagger$ is the state of a system prepared in $K$ after a unitary $U_j$, chosen with probability $p_j$, has acted on it and the choice has been forgotten. Theorem 12.13 decides which operators $H$ arise from $K$ in this way, by a condition on the eigenvalues of the two operators alone: majorization.

Majorization

Let $\vec{y}$ be a real vector with $d$ entries $y_1, \dots, y_d$. For $0 \le k \le d$, the largest sum of $k$ entries of $\vec{y}$ is $$L_k(\vec{y}) = \max_{|s| = k} \sum_{i \in s} y_i,$$(1)^✦ the maximum running over all sets $s$ of $k$ indices.

A real vector $\vec{x}$ with $d$ entries is majorized by $\vec{y}$, written $\vec{x} \prec \vec{y}$, when the two have the same total and the entries of $\vec{x}$ in any set $s$ of indices sum to no more than the largest sum of as many entries of $\vec{y}$: $$\sum_{i=1}^{d} x_i = \sum_{i=1}^{d} y_i, \qquad \sum_{i \in s} x_i \le L_{|s|}(\vec{y}) \quad \text{for every } s \subseteq \{1, \dots, d\}.$$(2)^✦

A Hermitian $d \times d$ matrix $H$ is majorized by a Hermitian $d \times d$ matrix $K$, written $H \prec K$, when the vector $\vec{\lambda}(H)$ of the eigenvalues of $H$, each repeated as often as its multiplicity, is majorized by the vector $\vec{\lambda}(K)$ of the eigenvalues of $K$: $$H \prec K \iff \vec{\lambda}(H) \prec \vec{\lambda}(K).$$(3)^✦

The Claim

What Is Checked

The claim is stated over the majorization of Hermitian matrices (3), built from the vector majorization (2) and the largest sums (1), and over mixtures (4) of finitely many unitary conjugates of $K$. What the library proves about these constructions is the equivalence of the theorem, in both directions, for Hermitian matrices of every size.