EconCSLib.GameTheory.StrategicGame.Nash

Best-response map (nash_map) for n-player finite strategic games, and its continuity. Together with Brouwer's fixed-point theorem these are the two ingredients for the Nash existence theorem (SG-L2 #199).

Main definitions

• evaluate_at_mixed G i σ — expected payoff of player i under mixed profile σ; equals ∑_{s : Profile G} (∏_j σ_j(s_j)) · G.payoff s i.
• mixed_g G i m — the multilinear payoff functional on arbitrary weight vectors m : ∀ i, G.strategy i → ℝ; used as an intermediate form inside proofs.
• g_function G i σ a — the augmented weight σ_i(a) + max 0 (EU(σ[i↦a]) - EU(σ)).
• nash_map G σ — the best-response map; normalizes g_function to a mixed profile. It is a continuous self-map on the product of standard simplices.
• mixedNashEquilibrium G σ — σ is a mixed Nash equilibrium of G.

Main results

• sigma_le_g_function — σ_i(a) ≤ g_function i σ a (pointwise lower bound).
• g_function_nonneg — 0 ≤ g_function i σ a.
• one_le_sum_g — 1 ≤ ∑_a g_function i σ a.
• nash_map_cert — the normalized weights form a valid probability distribution.
• nash_map_cont — nash_map G is continuous.
• exists_mixed_nash_equilibrium_finite — every finite n-player strategic game has a mixed Nash equilibrium (proved via Brouwer_Product).

Design

We work with the raw type ∀ i, stdSimplex ℝ (G.strategy i) (the product of standard simplices) rather than the defined MixedProfile G, so that Lean's type-class machinery automatically finds the product topology. The payoff convention follows EconCSLib: G.payoff s i is player i's payoff at pure profile s.

References

• [Nash 1951] J. Nash, "Non-cooperative Games", Ann. Math. 54(2):286–295.
• Source: math-xmum/Brouwer/Gametheory/Nash.lean.
• [MFoGT §4.6.2] Maschler, Solan, Zamir, Game Theory, Brouwer-based Nash existence.

@[reducible, inline]

abbrev StrategicGame.MixedS {N : Type u_1} (G : StrategicGame N ℝ) [(i : N) → Fintype (G.strategy i)] : Type (max u_1 u_2)

Type abbreviation for the product of standard simplices (one per player), used throughout this file. Defined as an abbrev so Lean unfolds it automatically for topology and continuity instances.

Equations

• G.MixedS = ((i : N) → ↑(stdSimplex ℝ (G.strategy i)))

Mixed-payoff functional

def StrategicGame.evaluate_at_mixed {N : Type u_1} (G : StrategicGame N ℝ) [Fintype N] [DecidableEq N] [(i : N) → Fintype (G.strategy i)] (i : N) (σ : G.MixedS) : ℝ

Expected payoff of player i under mixed profile σ. Sums over all pure profiles, weighting by the product of each player's probability.

Equations

• G.evaluate_at_mixed i σ = ∑ s : G.Profile, (∏ j : N, ↑(σ j) (s j)) * G.payoff s i

def StrategicGame.mixed_g {N : Type u_1} (G : StrategicGame N ℝ) [Fintype N] [DecidableEq N] [(i : N) → Fintype (G.strategy i)] (i : N) (m : (i : N) → G.strategy i → ℝ) : ℝ

Multilinear payoff functional on raw weight vectors m : ∀ i, G.strategy i → ℝ. Same as evaluate_at_mixed but with arbitrary (not necessarily probability-normalized) weights; used inside continuity arguments.

Equations

• G.mixed_g i m = ∑ s : G.Profile, (∏ j : N, m j (s j)) * G.payoff s i

theorem StrategicGame.evaluate_at_mixed_eq_mixed_g {N : Type u_1} (G : StrategicGame N ℝ) [Fintype N] [DecidableEq N] [(i : N) → Fintype (G.strategy i)] [(i : N) → DecidableEq (G.strategy i)] [(i : N) → Inhabited (G.strategy i)] (i : N) (σ : G.MixedS) : G.evaluate_at_mixed i σ = G.mixed_g i fun (j : N) => ↑(σ j)

evaluate_at_mixed is the restriction of mixed_g to simplex weights.

Best-response augmentation

noncomputable def StrategicGame.g_function {N : Type u_1} (G : StrategicGame N ℝ) [Fintype N] [DecidableEq N] [(i : N) → Fintype (G.strategy i)] [(i : N) → DecidableEq (G.strategy i)] (i : N) (σ : G.MixedS) (a : G.strategy i) : ℝ

Augmented weight for pure strategy a of player i at mixed profile σ: the original probability σ_i(a) plus the positive part of the gain from deviating to pure strategy a.

Equations

• G.g_function i σ a = ↑(σ i) a + max 0 (G.evaluate_at_mixed i (Function.update σ i (stdSimplex.pure a)) - G.evaluate_at_mixed i σ)

theorem StrategicGame.sigma_le_g_function {N : Type u_1} (G : StrategicGame N ℝ) [Fintype N] [DecidableEq N] [(i : N) → Fintype (G.strategy i)] [(i : N) → DecidableEq (G.strategy i)] [(i : N) → Inhabited (G.strategy i)] (i : N) (σ : G.MixedS) (a : G.strategy i) : ↑(σ i) a ≤ G.g_function i σ a

The augmented weight is at least σ_i(a).

theorem StrategicGame.g_function_nonneg {N : Type u_1} (G : StrategicGame N ℝ) [Fintype N] [DecidableEq N] [(i : N) → Fintype (G.strategy i)] [(i : N) → DecidableEq (G.strategy i)] [(i : N) → Inhabited (G.strategy i)] (i : N) (σ : G.MixedS) (a : G.strategy i) : 0 ≤ G.g_function i σ a

The augmented weight is nonnegative.

theorem StrategicGame.one_le_sum_g {N : Type u_1} (G : StrategicGame N ℝ) [Fintype N] [DecidableEq N] [(i : N) → Fintype (G.strategy i)] [(i : N) → DecidableEq (G.strategy i)] [(i : N) → Inhabited (G.strategy i)] (i : N) (σ : G.MixedS) : 1 ≤ ∑ a : G.strategy i, G.g_function i σ a

The sum of augmented weights is at least 1.

Nash map

theorem StrategicGame.nash_map_cert {N : Type u_1} (G : StrategicGame N ℝ) [Fintype N] [DecidableEq N] [(i : N) → Fintype (G.strategy i)] [(i : N) → DecidableEq (G.strategy i)] [(i : N) → Inhabited (G.strategy i)] (σ : G.MixedS) (i : N) : StrategicGame.nash_map_aux✝ G σ i ∈ stdSimplex ℝ (G.strategy i)

The normalized augmented weights form a valid probability distribution on G.strategy i.

noncomputable def StrategicGame.nash_map {N : Type u_1} (G : StrategicGame N ℝ) [Fintype N] [DecidableEq N] [(i : N) → Fintype (G.strategy i)] [(i : N) → DecidableEq (G.strategy i)] [(i : N) → Inhabited (G.strategy i)] (σ : G.MixedS) : G.MixedS

The Nash best-response map: sends a mixed profile σ to the profile where each player i plays proportional to g_function i σ. A fixed point of this map is a mixed Nash equilibrium.

Equations

• G.nash_map σ i = ⟨StrategicGame.nash_map_aux✝ G σ i, ⋯⟩

Continuity

theorem StrategicGame.nash_map_cont {N : Type u_1} (G : StrategicGame N ℝ) [Fintype N] [DecidableEq N] [(i : N) → Fintype (G.strategy i)] [(i : N) → DecidableEq (G.strategy i)] [(i : N) → Inhabited (G.strategy i)] : Continuous G.nash_map

nash_map G is a continuous self-map of the product simplex.

Nash equilibrium predicate and existence theorem

theorem StrategicGame.evaluate_at_mixed_linear {N : Type u_1} (G : StrategicGame N ℝ) [Fintype N] [DecidableEq N] [(i : N) → Fintype (G.strategy i)] [(i : N) → DecidableEq (G.strategy i)] [(i : N) → Inhabited (G.strategy i)] (i : N) (σ : G.MixedS) (τ : ↑(stdSimplex ℝ (G.strategy i))) : G.evaluate_at_mixed i (Function.update σ i τ) = ∑ a : G.strategy i, ↑τ a * G.evaluate_at_mixed i (Function.update σ i (stdSimplex.pure a))

evaluate_at_mixed G i is linear in the i-th mixed strategy: for any τ : stdSimplex ℝ (G.strategy i), evaluate_at_mixed G i (update σ i τ) = ∑ a, (τ.val a) * evaluate_at_mixed G i (update σ i (stdSimplex.pure a)).

def StrategicGame.mixedNashEquilibrium {N : Type u_1} [DecidableEq N] (G : StrategicGame N ℝ) [Fintype N] [(i : N) → Fintype (G.strategy i)] : G.MixedS → Prop

Nash equilibrium predicate at the mixed-profile level: σ is a Nash equilibrium of G if no player i can improve by unilaterally deviating to any mixed strategy τ.

Equations

• G.mixedNashEquilibrium σ = ∀ (i : N) (τ : ↑(stdSimplex ℝ (G.strategy i))), G.evaluate_at_mixed i (Function.update σ i τ) ≤ G.evaluate_at_mixed i σ

theorem StrategicGame.exists_mixed_nash_equilibrium_finite {N : Type u_1} [Fintype N] [DecidableEq N] (G : StrategicGame N ℝ) [Fintype N] [DecidableEq N] [(i : N) → Fintype (G.strategy i)] [(i : N) → DecidableEq (G.strategy i)] [(i : N) → Inhabited (G.strategy i)] [Inhabited N] : ∃ (σ : G.MixedS), G.mixedNashEquilibrium σ

Main theorem: every finite n-player strategic game has a mixed Nash equilibrium.

Proof: transport nash_map G via player-index and strategy equivalences to a continuous self-map of ProductSimplices card' (where the players are reindexed as Fin n and card' k = |G.strategy (eI.symm k)|), apply Brouwer_Product to get a fixed point, transport back to MixedS G, and use the fixed-point equation to certify Nash equilibrium.