FiniteMajorization

Abstract

Finite real-vector convex domination yields a doubly stochastic matrix carrying the larger vector to the smaller one. Prefix sums of increasing vectors give convex domination. The proof constructs the majorization relation and consumes pinned Mathlib Birkhoff theory; it is not a second proof of Birkhoff.

The construction of Daniel Lyng in Econlib revision d7bd9477476cade1c6695c8891746048ceddc52f is adapted under Apache-2.0. Apache-2.0 license: docs/reports/licenses/econlib-strassen/LICENSE.txt. Strassen (1965) provides the historical martingale-transport context. In formulas, coe denotes the canonical coercion, dmu the integration measure, iUnion indexed union, smul scalar multiplication, and ae almost everywhere. Namespace-qualified Lean names and interval constructors retain their mathematical meaning; separated identifier words denote the corresponding underscored Lean constant.

Lemma 1.1 (convexOn_hinge_right).

$$\forall (a:\mathbb{R}),\mathrm{ConvexOn}\mathbb{R}\mathrm{Set}.\mathrm{univ}\mathrm{fun}z\mapsto \max (z-a)0$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Convexity/FiniteMajorization.convexOn_hinge_right (✓ std3). ∎

Citation. Daniel Lyng (2026). Econlib compact scalar Strassen construction. URL: https://github.com/danlyng/Econlib/blob/d7bd9477476cade1c6695c8891746048ceddc52f/Econlib/Probability/Order/Strassen.lean.

Commentary.

The positive-part excess over a fixed real threshold is convex on the whole real line.

Theorem 1.2 (exists_doublyStochastic_mulVec_of_convex_dominates).

$$\forall \{n:\mathbb{N}\}(xy:\mathrm{Fin}n\to \mathbb{R}),(\forall (\phi :\mathbb{R}\to \mathbb{R}),\mathrm{ConvexOn}\mathbb{R}\mathrm{Set}.\mathrm{univ}\phi \to \sum i,\phi (xi)\le \sum j,\phi (yj))\to \sum i,xi=\sum j,yj\to \exists D\in \mathrm{doublyStochastic}\mathbb{R}(\mathrm{Fin}n),D.\mathrm{mulVec}y=x$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Convexity/FiniteMajorization.exists_doublyStochastic_mulVec_of_convex_dominates (✓ std3). ∎

Citation. Daniel Lyng (2026). Econlib compact scalar Strassen construction. URL: https://github.com/danlyng/Econlib/blob/d7bd9477476cade1c6695c8891746048ceddc52f/Econlib/Probability/Order/Strassen.lean.

Commentary.

Convex domination and equal total sums for two finite real vectors yield a doubly stochastic matrix taking the second vector to the first. Empty vectors are included.

Theorem 1.3 (sum_convex_le_of_partial_sum_ge).

$$\forall \{n:\mathbb{N}\}(xy:\mathrm{Fin}n\to \mathbb{R}),\mathrm{Monotone}x\to \mathrm{Monotone}y\to \sum i,xi=\sum i,yi\to (\forall (K:\mathrm{Fin}n),\sum i\mathrm{with}\mathrm{coe}i\le \mathrm{coe}K,yi\le \sum i\mathrm{with}\mathrm{coe}i\le \mathrm{coe}K,xi)\to \forall \{\phi :\mathbb{R}\to \mathbb{R}\},\mathrm{ConvexOn}\mathbb{R}\mathrm{Set}.\mathrm{univ}\phi \to \sum i,\phi (xi)\le \sum i,\phi (yi)$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Convexity/FiniteMajorization.sum_convex_le_of_partial_sum_ge (✓ std3). ∎

Citation. Daniel Lyng (2026). Econlib compact scalar Strassen construction. URL: https://github.com/danlyng/Econlib/blob/d7bd9477476cade1c6695c8891746048ceddc52f/Econlib/Probability/Order/Strassen.lean.

Commentary.

For increasing finite vectors of equal total sum, domination of every lower prefix sum implies the inequality for every globally convex real test.

References

• Truth anchor: D5/S3/Analytic/Convexity/FiniteMajorization.convexOn_hinge_right
• Truth anchor: D5/S3/Analytic/Convexity/FiniteMajorization.exists_doublyStochastic_mulVec_of_convex_dominates
• Truth anchor: D5/S3/Analytic/Convexity/FiniteMajorization.sum_convex_le_of_partial_sum_ge