The Exercise

Two real vectors $x$ and $y$, with entries labelled by the same finite set, are compared by majorization, $x \prec y$: the entries of $x$ are spread more evenly than those of $y$, with the same total. The usual test runs over subsets of entries and their sizes. The exercise trades it for a test over a real threshold $t$: for each vector, add up the amounts by which its entries exceed $t$, and compare the two sums at every $t$, together with the two totals.

Majorization and Tail Functions

A real vector $y$ on a finite set $\iota$ assigns a real number $y_i$ to each index $i$ of $\iota$. For a natural number $k$, the largest sum of $k$ entries of $y$, written $L_k(y)$, is the supremum, over all subsets $s$ of $\iota$ with $k$ elements, of the sum of the entries of $y$ over $s$, $$L_k(y) = \sup_{s \subseteq \iota,\ |s| = k}\ \sum_{i \in s} y_i ,$$(1)^✦ and it is $0$ when $k$ exceeds the number of indices, where no such subset exists.

A real vector $x$ on $\iota$ is majorized by a real vector $y$ on $\iota$, written $x \prec y$, when the two have the same total and no $k$ entries of $x$ add up to more than the largest sum of $k$ entries of $y$: $$x \prec y \iff \sum_{i \in \iota} x_i = \sum_{i \in \iota} y_i \ \text{ and }\ \sum_{i \in s} x_i \le L_{|s|}(y) \ \text{ for every } s \subseteq \iota .$$(2)^✦

The tail function of a real vector $x$ on $\iota$ is the function $T_x$ of a real threshold $t$ that adds up the excess of each entry over $t$, an entry at or below $t$ counting zero: $$T_x(t) = \sum_{i \in \iota} \max(x_i - t,\, 0) .$$(3)^✦

The Claim

What Is Checked

The claim is stated over majorization (2), built on the largest sums of entries (1), and over the tail functions (3) of the two vectors. What the library proves about them is the equivalence (4) in both directions, for vectors on any finite index set.