EconCSLib.Math.Minimax.MinimaxLoomis

LRS-style "simplified Loomis" proof of the finite minimax theorem.

This file ports the layered scaffolding from math-xmum/gametheory's GameTheory/Zerosum.lean. It is specialised to ℝ because the strategy spaces use compactness + continuity for the existence of optimisers — the ordered-field generalisation (any linearly ordered field) is Minimax.minimax, proved separately by von Neumann symmetrisation.

This file provides the foundational layer for the simplified-Loomis (von Neumann) minimax theorem: the mixed-strategy aggregates lam.aux / mu.aux, the scalar values lam0 / mu0, existence of optimisers via compactness, weak duality lam0 ≤ mu0, and the column/row dropping infrastructure (extendDropColumn / extendDropRow) reused by the general development.

The scalar equality lam0 A = mu0 A is not re-proved here by a standalone induction. It is the B = 𝟙 specialisation of the general (positive-B) Loomis theorem, exported as Loomis.minmax_from_general. (Earlier revisions carried an inlined copy of that induction, minmax'; it was removed as redundant once the general proof subsumed it.)

Attribution

Ported from GameTheory/Zerosum.lean in math-xmum/gametheory.

Expected payoff in mixed strategies

noncomputable def MinimaxLoomis.E {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] (A : I → J → ℝ) (x : ↑(stdSimplex ℝ I)) (y : ↑(stdSimplex ℝ J)) : ℝ

Expected payoff of a matrix game A : I → J → ℝ under mixed strategies x : stdSimplex ℝ I and y : stdSimplex ℝ J.

Equations

• MinimaxLoomis.E A x y = wsum x fun (i : I) => wsum y (A i)

Row aggregate lam.aux and its scalar value lam0

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

Player I's guaranteed payoff from mixed strategy x: the minimum over pure columns of the expected payoff.

Equations

• MinimaxLoomis.lam.aux A x = Finset.univ.inf' ⋯ fun (j : J) => wsum x fun (i : I) => A i j

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

Player I's maxmin value (the row player's best guarantee).

Equations

• MinimaxLoomis.lam0 A = iSup (MinimaxLoomis.lam.aux A)

theorem MinimaxLoomis.lam.aux_gt_iff_gt {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : I → J → ℝ) (c : ℝ) (x : ↑(stdSimplex ℝ I)) : c < aux A x ↔ ∀ (j : J), c < wsum x fun (i : I) => A i j

lam.aux A x > c iff every pure-column expected payoff exceeds c.

theorem MinimaxLoomis.lam.aux.continuous {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : I → J → ℝ) : Continuous (aux A)

lam.aux A is continuous as a function of the simplex point.

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

lam.aux A is uniformly bounded above on the simplex.

theorem MinimaxLoomis.lam.aux.le_lam0 {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : I → J → ℝ) (x : ↑(stdSimplex ℝ I)) : aux A x ≤ lam0 A

The supremum lam0 dominates every lam.aux value.

theorem MinimaxLoomis.exists_xx_lam0 {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : I → J → ℝ) : ∃ (xx : ↑(stdSimplex ℝ I)), ∀ (j : J), lam0 A ≤ wsum xx fun (i : I) => A i j

There exists a mixed strategy xx whose column-payoffs all dominate lam0 A. Compactness + continuity gives a maximiser of lam.aux; that maximiser realises the supremum and beats every pure-column expectation.

Column aggregate mu.aux and its scalar value mu0

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

Player II's maximum loss against mixed strategy y: the maximum over pure rows of the expected payoff.

Equations

• MinimaxLoomis.mu.aux A y = Finset.univ.sup' ⋯ fun (i : I) => wsum y fun (j : J) => A i j

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

Player II's minmax value (the column player's best cap).

Equations

• MinimaxLoomis.mu0 A = iInf (MinimaxLoomis.mu.aux A)

theorem MinimaxLoomis.mu.aux_lt_iff_lt {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : I → J → ℝ) (c : ℝ) (y : ↑(stdSimplex ℝ J)) : aux A y < c ↔ ∀ (i : I), (wsum y fun (j : J) => A i j) < c

mu.aux A y < c iff every pure-row expected payoff is below c.

theorem MinimaxLoomis.mu.aux.continuous {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : I → J → ℝ) : Continuous (aux A)

mu.aux A is continuous as a function of the simplex point.

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

mu.aux A is uniformly bounded below on the simplex.

theorem MinimaxLoomis.mu.aux.ge_mu0 {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : I → J → ℝ) (y : ↑(stdSimplex ℝ J)) : mu0 A ≤ aux A y

The infimum mu0 is dominated by every mu.aux value.

theorem MinimaxLoomis.exists_yy_mu0 {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : I → J → ℝ) : ∃ (yy : ↑(stdSimplex ℝ J)), ∀ (i : I), (wsum yy fun (j : J) => A i j) ≤ mu0 A

There exists a mixed strategy yy whose row-payoffs are all dominated by mu0 A.

Weak duality: lam0 ≤ mu0

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

Weak duality for the two-player zero-sum matrix game: every maxmin value is bounded by every minmax value.

Singleton reduction for |I| = |J| = 1

singleton_of_card_one is the shared helper feeding the base case of the general Loomis induction in Loomis.

theorem MinimaxLoomis.singleton_of_card_one {K : Type u_3} [Fintype K] [DecidableEq K] (H : Fintype.card K = 1) : ∃ (a : K), Finset.univ = {a}

When the row index type has cardinality 1, every simplex point is the unique pure strategy and Finset.univ is a singleton.

Restricting a matrix game by dropping a column / row

noncomputable def MinimaxLoomis.dropEquiv {J : Type u_2} [DecidableEq J] (j₀ : J) : J ≃ Option { j : J // j ≠ j₀ }

The equivalence J ≃ Option {j // j ≠ j₀}: j₀ ↦ none, other j ↦ some j.

Equations

• One or more equations did not get rendered due to their size.

theorem MinimaxLoomis.sum_split_at {J : Type u_2} [Fintype J] [Nonempty J] [DecidableEq J] (j₀ : J) (f : J → ℝ) : ∑ j : J, f j = f j₀ + ∑ j' : { j : J // j ≠ j₀ }, f ↑j'

Sum-splitting lemma: any function on J decomposes as the value at j₀ plus the sum over {j // j ≠ j₀}.

noncomputable def MinimaxLoomis.extendDropColumn {J : Type u_2} [Fintype J] [Nonempty J] [DecidableEq J] (j₀ : J) (y' : ↑(stdSimplex ℝ { j : J // j ≠ j₀ })) : ↑(stdSimplex ℝ J)

Extend a mixed strategy on J' = {j // j ≠ j₀} to a mixed strategy on J by putting zero mass on j₀.

Equations

• MinimaxLoomis.extendDropColumn j₀ y' = ⟨fun (j : J) => if h : j = j₀ then 0 else ↑y' ⟨j, h⟩, ⋯⟩

noncomputable def MinimaxLoomis.extendDropRow {I : Type u_1} [Fintype I] [Nonempty I] [DecidableEq I] (i₀ : I) (x' : ↑(stdSimplex ℝ { i : I // i ≠ i₀ })) : ↑(stdSimplex ℝ I)

Dual: extend a mixed strategy on I' = {i // i ≠ i₀} to one on I.

Equations

• MinimaxLoomis.extendDropRow i₀ x' = MinimaxLoomis.extendDropColumn i₀ x'

theorem MinimaxLoomis.wsum_extendDropColumn {J : Type u_2} [Fintype J] [Nonempty J] [DecidableEq J] (j₀ : J) (y' : ↑(stdSimplex ℝ { j : J // j ≠ j₀ })) (f : J → ℝ) : wsum (extendDropColumn j₀ y') f = ∑ j' : { j : J // j ≠ j₀ }, ↑y' j' * f ↑j'

wsum (extendDropColumn j₀ y') f equals the wsum of y' restricted to the corresponding sub-function on {j // j ≠ j₀}.

theorem MinimaxLoomis.wsum_extendDropRow {I : Type u_1} [Fintype I] [Nonempty I] [DecidableEq I] (i₀ : I) (x' : ↑(stdSimplex ℝ { i : I // i ≠ i₀ })) (f : I → ℝ) : wsum (extendDropRow i₀ x') f = ∑ i' : { i : I // i ≠ i₀ }, ↑x' i' * f ↑i'

Companion for row extension.