Loomis Theorem (Positive B)

Setup

Fix finite nonempty index types $I$ and $J$. Let $A, B \colon I \times J \to \mathbb{R}$ be two real matrices, and assume $B$ is entrywise positive: $B_{ij} > 0$ for every $(i, j) \in I \times J$.

For $x \in \Delta(I)$ and $y \in \Delta(J)$ define the row- and column-vector products $$ (xA)_j = \sum_i x_i A_{ij}, \qquad (Ay)_i = \sum_j A_{ij}\, y_j, $$ and similarly $(xB)_j$, $(By)_i$. Positivity of $B$ implies $(xB)_j > 0$ for every $x \in \Delta(I)$ and every $j$, and $(By)_i > 0$ for every $y \in \Delta(J)$ and every $i$ — recorded as Positive Aggregates xB and By.

Statement

Theorem (Loomis). There exist $x \in \Delta(I)$, $y \in \Delta(J)$, and $v \in \mathbb{R}$ such that $$ xA \ge v \cdot xB, \qquad Ay \le v \cdot By, $$ where the inequalities are componentwise. Equivalently, for every $j \in J$ and every $i \in I$, $$ \sum_i x_i A_{ij} \ge v \sum_i x_i B_{ij}, \qquad \sum_j A_{ij}\, y_j \le v \sum_j B_{ij}\, y_j. $$

The common ratio level $v$ is the Loomis value of the pair $(A, B)$. The scalar form of the same statement is $$ \lambda_0 \;=\; \mu_0 \;=\; v, $$ where $$ \lambda_0 \;=\; \sup_{x \in \Delta(I)} \inf_{j \in J} \frac{(xA)_j}{(xB)_j}, \qquad \mu_0 \;=\; \inf_{y \in \Delta(J)} \sup_{i \in I} \frac{(Ay)_i}{(By)_i}. $$ The denominators are strictly positive by positivity of $B$, so both expressions are well-defined.

Discussion

MFoGT presents Loomis as an extension of von Neumann's minimax theorem. The canonical blueprint route in this library is the opposite: Loomis is proved directly by induction on $|I| + |J|$ (see the proof-plan Direct Induction Proof Of Loomis Theorem). Finite minimax is then the $B = \mathbf{1}$ specialisation (Minimax via the All-Ones Specialization of Loomis): for any probability vectors $x, y$ and the all-ones matrix $B = \mathbf{1}$, both $xB$ and $By$ are identically $1$, so the Loomis inequalities collapse to $\min_j (xA)_j \ge v \ge \max_i (Ay)_i$.

The library's Lean development formalises the general positive-$B$ Loomis theorem in EconCSLib.StrategicGame.Loomis, and re-derives the $B = \mathbf{1}$ specialisation (the finite von Neumann minimax) as the corollary Loomis.minmax_from_general. The original inlined induction at $B = \mathbf{1}$ in EconCSLib.StrategicGame.MinimaxLoomis is retained as an independent witness.