EconCSLib.Math.Minimax.Loomis

LRS-style direct induction proof of the general (positive-B) Loomis theorem [MFoGT, Theorem 2.5.1]:

For matrices A, B : I → J → ℝ with B entrywise positive there exist x : Δ(I), y : Δ(J), and v : ℝ with xA ≥ v · xB and Ay ≤ v · By.

This file begins with the scaffolding layer: positivity of the aggregates xB and By, the ratio-form auxiliaries lamB.aux and muB.aux, and the Loomis scalars lamB0, muB0.

Subsequent layers (continuity / attainment / weak duality / induction / packaged theorem) build on that scaffolding. The simplified-Loomis (von Neumann minimax) MinimaxLoomis.lam0 = MinimaxLoomis.mu0 is re-derived as the B = 𝟙 corollary minmax_from_general at the end of this file.

Blueprint

• docs/knowledge/nodes/zero_sum/loomis_theorem.md
• docs/knowledge/nodes/zero_sum/loomis_induction_proof.md
• docs/knowledge/nodes/zero_sum/loomis_induction_proof.positive_aggregate.md

Attribution

Structurally parallel to EconCSLib.Math.Minimax.MinimaxLoomis (ported from math-xmum/gametheory's GameTheory/Zerosum.lean), with B factors threaded through where the simplified-Loomis route had 1.

Entrywise positivity predicate

def Loomis.IsPositive {I : Type u_1} {J : Type u_2} (B : I → J → ℝ) : Prop

A matrix B : I → J → ℝ is entrywise positive if every entry is > 0. This is the hypothesis driving the general Loomis theorem, and the only property of B the proof needs.

Equations

• Loomis.IsPositive B = ∀ (i : I) (j : J), 0 < B i j

theorem Loomis.IsPositive.one {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] : IsPositive fun (x : I) (x_1 : J) => 1

The all-ones matrix is positive; the simplified-Loomis specialisation plugs B := fun _ _ => 1 into the general theorem.

Vector aggregates: xA, xB, Ay, By, and their positivity

The generic positivity lemma wsum_pos lives in Math.Simplex; the Loomis-flavored aggregates below are one-line applications of it.

noncomputable def Loomis.xA {I : Type u_1} {J : Type u_2} [Fintype I] (A : I → J → ℝ) (x : ↑(stdSimplex ℝ I)) (j : J) : ℝ

Row-vector product (xA)_j = ∑ᵢ xᵢ Aᵢⱼ.

Equations

• Loomis.xA A x j = wsum x fun (i : I) => A i j

noncomputable def Loomis.xB {I : Type u_1} {J : Type u_2} [Fintype I] (B : I → J → ℝ) (x : ↑(stdSimplex ℝ I)) (j : J) : ℝ

Row-vector product (xB)_j = ∑ᵢ xᵢ Bᵢⱼ.

Equations

• Loomis.xB B x j = wsum x fun (i : I) => B i j

noncomputable def Loomis.Ay {I : Type u_1} {J : Type u_2} [Fintype J] (A : I → J → ℝ) (y : ↑(stdSimplex ℝ J)) (i : I) : ℝ

Column-vector product (Ay)_i = ∑ⱼ Aᵢⱼ yⱼ.

Equations

• Loomis.Ay A y i = wsum y fun (j : J) => A i j

noncomputable def Loomis.By {I : Type u_1} {J : Type u_2} [Fintype J] (B : I → J → ℝ) (y : ↑(stdSimplex ℝ J)) (i : I) : ℝ

Column-vector product (By)_i = ∑ⱼ Bᵢⱼ yⱼ.

Equations

• Loomis.By B y i = wsum y fun (j : J) => B i j

theorem Loomis.xB_pos {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] {B : I → J → ℝ} (hB : IsPositive B) (x : ↑(stdSimplex ℝ I)) (j : J) : 0 < xB B x j

Positivity of the row aggregate when B is entrywise positive.

theorem Loomis.By_pos {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] {B : I → J → ℝ} (hB : IsPositive B) (y : ↑(stdSimplex ℝ J)) (i : I) : 0 < By B y i

Positivity of the column aggregate when B is entrywise positive.

theorem Loomis.xBy_pos {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] {B : I → J → ℝ} (hB : IsPositive B) (x : ↑(stdSimplex ℝ I)) (y : ↑(stdSimplex ℝ J)) : 0 < wsum x fun (i : I) => By B y i

Positivity of the bilinear pairing xBy = ∑ᵢⱼ xᵢ Bᵢⱼ yⱼ.

Loomis ratios and the scalars lamB0, muB0

noncomputable def Loomis.colRatio {I : Type u_1} {J : Type u_2} [Fintype I] (A B : I → J → ℝ) (x : ↑(stdSimplex ℝ I)) (j : J) : ℝ

Row player's per-column Loomis ratio (xA)_j / (xB)_j.

Equations

• Loomis.colRatio A B x j = Loomis.xA A x j / Loomis.xB B x j

noncomputable def Loomis.rowRatio {I : Type u_1} {J : Type u_2} [Fintype J] (A B : I → J → ℝ) (y : ↑(stdSimplex ℝ J)) (i : I) : ℝ

Column player's per-row Loomis ratio (Ay)_i / (By)_i.

Equations

• Loomis.rowRatio A B y i = Loomis.Ay A y i / Loomis.By B y i

noncomputable def Loomis.lamB.aux {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty J] (A B : I → J → ℝ) (x : ↑(stdSimplex ℝ I)) : ℝ

Player I's guaranteed Loomis ratio under mixed strategy x: infimum over pure columns.

Equations

• Loomis.lamB.aux A B x = Finset.univ.inf' ⋯ fun (j : J) => Loomis.colRatio A B x j

noncomputable def Loomis.muB.aux {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] (A B : I → J → ℝ) (y : ↑(stdSimplex ℝ J)) : ℝ

Player II's Loomis-ratio cap under mixed strategy y: supremum over pure rows.

Equations

• Loomis.muB.aux A B y = Finset.univ.sup' ⋯ fun (i : I) => Loomis.rowRatio A B y i

noncomputable def Loomis.lamB0 {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty J] (A B : I → J → ℝ) : ℝ

Maxmin Loomis scalar λ₀ = sup_x λ_aux(x).

Equations

• Loomis.lamB0 A B = iSup (Loomis.lamB.aux A B)

noncomputable def Loomis.muB0 {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] (A B : I → J → ℝ) : ℝ

Minmax Loomis scalar μ₀ = inf_y μ_aux(y).

Equations

• Loomis.muB0 A B = iInf (Loomis.muB.aux A B)

theorem Loomis.lamB.aux_gt_iff_gt {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A B : I → J → ℝ) (c : ℝ) (x : ↑(stdSimplex ℝ I)) : c < aux A B x ↔ ∀ (j : J), c < colRatio A B x j

Characterisation: lamB.aux A B x > c iff every column ratio exceeds c.

theorem Loomis.muB.aux_lt_iff_lt {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A B : I → J → ℝ) (c : ℝ) (y : ↑(stdSimplex ℝ J)) : aux A B y < c ↔ ∀ (i : I), rowRatio A B y i < c

Characterisation: muB.aux A B y < c iff every row ratio is below c.

Continuity, boundedness, and attainment

The Loomis ratios are continuous on the compact simplex (positive denominators by xB_pos / By_pos), so the inf'/sup' aggregates are continuous and their extrema lamB0 / muB0 are attained.

theorem Loomis.colRatio.continuous {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] {A B : I → J → ℝ} (hB : IsPositive B) (j : J) : Continuous fun (x : ↑(stdSimplex ℝ I)) => colRatio A B x j

Each column ratio (xA)_j / (xB)_j is continuous on Δ(I).

theorem Loomis.rowRatio.continuous {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] {A B : I → J → ℝ} (hB : IsPositive B) (i : I) : Continuous fun (y : ↑(stdSimplex ℝ J)) => rowRatio A B y i

Each row ratio (Ay)_i / (By)_i is continuous on Δ(J).

theorem Loomis.lamB.aux.continuous {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] {A B : I → J → ℝ} (hB : IsPositive B) : Continuous (aux A B)

lamB.aux A B is continuous on the simplex.

theorem Loomis.muB.aux.continuous {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] {A B : I → J → ℝ} (hB : IsPositive B) : Continuous (aux A B)

muB.aux A B is continuous on the simplex.

theorem Loomis.lamB.aux.bddAbove {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] {A B : I → J → ℝ} (hB : IsPositive B) : ∃ (C : ℝ), ∀ (x : ↑(stdSimplex ℝ I)), aux A B x ≤ C

lamB.aux A B is bounded above on the simplex (continuous function on a compact set).

theorem Loomis.muB.aux.bddBelow {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] {A B : I → J → ℝ} (hB : IsPositive B) : ∃ (C : ℝ), ∀ (y : ↑(stdSimplex ℝ J)), C ≤ aux A B y

muB.aux A B is bounded below on the simplex.

theorem Loomis.lamB.aux.le_lamB0 {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] {A B : I → J → ℝ} (hB : IsPositive B) (x : ↑(stdSimplex ℝ I)) : aux A B x ≤ lamB0 A B

Every lamB.aux value is bounded by the supremum lamB0.

theorem Loomis.muB.aux.ge_muB0 {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] {A B : I → J → ℝ} (hB : IsPositive B) (y : ↑(stdSimplex ℝ J)) : muB0 A B ≤ aux A B y

Every muB.aux value dominates the infimum muB0.

theorem Loomis.exists_xx_lamB0 {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A B : I → J → ℝ) (hB : IsPositive B) : ∃ (xx : ↑(stdSimplex ℝ I)), ∀ (j : J), lamB0 A B * xB B xx j ≤ xA A xx j

Attainment of lamB0: there exists a mixed strategy xx with (xA xx)_j ≥ lamB0 · (xB xx)_j for every column.

theorem Loomis.exists_yy_muB0 {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A B : I → J → ℝ) (hB : IsPositive B) : ∃ (yy : ↑(stdSimplex ℝ J)), ∀ (i : I), Ay A yy i ≤ muB0 A B * By B yy i

Attainment of muB0: there exists a mixed strategy yy with (Ay yy)_i ≤ muB0 · (By yy)_i for every row.

Weak duality lamB0 ≤ muB0

theorem Loomis.lamB0_le_muB0 {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A B : I → J → ℝ) (hB : IsPositive B) : lamB0 A B ≤ muB0 A B

Weak duality for the Loomis scalars: lamB0 ≤ muB0.

Base case |I| + |J| = 2

theorem Loomis.loomis_value_IJ_2 {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (Hn : 2 = Fintype.card I + Fintype.card J) {A B : I → J → ℝ} (_hB : IsPositive B) : lamB0 A B = muB0 A B

Base case of the Loomis induction: a 1×1 matrix pair has the single ratio A i₀ j₀ / B i₀ j₀ as the common Loomis value.

Induction step

We linearise the Loomis inequalities by introducing the offset functionals G(x, j) := (xA)_j - λ₀ · (xB)_j and H(y, i) := μ₀ · (By)_i - (Ay)_i, turning the inequalities xA ≥ λ₀ · xB and Ay ≤ μ₀ · By into nonneg conditions on functions linear in their simplex argument. Convex combinations then reduce to the constant-c = 0 linear_comb_* and mix_*_nbh lemmas from Core.Simplex.

Equivalence of the ratio form and the offset form

Column / row extension to the unrestricted simplex

The strong induction loomis_value_eq

theorem Loomis.loomis_value_eq {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A B : I → J → ℝ) (hB : IsPositive B) : lamB0 A B = muB0 A B

Loomis scalar equality: every finite positive-B matrix pair over ℝ has equal maxmin and minmax Loomis ratios.

Packaged Loomis theorem

theorem Loomis.loomis_theorem {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A B : I → J → ℝ) (hB : IsPositive B) : ∃ (x : ↑(stdSimplex ℝ I)) (y : ↑(stdSimplex ℝ J)) (v : ℝ), (∀ (j : J), v * xB B x j ≤ xA A x j) ∧ ∀ (i : I), Ay A y i ≤ v * By B y i

Loomis Theorem [MFoGT, Theorem 2.5.1].

For any pair of matrices A B : I → J → ℝ with B entrywise positive, there exist mixed strategies x : Δ(I), y : Δ(J) and a value v : ℝ such that for every column j ∈ J and every row i ∈ I, $$ v \cdot (xB)_j \le (xA)_j, \qquad (Ay)_i \le v \cdot (By)_i. $$ The common value v = lamB0 A B = muB0 A B.

Corollary: simplified Loomis = B = 1 specialisation

The simplified-Loomis development in MinimaxLoomis proves lam0 A = mu0 A directly by inlining the B = 𝟙 specialisation of the induction. This section re-derives that statement from the general positive-B Loomis theorem above, validating the minimax_from_loomis blueprint node's "all-ones specialisation" claim.

theorem Loomis.lamB0_one {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : I → J → ℝ) : (lamB0 A fun (x : I) (x_1 : J) => 1) = MinimaxLoomis.lam0 A

theorem Loomis.muB0_one {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : I → J → ℝ) : (muB0 A fun (x : I) (x_1 : J) => 1) = MinimaxLoomis.mu0 A

theorem Loomis.minmax_from_general {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : I → J → ℝ) : MinimaxLoomis.lam0 A = MinimaxLoomis.mu0 A

Simplified Loomis as a corollary of the general theorem: the finite von Neumann minimax MinimaxLoomis.lam0 A = MinimaxLoomis.mu0 A follows by instantiating loomis_value_eq at the all-ones matrix B = 𝟙.

This is the canonical "B = 𝟙 specialisation" route recorded by the [[minimax_from_loomis]] blueprint node, and the sole route to the finite von Neumann minimax: MinimaxLoomis keeps only the shared foundational layer (aggregates, attainment, weak duality, drop/extend infra), and its scalar equality is exported here rather than re-proved by a standalone induction.