EconCSLib.GameTheory.StrategicGame.ZeroSum.MatrixGame

Von Neumann's Minimax Theorem for finite two-player zero-sum games.

Main definitions

• ZerosumGame — a matrix game g : I → J → ℝ
• maximin — player I's maximin value: max_x min_j E(x, j)
• minimax — player II's minimax value: min_y max_i E(i, y)
• HasMixedValue — the game has a value in mixed strategies

Main results

• maximin_le_minimax — maximin ≤ minimax (always)
• minimax_theorem — maximin = minimax for finite games [von Neumann 1928]
• minimax_optimal_strategies — existence of optimal mixed strategies

Proof method

This module exposes the real-valued Loomis route. The reusable ordered-field minimax theorem is available in EconCSLib.Math.Minimax.Minimax.

Attribution

Ported from GameTheory/Zerosum.lean in math-xmum/gametheory by Ma Jia-Jun, HXZ, yuxuan, and Lazyfill.

References

• [MSZ] Theorem 5.11 (von Neumann's Minimax Theorem)
• [LRS] Laraki, Renault, Sorin, Theorem 2.3.1

Matrix game

structure MatrixGame (I : Type u_1) (J : Type u_2) (𝕜 : Type := ℚ) : Type (max u_1 u_2)

A finite two-player zero-sum matrix game. Player I chooses row i : I, Player II chooses column j : J. Payoff to Player I is g i j (in the scalar field 𝕜); payoff to Player II is -g i j.

The scalar field 𝕜 defaults to ℚ so that unannotated MatrixGame I J means a rational matrix game — keeping the data structure Bourbaki-minimal and forcing the choice of ℝ (or any other ordered field) to be explicit at the use site.

• g : I → J → 𝕜

  The payoff matrix.

Expected payoff under mixed strategies

These bilinear-payoff and guarantee definitions are purely arithmetic + order; they go through over any linearly ordered field. Order-completeness (needed for maximin / minimax below) is not required here.

noncomputable def MatrixGame.payoffAgainstColumn {I : Type u_1} {J : Type u_2} [Fintype I] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] (A : MatrixGame I J 𝕜) (x : ↑(stdSimplex 𝕜 I)) (j : J) : 𝕜

Expected payoff when Player I uses mixed strategy x against pure column j.

Equations

• A.payoffAgainstColumn x j = ⇑x ⬝ᵥ fun (i : I) => A.g i j

noncomputable def MatrixGame.payoffAgainstRow {I : Type u_1} {J : Type u_2} [Fintype J] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] (A : MatrixGame I J 𝕜) (i : I) (y : ↑(stdSimplex 𝕜 J)) : 𝕜

Expected payoff when pure row i faces Player II's mixed strategy y.

Equations

• A.payoffAgainstRow i y = ⇑y ⬝ᵥ A.g i

noncomputable def MatrixGame.expectedPayoff {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] (A : MatrixGame I J 𝕜) (x : ↑(stdSimplex 𝕜 I)) (y : ↑(stdSimplex 𝕜 J)) : 𝕜

Expected payoff when Player I uses mixed strategy x and Player II uses y.

Equations

• A.expectedPayoff x y = ⇑x ⬝ᵥ fun (i : I) => A.payoffAgainstRow i y

noncomputable def MatrixGame.E {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] (A : MatrixGame I J 𝕜) (x : ↑(stdSimplex 𝕜 I)) (y : ↑(stdSimplex 𝕜 J)) : 𝕜

Expected payoff when Player I uses mixed strategy x and Player II uses y.

Equations

• A.E x y = A.expectedPayoff x y

noncomputable def MatrixGame.Ej {I : Type u_1} {J : Type u_2} [Fintype I] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] (A : MatrixGame I J 𝕜) (x : ↑(stdSimplex 𝕜 I)) (j : J) : 𝕜

Expected payoff when Player I uses x against pure column j.

Equations

• A.Ej x j = A.payoffAgainstColumn x j

noncomputable def MatrixGame.Ei {I : Type u_1} {J : Type u_2} [Fintype J] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] (A : MatrixGame I J 𝕜) (i : I) (y : ↑(stdSimplex 𝕜 J)) : 𝕜

Expected payoff when pure row i faces Player II's mixed strategy y.

Equations

• A.Ei i y = A.payoffAgainstRow i y

Pure-row / pure-column guarantees

noncomputable def MatrixGame.guarantee_I {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty J] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] (A : MatrixGame I J 𝕜) (x : ↑(stdSimplex 𝕜 I)) : 𝕜

Player I's guaranteed payoff using mixed strategy x: the minimum expected payoff over all of Player II's pure responses.

A finite Finset.inf' over J, so only [LinearOrder 𝕜] is needed — no order completeness.

Equations

• A.guarantee_I x = Finset.univ.inf' ⋯ fun (j : J) => A.Ej x j

noncomputable def MatrixGame.guarantee_II {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] (A : MatrixGame I J 𝕜) (y : ↑(stdSimplex 𝕜 J)) : 𝕜

Player II's guaranteed loss using mixed strategy y: the maximum expected payoff (for Player I) over all of Player I's pure responses.

Equations

• A.guarantee_II y = Finset.univ.sup' ⋯ fun (i : I) => A.Ei i y

Value predicates (field-generic)

IsMaximin, IsMinimax, IsValue express the value of a matrix game without committing to any specific witness construction. They are inequality predicates only, so they live at the Layer-2 hypothesis level [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] — usable over ℚ, ℝ, any ordered field, even when sSup-based maximin / minimax below are unavailable.

def MatrixGame.IsMaximin {I : Type u_1} {J : Type u_2} [Fintype I] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] (A : MatrixGame I J 𝕜) (v : 𝕜) : Prop

v is a maximin value of A: some row strategy guarantees at least v (existence), and no strictly larger value is achievable (maximality).

Equations

• A.IsMaximin v = ((∃ (x : ↑(stdSimplex 𝕜 I)), ∀ (j : J), v ≤ A.Ej x j) ∧ ∀ (w : 𝕜), (∃ (x : ↑(stdSimplex 𝕜 I)), ∀ (j : J), w ≤ A.Ej x j) → w ≤ v)

def MatrixGame.IsMinimax {I : Type u_1} {J : Type u_2} [Fintype J] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] (A : MatrixGame I J 𝕜) (v : 𝕜) : Prop

v is a minimax value of A: some column strategy caps player I's payoff at v (existence), and no strictly smaller cap is achievable (minimality).

Equations

• A.IsMinimax v = ((∃ (y : ↑(stdSimplex 𝕜 J)), ∀ (i : I), A.Ei i y ≤ v) ∧ ∀ (w : 𝕜), (∃ (y : ↑(stdSimplex 𝕜 J)), ∀ (i : I), A.Ei i y ≤ w) → v ≤ w)

def MatrixGame.IsValue {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] (A : MatrixGame I J 𝕜) (v : 𝕜) : Prop

v is the value of A (saddle-point form): there exist a row mixed strategy x and column mixed strategy y such that x guarantees at least v against every column and y caps player I's payoff at v against every row. Field-generic; MatrixGame.value below is the ℝ-valued specialisation (via iSup) when 𝕜 admits order completeness.

Equations

• A.IsValue v = ∃ (x : ↑(stdSimplex 𝕜 I)) (y : ↑(stdSimplex 𝕜 J)), (∀ (j : J), v ≤ A.Ej x j) ∧ ∀ (i : I), A.Ei i y ≤ v

Maximin and minimax values via iSup / iInf

maximin and minimax use iSup / iInf over the (uncountable) mixed-strategy simplex, so they need order completeness in addition to the Layer-2 hypotheses. We require [ConditionallyCompleteLinearOrder 𝕜] — satisfied by ℝ via Real.instConditionallyCompleteLinearOrder, but not by ℚ.

For an ordered field without order completeness (e.g. ℚ), use the field-generic IsMaximin / IsMinimax / IsValue predicates above instead — they characterise the same notion without invoking sSup.

noncomputable def MatrixGame.maximin {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty J] {𝕜 : Type} [Field 𝕜] [ConditionallyCompleteLinearOrder 𝕜] (A : MatrixGame I J 𝕜) : 𝕜

The maximin value: the best guarantee Player I can achieve. maximin = sup_x inf_j E(x, j)

Equations

• A.maximin = ⨆ (x : ↑(stdSimplex 𝕜 I)), A.guarantee_I x

noncomputable def MatrixGame.minimax {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] {𝕜 : Type} [Field 𝕜] [ConditionallyCompleteLinearOrder 𝕜] (A : MatrixGame I J 𝕜) : 𝕜

The minimax value: the best guarantee Player II can achieve. minimax = inf_y sup_i E(i, y)

Equations

• A.minimax = ⨅ (y : ↑(stdSimplex 𝕜 J)), A.guarantee_II y

Loomis-route theorems (ℝ-only)

These theorems carry the actual content of the von Neumann minimax theorem and are proved by aliasing the simplified-Loomis development in MinimaxLoomis. The Loomis proof uses ℝ-specific compactness / continuity, so the theorems are pinned to ℝ even though their statements (via maximin / minimax above) make sense over any order-complete linearly ordered field.

theorem MatrixGame.maximin_le_minimax {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) : A.maximin ≤ A.minimax

Maximin ≤ minimax (always holds, for any matrix game). This is the finite weak-duality inequality.

theorem MatrixGame.minimax_theorem {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) : A.maximin = A.minimax

Von Neumann's Minimax Theorem: For any finite matrix game, maximin = minimax. [MSZ 5.11, von Neumann 1928]

Proof: the general (positive-B) Loomis theorem specialised to B = 𝟙, exported as [Loomis.minmax_from_general] (compactness + continuity

• strong induction on |I| + |J|).

The field-generic minimax (any linearly ordered field, not just ℝ) is proved separately by von Neumann symmetrisation in [Minimax.minimax] — no compactness, no order completeness.

theorem MatrixGame.minimax_optimal_strategies {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) : ∃ (xx : ↑(stdSimplex ℝ I)) (yy : ↑(stdSimplex ℝ J)) (v : ℝ), (∀ (j : J), A.Ej xx j ≥ v) ∧ ∀ (i : I), A.Ei i yy ≤ v

Existence of optimal mixed strategies: there exist mixed strategies xx for Player I and yy for Player II and a value v such that:

• Player I guarantees at least v: ∀ j, E(xx, j) ≥ v
• Player II limits payoff to at most v: ∀ i, E(i, yy) ≤ v

[MSZ Theorem 5.11, LRS Theorem 2.3.1]