The Exercise

Fix a real vector $\vec y$. The exercise asks to show that the set of all vectors majorized by $\vec y$ is convex.^✦

Majorization

Let $I$ be a finite set. A real vector $\vec x$ on $I$ assigns a real number $x_i$ to each index $i \in I$.

The largest $k$-sum $L_k(\vec x)$ of a real vector $\vec x$ on $I$ is the largest sum of $k$ of its entries, $$L_k(\vec x) = \max_{S \subseteq I,\ |S| = k} \; \sum_{i \in S} x_i ,$$(1)^✦ the maximum running over the subsets $S$ of $I$ with $k$ elements; it is taken to be $0$ when $k$ exceeds the number of elements of $I$, since then there is no such subset.

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

The Claim

What Is Checked

The claim is stated over majorization (2) of real vectors on an arbitrary finite index set, and through it over the largest $k$-sum (1). The one property of these constructions the library has is the claim itself, (3), for every vector $\vec y$ and every finite set $I$.