The Exercise

Two lists of $d$ real numbers, $x$ and $y$ , are each sorted from largest to smallest, with the same total and with every partial sum of the largest entries of $x$ at most the largest possible sum of as many entries of $y$ . Mix the first entry of $y$ with a later one, the $p$ th, with weights $t$ and $1-t$ : the first becomes $t y_1 + (1-t) y_p$ and the $p$ th becomes $(1-t) y_1 + t y_p$ . The weight is chosen so that the new first entry is $x_1$ , and the index so that the entry of $y$ just before the $p$ th is still at least $x_1$ . The exercise is to show that when this common first entry is struck from both lists, what remains of $x$ is majorized by what remains of the mixed $y$ .^✦

Majorization

The largest sum of $k$ entries $S_k(y)$ of a real vector $y$ indexed by a set $I$ is the supremum, over the subsets $A$ of $I$ with $k$ elements, of the sum of the entries of $y$ over $A$ , $S_k(y) = \sup_{A \subseteq I,\ |A| = k} \ \sum_{i \in A} y_i ,$ (1)^✦ with $S_k(y) = 0$ when $k$ exceeds the number of indices.

A real vector $x$ indexed by a finite set $I$ is majorized by a real vector $y$ indexed by the same set, written $x \prec y$ , when the two have the same total and the sum of the entries of $x$ over any subset of $I$ is at most the largest sum of as many entries of $y$ : $x \prec y \iff \sum_{i \in I} x_i = \sum_{i \in I} y_i \ \text{ and } \ \sum_{i \in A} x_i \le S_{|A|}(y) \ \text{ for every } A \subseteq I .$ (2)^✦

The Claim

Theorem 1. Let $x$ and $y$ be real vectors of length $d$ with their entries in decreasing order, $x_1 \ge \dots \ge x_d$ and $y_1 \ge \dots \ge y_d$ , and with $x \prec y$ . Let $p$ be an index with $2 \le p \le d$ and $x_1 \le y_{p-1}$ , and let $t$ be a real number with $x_1 = t y_1 + (1-t) y_p$ . Let $\tilde y$ be the vector $y$ with its $p$ th entry replaced by $(1-t) y_1 + t y_p$ . Then the vectors left when the first entries of $x$ and $\tilde y$ are removed satisfy $(x_2, \dots, x_d) \prec (\tilde y_2, \dots, \tilde y_d) .$ (3)^✦

What Is Checked

The claim is stated over majorization of real vectors of lengths $d$ and $d-1$ , (2), and through it over the largest sum of $k$ entries, (1). What the library proves about these constructions is the theorem above, for every length $d$ and every real weight $t$ that meets its hypotheses.