EconCSLib.GameTheory.StrategicGame.ZeroSum.MatrixGameNash

Existence of a mixed Nash equilibrium for a finite matrix game.

Main statements

• MatrixGame.IsMixedNashEq xx yy — saddle-point definition: xx is a best response to yy for the row player, and yy is a best response to xx for the column player (zero-sum convention: column player minimises the same A).
• MatrixGame.exists_mixed_nash_equilibrium — every finite matrix game over any linearly ordered field has a pair (xx, yy) satisfying IsMixedNashEq; packaged from Minimax.minimax (von Neumann symmetrisation).
• MatrixGame.toStrategicGame — the explicit two-player zero-sum strategic game whose mixed Nash equilibria correspond to saddle points of A.

The intermediate IsMixedNashEq defined here is on the matrix game itself (not on the strategic-game embedding) because it is exactly the textbook statement of "matrix game has a value" and is easier to reason about than the dependently-typed Fin 2-indexed strategic game.

References

• [MSZ] Maschler, Solan, Zamir, Game Theory, Theorems 5.11 and 5.13.
• [LRS] Laraki, Renault, Sorin, Mathematical Foundations of Game Theory, Theorem 2.3.1.

Saddle-point mixed Nash equilibrium

def MatrixGame.IsMixedNashEq {I J : Type u} [Fintype I] [Fintype J] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (A : MatrixGame I J 𝕜) (xx : ↑(stdSimplex 𝕜 I)) (yy : ↑(stdSimplex 𝕜 J)) : Prop

Saddle-point form of a mixed Nash equilibrium for a matrix game.

For zero-sum two-player games, the standard mixed-strategy Nash equilibrium is exactly the saddle point of the bilinear payoff: the row player cannot improve by deviating to any mixed row, and the column player cannot improve (i.e., decrease the row player's payoff) by deviating to any mixed column.

Field-generic: the saddle-point inequalities only need a linearly ordered field, not order-completeness.

Equations

• A.IsMixedNashEq xx yy = ((∀ (x' : ↑(stdSimplex 𝕜 I)), A.E x' yy ≤ A.E xx yy) ∧ ∀ (y' : ↑(stdSimplex 𝕜 J)), A.E xx yy ≤ A.E xx y')

@[reducible, inline]

abbrev MatrixGame.IsSaddlePoint {I J : Type u} [Fintype I] [Fintype J] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (A : MatrixGame I J 𝕜) (xx : ↑(stdSimplex 𝕜 I)) (yy : ↑(stdSimplex 𝕜 J)) : Prop

A pair of mixed strategies is a saddle point when player I's payoff is maximised by the row strategy against the column strategy and minimised by the column strategy against the row strategy. For a matrix game this is synonymous with the mixed Nash equilibrium predicate [MatrixGame.IsMixedNashEq].

Equations

• A.IsSaddlePoint xx yy = A.IsMixedNashEq xx yy

theorem MatrixGame.isMixedNashEq_iff_isSaddlePoint {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (A : MatrixGame I J 𝕜) (xx : ↑(stdSimplex 𝕜 I)) (yy : ↑(stdSimplex 𝕜 J)) : A.IsMixedNashEq xx yy ↔ A.IsSaddlePoint xx yy

Nash equilibrium ↔ saddle point for matrix games. Both sides unfold to the same saddle-point inequality system; the equivalence is therefore definitional.

noncomputable def MatrixGame.value {I J : Type u} [Fintype I] [Fintype J] [Nonempty J] {𝕜 : Type} [Field 𝕜] [ConditionallyCompleteLinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (A : MatrixGame I J 𝕜) : 𝕜

The value of a matrix game (sSup-based; needs order completeness).

Equal to both maximin and minimax by the minimax theorem ([MatrixGame.minimax_theorem]); the maximin = minimax equality is the ℝ-bound piece (Loomis). Field-generic existence of a value (without sSup) is the IsValue predicate in Minimax.lean.

Equations

• A.value = A.maximin

theorem MatrixGame.value_eq_maximin {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] {𝕜 : Type} [Field 𝕜] [ConditionallyCompleteLinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (A : MatrixGame I J 𝕜) : A.value = A.maximin

theorem MatrixGame.value_eq_minimax {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) : A.value = A.minimax

noncomputable def MatrixGame.dualityGap {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (A : MatrixGame I J 𝕜) (xx : ↑(stdSimplex 𝕜 I)) (yy : ↑(stdSimplex 𝕜 J)) : 𝕜

Point-wise duality gap at a strategy pair: the column player's realised loss-cap minus the row player's realised guarantee. Always nonnegative, zero exactly at optimal pairs.

Field-generic: just the difference of two L2 guarantees, no sup/inf.

Equations

• A.dualityGap xx yy = A.guarantee_II yy - A.guarantee_I xx

def MatrixGame.optimalRowStrategies {I J : Type u} [Fintype I] [Fintype J] [Nonempty J] {𝕜 : Type} [Field 𝕜] [ConditionallyCompleteLinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (A : MatrixGame I J 𝕜) : Set ↑(stdSimplex 𝕜 I)

The set of optimal row strategies: mixed strategies that achieve the maximin value.

Equations

• A.optimalRowStrategies = {xx : ↑(stdSimplex 𝕜 I) | A.guarantee_I xx = A.value}

def MatrixGame.optimalColumnStrategies {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] {𝕜 : Type} [Field 𝕜] [ConditionallyCompleteLinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (A : MatrixGame I J 𝕜) : Set ↑(stdSimplex 𝕜 J)

The set of optimal column strategies: mixed strategies that achieve the minimax value.

Equations

• A.optimalColumnStrategies = {yy : ↑(stdSimplex 𝕜 J) | A.guarantee_II yy = A.value}

def MatrixGame.IsEpsilonOptimalRow {I J : Type u} [Fintype I] [Fintype J] [Nonempty J] {𝕜 : Type} [Field 𝕜] [ConditionallyCompleteLinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (A : MatrixGame I J 𝕜) (ε : 𝕜) (xx : ↑(stdSimplex 𝕜 I)) : Prop

An ε-optimal row strategy guarantees at least value - ε.

Equations

• A.IsEpsilonOptimalRow ε xx = (A.value - ε ≤ A.guarantee_I xx)

def MatrixGame.IsEpsilonOptimalColumn {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] {𝕜 : Type} [Field 𝕜] [ConditionallyCompleteLinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (A : MatrixGame I J 𝕜) (ε : 𝕜) (yy : ↑(stdSimplex 𝕜 J)) : Prop

An ε-optimal column strategy caps player I's payoff at value + ε.

Equations

• A.IsEpsilonOptimalColumn ε yy = (A.guarantee_II yy ≤ A.value + ε)

def MatrixGame.IsPlayerIGuarantee {I J : Type u} [Fintype I] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (A : MatrixGame I J 𝕜) (w : 𝕜) : Prop

w is a guarantee for player I when some mixed row strategy achieves expected payoff ≥ w against every pure column. Equivalent to w ≤ A.maximin.

Equations

• A.IsPlayerIGuarantee w = ∃ (xx : ↑(stdSimplex 𝕜 I)), ∀ (j : J), w ≤ A.Ej xx j

def MatrixGame.IsPlayerIIGuarantee {I J : Type u} [Fintype J] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (A : MatrixGame I J 𝕜) (w : 𝕜) : Prop

w is a guarantee for player II when some mixed column strategy caps expected payoff ≤ w against every pure row. Equivalent to A.minimax ≤ w.

Equations

• A.IsPlayerIIGuarantee w = ∃ (yy : ↑(stdSimplex 𝕜 J)), ∀ (i : I), A.Ei i yy ≤ w

noncomputable def MatrixGame.support {I : Type u} [Fintype I] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [DecidableEq I] (xx : ↑(stdSimplex 𝕜 I)) : Finset I

Support of a mixed strategy: the indices with positive probability.

Equations

• MatrixGame.support xx = {i : I | 0 < ↑xx i}

Optimal pairs ↔ saddle points

theorem MatrixGame.mem_optimalRowStrategies_iff_E_ge {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) (xx : ↑(stdSimplex ℝ I)) : xx ∈ A.optimalRowStrategies ↔ ∀ (y' : ↑(stdSimplex ℝ J)), A.value ≤ A.E xx y'

A row strategy is optimal iff against every mixed column it secures the value.

theorem MatrixGame.mem_optimalColumnStrategies_iff_E_le {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) (yy : ↑(stdSimplex ℝ J)) : yy ∈ A.optimalColumnStrategies ↔ ∀ (x' : ↑(stdSimplex ℝ I)), A.E x' yy ≤ A.value

A column strategy is optimal iff against every mixed row it caps payoff at the value.

theorem MatrixGame.support_complementarity_row {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) [DecidableEq I] (xx : ↑(stdSimplex ℝ I)) (yy : ↑(stdSimplex ℝ J)) (hxx : xx ∈ A.optimalRowStrategies) (hyy : yy ∈ A.optimalColumnStrategies) {i : I} (hi : 0 < ↑xx i) : A.Ei i yy = A.value

Support complementarity (row). For an optimal pair (xx, yy), every row i with positive probability under xx is a best response to yy, i.e., A.Ei i yy = A.value.

theorem MatrixGame.support_complementarity_column {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) [DecidableEq J] (xx : ↑(stdSimplex ℝ I)) (yy : ↑(stdSimplex ℝ J)) (hxx : xx ∈ A.optimalRowStrategies) (hyy : yy ∈ A.optimalColumnStrategies) {j : J} (hj : 0 < ↑yy j) : A.Ej xx j = A.value

Support complementarity (column). For an optimal pair (xx, yy), every column j with positive probability under yy is a best response to xx, i.e., A.Ej xx j = A.value.

theorem MatrixGame.common_guarantee_eq_value {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) (w : ℝ) (h1 : A.IsPlayerIGuarantee w) (h2 : A.IsPlayerIIGuarantee w) : w = A.value

Common guarantee gives the value. If both players guarantee the same scalar w, then w equals the game value.

theorem MatrixGame.optimal_pairs_iff_saddle_point {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) (xx : ↑(stdSimplex ℝ I)) (yy : ↑(stdSimplex ℝ J)) : xx ∈ A.optimalRowStrategies ∧ yy ∈ A.optimalColumnStrategies ↔ A.IsSaddlePoint xx yy

Optimal pairs ↔ saddle points. A pair of mixed strategies is in the product X(A) × Y(A) of optimal strategy sets iff it is a saddle point.

Existence

theorem MatrixGame.isMixedNashEq_of_pure {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (A : MatrixGame I J 𝕜) {xx : ↑(stdSimplex 𝕜 I)} {yy : ↑(stdSimplex 𝕜 J)} {v : 𝕜} (Hxx : ∀ (j : J), v ≤ wsum xx fun (i : I) => A.g i j) (Hyy : ∀ (i : I), wsum yy (A.g i) ≤ v) : A.IsMixedNashEq xx yy

Pure-strategy guarantees give a mixed Nash equilibrium. If xx guarantees value v against every pure column and yy caps the row player's payoff at v against every pure row, then (xx, yy) is a saddle-point mixed Nash equilibrium. Field-generic — only the saddle inequalities are used (no order-completeness).

theorem MatrixGame.exists_mixed_nash_equilibrium {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (A : MatrixGame I J 𝕜) : ∃ (xx : ↑(stdSimplex 𝕜 I)) (yy : ↑(stdSimplex 𝕜 J)), A.IsMixedNashEq xx yy

Matrix games have a mixed Nash equilibrium — over any linearly ordered field. Packages the field-generic saddle Minimax.minimax (proved by von Neumann symmetrisation; no compactness, no order-completeness) into the IsMixedNashEq saddle-point form. The ℝ case is the 𝕜 := ℝ instance, so all ℝ consumers are unaffected.

Strategic-game embedding

A matrix game A : I → J → 𝕜 lifts to a two-player zero-sum strategic game with players Fin 2, strategy spaces I and J, and payoffs A (for the row player) and −A (for the column player). Polymorphic in the scalar field 𝕜. The standard [StrategicGame.IsMixedNashEq] then unfolds — modulo a 2-player profile expansion — to the saddle-point form MatrixGame.IsMixedNashEq above.

noncomputable def MatrixGame.toStrategicGame {I J : Type u} {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (A : MatrixGame I J 𝕜) : StrategicGame (Fin 2) 𝕜

The two-player zero-sum strategic game associated with a matrix game.

See MatrixGame.toStrategicGame_isZeroSum for the proof that this game satisfies the abstract StrategicGame.IsZeroSum predicate, so results stated against IsZeroSum (e.g. IsZeroSum.nash_payoff_eq) can be invoked on A.toStrategicGame without re-unfolding the definition.

Equations

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

theorem MatrixGame.toStrategicGame_isZeroSum {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (A : MatrixGame I J 𝕜) : A.toStrategicGame.IsZeroSum

A.toStrategicGame satisfies the abstract zero-sum predicate: by construction player 1's payoff is the negation of player 0's.

toStrategicGame instance synthesis

@[implicit_reducible]

instance MatrixGame.instDecidableEqStrategyFinOfNatNatToStrategicGame {I J : Type u} {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (A : MatrixGame I J 𝕜) [DecidableEq I] [DecidableEq J] (i : Fin 2) : DecidableEq (A.toStrategicGame.strategy i)

Equations

• A.instDecidableEqStrategyFinOfNatNatToStrategicGame 0 = inst✝¹
• A.instDecidableEqStrategyFinOfNatNatToStrategicGame 1 = inst✝

@[implicit_reducible]

instance MatrixGame.instFintypeStrategyFinOfNatNatToStrategicGame {I J : Type u} [Fintype I] [Fintype J] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (A : MatrixGame I J 𝕜) (i : Fin 2) : Fintype (A.toStrategicGame.strategy i)

Equations

• A.instFintypeStrategyFinOfNatNatToStrategicGame 0 = inst✝⁴
• A.instFintypeStrategyFinOfNatNatToStrategicGame 1 = inst✝³

instance MatrixGame.instNonemptyStrategyFinOfNatNatToStrategicGame {I J : Type u} [Nonempty I] [Nonempty J] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (A : MatrixGame I J 𝕜) (i : Fin 2) : Nonempty (A.toStrategicGame.strategy i)

noncomputable def MatrixGame.toMixedProfile {I J : Type u} [Fintype I] [Fintype J] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (A : MatrixGame I J 𝕜) (xx : ↑(stdSimplex 𝕜 I)) (yy : ↑(stdSimplex 𝕜 J)) : A.toStrategicGame.MixedProfile

Build a MixedProfile of toStrategicGame from a saddle-point pair.

Equations

• A.toMixedProfile xx yy 0 = xx
• A.toMixedProfile xx yy 1 = yy

@[simp]

theorem MatrixGame.toMixedProfile_zero {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] [DecidableEq I] [DecidableEq J] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (A : MatrixGame I J 𝕜) (xx : ↑(stdSimplex 𝕜 I)) (yy : ↑(stdSimplex 𝕜 J)) : A.toMixedProfile xx yy 0 = xx

@[simp]

theorem MatrixGame.toMixedProfile_one {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] [DecidableEq I] [DecidableEq J] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (A : MatrixGame I J 𝕜) (xx : ↑(stdSimplex 𝕜 I)) (yy : ↑(stdSimplex 𝕜 J)) : A.toMixedProfile xx yy 1 = yy

Profile expansion for Fin 2

Player-0's strategic-game expected payoff on toStrategicGame reduces to A.E, and player-1's to -A.E. This is the technical core of the bridge from saddle-point Nash to StrategicGame.IsMixedNashEq.

theorem MatrixGame.expectedPayoff_toStrategicGame_zero {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] [DecidableEq I] [DecidableEq J] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (A : MatrixGame I J 𝕜) (p : A.toStrategicGame.MixedProfile) : A.toStrategicGame.expectedPayoff p 0 = A.E (p 0) (p 1)

Bridge lemma: expectedPayoff A.toStrategicGame p 0 = A.E (p 0) (p 1). Reduces both sides to the canonical double sum ∑ i, ∑ j, (p 0)ᵢ · (p 1)ⱼ · A i j.

theorem MatrixGame.expectedPayoff_toStrategicGame_one {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] [DecidableEq I] [DecidableEq J] {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (A : MatrixGame I J 𝕜) (p : A.toStrategicGame.MixedProfile) : A.toStrategicGame.expectedPayoff p 1 = -A.E (p 0) (p 1)

Mirror: expectedPayoff A.toStrategicGame p 1 = -(A.E (p 0) (p 1)).

Main theorem: mixed Nash equilibrium of the embedded strategic game

theorem MatrixGame.exists_strategic_game_nash_equilibrium {I J : Type u} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) [DecidableEq I] [DecidableEq J] : ∃ (p : A.toStrategicGame.MixedProfile), A.toStrategicGame.IsMixedNashEq p

The strategic-game embedding of a finite matrix game admits a mixed Nash equilibrium. Combines MatrixGame.exists_mixed_nash_equilibrium with the profile-expansion bridge lemmas above.