Existence of mixed Nash equilibria

This file defines finite games (FinGame), mixed strategy profiles, and the mixed Nash equilibrium predicate (FinGame.mixedNashEquilibrium). The best-response correspondence is turned into a continuous self-map of the product of strategy simplices, and ExistsNashEq derives the existence of a mixed Nash equilibrium in every finite game from Brouwer's fixed-point theorem on a product of simplices.

structure Game : Type (u + 1)

A game: a finite-or-infinite set of players, each with a set of pure strategies and a real-valued payoff function on the profiles of all players.

• I : Type u

  The set of players.

• HI : Inhabited self.I
• SS : self.I → Type u

  For each player, the set of pure strategies.

• HSS (i : self.I) : Inhabited (self.SS i)
• g : self.I → ((i : self.I) → self.SS i) → ℝ

  The payoff of each player as a function of the strategy profile.

def Game.NashEquilibrium {G : Game} (x : (i : G.I) → G.SS i) : Prop

A strategy profile is a Nash equilibrium if no player can improve unilaterally.

Equations

• Game.NashEquilibrium x = ∀ (i : G.I) (y : (i : G.I) → G.SS i), (∀ (j : G.I), i ≠ j → x j = y j) → G.g i x ≥ G.g i y

@[implicit_reducible]

instance Game.instInhabitedSS {G : Game} {i : G.I} : Inhabited (G.SS i)

Equations

• Game.instInhabitedSS = G.HSS i

structure FinGameextends Game : Type (u + 1)

A finite game: a game with finitely many players and finite strategy sets.

• I : Type u
• HI : Inhabited self.I
• SS : self.I → Type u
• HSS (i : self.I) : Inhabited (self.SS i)
• g : self.I → ((i : self.I) → self.SS i) → ℝ
• FinI : Fintype self.I
• FinSS (i : self.I) : Fintype (self.SS i)

@[implicit_reducible]

instance FinGame.instFintypeI {G : FinGame} : Fintype G.I

Equations

• FinGame.instFintypeI = G.FinI

@[implicit_reducible]

instance FinGame.instFintypeSS {G : FinGame} {i : G.I} : Fintype (G.SS i)

Equations

• FinGame.instFintypeSS = G.FinSS i

@[reducible, inline]

abbrev FinGame.mixedS (G : FinGame) : Type u_1

A mixed strategy profile of a finite game: a simplex point per player.

Equations

• G.mixedS = ((i : G.I) → ↑(stdSimplex ℝ (G.SS i)))

noncomputable def FinGame.mixedG {G : FinGame} (i : G.I) (m : (i : G.I) → ↑(MixedStrategy (G.SS i))) : ℝ

The expected payoff of player i under a mixed strategy profile.

Equations

• FinGame.mixedG i m = ∑ s : (j : G.I) → G.SS j, (∏ j : G.I, (m j) (s j)) * G.g i s

theorem FinGame.mixed_g_linear {G : FinGame} {i : G.I} {x : (a : G.I) → ↑(MixedStrategy (G.SS a))} {y : ↑(MixedStrategy (G.SS i))} : mixedG i (Function.update x i y) = ∑ s : G.SS i, y s * mixedG i (Function.update x i (stdSimplex.pure s))

noncomputable def FinGame.FinGame2MixedGame (G : FinGame) : Game

The mixed extension of a finite game, as a Game on simplices.

Equations

• G.FinGame2MixedGame = { I := G.I, HI := G.HI, SS := fun (i : G.I) => ↑(MixedStrategy (G.SS i)), HSS := inferInstance, g := FinGame.mixedG }

def FinGame.termμ_ : Lean.ParserDescr

Notation μ G for the mixed extension of a finite game G.

Equations

• FinGame.termμ_ = Lean.ParserDescr.node `FinGame.termμ_ 999 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "μ") (Lean.ParserDescr.cat `term 60))

def FinGame.mixedNashEquilibrium {G : FinGame} (x : G.mixedS) : Prop

A mixed strategy profile is a Nash equilibrium of the mixed game.

Equations

• FinGame.mixedNashEquilibrium x = ∀ (i : G.I) (y : ↑(MixedStrategy (G.SS i))), FinGame.mixedG i x ≥ FinGame.mixedG i (Function.update x i y)

def reindex {G : FinGame} {n : ℕ} (eI : G.I ≃ Fin n) : G.mixedS → (k : Fin n) → ↑(stdSimplex ℝ (G.SS (eI.symm k)))

Reindex a mixed strategy profile along an equivalence G.I ≃ Fin n.

Equations

• reindex eI x k = x (eI.symm k)

def reindexInv {G : FinGame} {n : ℕ} (eI : G.I ≃ Fin n) : ((k : Fin n) → ↑(stdSimplex ℝ (G.SS (eI.symm k)))) → G.mixedS

The inverse of reindex, transporting along the equivalence.

Equations

• reindexInv eI z i = ⋯ ▸ z (eI i)

theorem reindex_right_inv {G : FinGame} {n : ℕ} (eI : G.I ≃ Fin n) (y : (k : Fin n) → ↑(stdSimplex ℝ (G.SS (eI.symm k)))) : reindex eI (reindexInv eI y) = y

theorem reindex_left_inv {G : FinGame} {n : ℕ} (eI : G.I ≃ Fin n) : have reindex := fun (w : G.mixedS) (k : Fin n) => w (eI.symm k); have reindexInv := fun (z : (k : Fin n) → ↑(stdSimplex ℝ (G.SS (eI.symm k)))) (i : G.I) => ⋯ ▸ z (eI i); ∀ (x : G.mixedS), reindexInv (reindex x) = x

def mapSimplex {n : Type u_1} {m : Type u_2} [Fintype n] [Fintype m] (e : n ≃ m) : ↑(stdSimplex ℝ n) → ↑(stdSimplex ℝ m)

Lifts an equivalence e : n ≃ m to a function between simplices.

Equations

• mapSimplex e x = ⟨fun (i : m) => ↑x (e.symm i), ⋯⟩

@[simp]

theorem map_simplex_apply {n : Type u_1} {m : Type u_2} [Fintype n] [Fintype m] (e : n ≃ m) (x : ↑(stdSimplex ℝ n)) (i : m) : ↑(mapSimplex e x) i = ↑x (e.symm i)

def mapSimplexEquiv {n : Type u_1} {m : Type u_2} [Fintype n] [Fintype m] (e : n ≃ m) : ↑(stdSimplex ℝ n) ≃ ↑(stdSimplex ℝ m)

The simplex map induced by an equivalence is itself an equivalence.

Equations

• mapSimplexEquiv e = { toFun := mapSimplex e, invFun := mapSimplex e.symm, left_inv := ⋯, right_inv := ⋯ }

def mapMixedSEquiv {G : FinGame} (e : (i : G.I) → G.SS i ≃ Fin (Fintype.card (G.SS i))) : G.mixedS ≃ ((i : G.I) → ↑(stdSimplex ℝ (Fin (Fintype.card (G.SS i)))))

Lifts component-wise equivalences to an equivalence on the space of mixed strategies.

Equations

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

theorem Brouwer.mixedGame {G : FinGame} (f : G.mixedS → G.mixedS) (hf : Continuous f) : ∃ (x : G.mixedS), f x = x

@[reducible, inline]

noncomputable abbrev gFunction {G : FinGame} (i : G.I) (σ : G.mixedS) (a : G.SS i) : ℝ

The best-response improvement map used to build the Nash fixed-point map.

Equations

• gFunction i σ a = (σ i) a + max 0 (FinGame.mixedG i (Function.update σ i (stdSimplex.pure a)) - FinGame.mixedG i σ)

theorem sigma_le_g_function {G : FinGame} (i : G.I) (σ : G.mixedS) (a : G.SS i) : (σ i) a ≤ gFunction i σ a

theorem g_function_noneg {G : FinGame} (i : G.I) (σ : G.mixedS) (a : G.SS i) : 0 ≤ gFunction i σ a

theorem one_le_sum_g {G : FinGame} (i : G.I) (σ : G.mixedS) : 1 ≤ ∑ b : G.SS i, gFunction i σ b

@[reducible, inline]

noncomputable abbrev nashMapAux {G : FinGame} (σ : G.mixedS) (i : G.I) (a : G.SS i) : ℝ

The unnormalized best-response update on a product of strategy simplices.

Equations

• nashMapAux σ i a = gFunction i σ a / ∑ b : G.SS i, gFunction i σ b

theorem nash_map_cert {G : FinGame} (σ : G.mixedS) (i : G.I) : nashMapAux σ i ∈ MixedStrategy (G.SS i)

noncomputable def nashMap (G : FinGame) (σ : G.mixedS) : G.mixedS

The continuous self-map of the strategy product whose fixed points are Nash equilibria.

Equations

• nashMap G σ i = ⟨nashMapAux σ i, ⋯⟩

theorem cg (G : FinGame) {i : G.I} {s : G.SS i} : Continuous fun (a : G.mixedS) => gFunction i a s

theorem nash_map_cont (G : FinGame) : Continuous (nashMap G)

theorem ExistsNashEq (G : FinGame) : ∃ (σ : G.mixedS), FinGame.mixedNashEquilibrium σ