The Exercise

Take two real vectors $x$ and $y$ with $d$ entries each, labelled by the same finite set of indices, such as two probability distributions over the same $d$ outcomes. Rearrange the entries of $y$ by a permutation chosen at random and average over the choice: the result is a mixture of permuted copies of $y$. Proposition 12.11 says which vectors are mixtures of this kind. They are exactly the vectors reachable this way, as the next section makes precise.

Majorization

The largest $k$-sum $L_k(y)$ of a real vector $y$, for a whole number $k \le d$, is the largest sum of $k$ of its entries, $$L_k(y) = \max_{|S| = k} \, \sum_{i \in S} y_i ,$$(1)^✦ where $S$ runs over the sets of $k$ indices.

A real vector $x$ is majorized by a real vector $y$ with the same indices, written $x \prec y$, when the entries of $x$ and of $y$ have the same sum and the entries of $x$ in any set $S$ of indices sum to at most the largest $|S|$-sum of $y$: $$\sum_i x_i = \sum_i y_i , \qquad \sum_{i \in S} x_i \le L_{|S|}(y) \quad \text{for every set $S$ of indices.}$$(2)^✦

The Claim

A permutation $\sigma$ of the indices acts on $y$ through its permutation matrix $P_\sigma$: the vector $P_\sigma y$ is $y$ with its entries rearranged by $\sigma$.

What Is Checked

The theorem is stated over majorization (2), which is defined through the largest $k$-sums (1), and over mixtures of the rearranged vectors $P_\sigma y$. What the library proves about these constructions is the theorem above, in both directions and for any finite set of indices.