Minimax via the All-Ones Specialization of Loomis
This proof-plan node records the selected route the library uses to close
the finite von Neumann minimax theorem
(Von Neumann Minimax Theorem): take the Loomis theorem
(Loomis Theorem (Positive B)) and specialise the positive matrix
$B$ to the all-ones matrix $\mathbf{1}$. An alternative, ordered-field-generic
route is Minimax.minimax
(Ordered-Field Minimax Statement), proved sorry-free by von
Neumann symmetrisation over any linearly ordered field.
Proof (specialization of Loomis). Apply the Loomis theorem Loomis Theorem (Positive B) with the positive matrix $B = \mathbf{1}$ (the all-ones $I \times J$ matrix). It produces $x \in \Delta(I)$, $y \in \Delta(J)$, and $v \in \mathbb{R}$ with $$ xA \ge v \cdot xB \qquad\text{and}\qquad Ay \le v \cdot By. $$ For every probability vector $x \in \Delta(I)$ and $y \in \Delta(J)$ the all-ones vectors $xB$ and $By$ are identically $1$. Hence the Loomis inequalities collapse to $$ \sum_i x_i A(i, j) \ge v \quad\text{for every } j \in J, \qquad \sum_j y_j A(i, j) \le v \quad\text{for every } i \in I. $$ The first inequality says $x$ guarantees at least $v$ for player I, so $\lambda_0 \ge v$; the second says $y$ holds player I to at most $v$, so $\mu_0 \le v$. Weak duality $\lambda_0 \le \mu_0$ (Maximin is Bounded by Minimax) closes the sandwich: $\lambda_0 = \mu_0 = v$, with $(x, y)$ the asserted optimisers.
Lean implementation note. The Lean development now formalises the general
positive-$B$ Loomis theorem in EconCSLib.StrategicGame.Loomis and
re-derives finite minimax as the one-line corollary
Loomis.minmax_from_general, which calls loomis_value_eq at the
all-ones matrix B = fun _ _ => 1 and uses the bridge lemmas
lamB0_one and muB0_one to translate lamB0 A 1 back to
MinimaxLoomis.lam0 A (resp. muB0/mu0). This corollary is now the sole
route: the earlier standalone induction in
EconCSLib.StrategicGame.MinimaxLoomis was removed as redundant. That module
now contributes only the shared foundational scaffold reused by the general
proof — the aggregates, the existence + weak-duality step
(Existence of Optimal Mixed Strategies (Loomis Foundations)), and the
column/row drop-extend infrastructure — built on the core simplex layer
(Point Mass on the Standard Simplex, Continuity on the Real Standard Simplex,
Convex Combination of Simplex Points, and Pointwise Bounds Are Simplex Bounds).
References
- [MFoGT, Chapter 2, Section 2.3, Thm. 2.3.1] Laraki, Renault, and Sorin, Mathematical Foundations of Game Theory. Finite von Neumann minimax theorem.
- [MFoGT, Thm. 2.5.1] Same. Loomis theorem; minimax is the $B = \mathbf{1}$ specialisation.