EconCSLib.GameTheory.StrategicGame.MixedStrategy

Mixed strategies and mixed Nash equilibrium for arbitrary player sets, polymorphic in the payoff field U.

Design

• MixedProfile G = a mixed strategy for each player, for any N
• IsCompletelyMixed G p i = player i assigns positive probability to every pure strategy
• IsCompletelyMixedProfile G p = every player is completely mixed
• expectedPayoff G p who = expected payoff (requires [Fintype N] and [∀ i, Fintype (G.strategy i)])
• IsMixedNashEq G p = no player can improve by deviating to any pure strategy

The payoff type U is polymorphic with [Field U] [LinearOrder U] [IsStrictOrderedRing U]. This covers both ℚ (for native_decide-style constructive examples) and ℝ (for the Loomis minimax theorem).

Key Bourbaki point: StrategicGame and MixedProfile have NO finiteness constraints. [Fintype N] is only added to theorems/definitions that need computation.

References

• [MSZ] Chapter 5

Mixed strategies and profiles

@[reducible, inline]

abbrev StrategicGame.MixedStrategy {N : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] (G : StrategicGame N U) (i : N) [Fintype (G.strategy i)] : Set (G.strategy i → U)

A mixed strategy for player i: a probability distribution over pure strategies. Requires [Fintype (G.strategy i)] but NOT [Fintype N].

Equations

• G.MixedStrategy i = stdSimplex U (G.strategy i)

def StrategicGame.MixedProfile {N : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] (G : StrategicGame N U) [(i : N) → Fintype (G.strategy i)] : Type (max (max u_1 u_2) u_3)

A mixed profile: each player has a mixed strategy. No finiteness constraint on N (player set can be arbitrary).

Equations

• G.MixedProfile = ((i : N) → ↑(G.MixedStrategy i))

Complete mixing

def StrategicGame.IsCompletelyMixed {N : Type u_1} (G : StrategicGame N ℚ) {i : N} [Fintype (G.strategy i)] (p : ↑(G.MixedStrategy i)) : Prop

A player's mixed strategy is completely mixed if every pure strategy is assigned positive probability. This is the strategic-form mixed-strategy part of MSZ Definition 7.6.

Equations

• G.IsCompletelyMixed p = ∀ (s : G.strategy i), 0 < ↑p s

def StrategicGame.IsCompletelyMixedProfile {N : Type u_1} (G : StrategicGame N ℚ) [(i : N) → Fintype (G.strategy i)] (p : G.MixedProfile) : Prop

A mixed profile is completely mixed if every player's mixed strategy is completely mixed.

Equations

• G.IsCompletelyMixedProfile p = ∀ (i : N), G.IsCompletelyMixed (p i)

theorem StrategicGame.IsCompletelyMixedProfile.player {N : Type u_1} {G : StrategicGame N ℚ} [(i : N) → Fintype (G.strategy i)] {p : G.MixedProfile} (hp : G.IsCompletelyMixedProfile p) (i : N) : G.IsCompletelyMixed (p i)

A completely mixed profile gives a completely mixed strategy for each player.

Constructors

def StrategicGame.pureToMixed {N : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] [IsStrictOrderedRing U] {G : StrategicGame N U} {i : N} [Fintype (G.strategy i)] [DecidableEq (G.strategy i)] (s₀ : G.strategy i) : ↑(G.MixedStrategy i)

Embed a pure strategy as a mixed strategy (point mass).

Equations

• StrategicGame.pureToMixed s₀ = ⟨fun (s : G.strategy i) => if s = s₀ then 1 else 0, ⋯⟩

def StrategicGame.uniformMixed {N : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] [IsStrictOrderedRing U] {G : StrategicGame N U} {i : N} [Fintype (G.strategy i)] [Nonempty (G.strategy i)] : ↑(G.MixedStrategy i)

The uniform mixed strategy over a finite nonempty strategy set.

Equations

• StrategicGame.uniformMixed = ⟨fun (x : G.strategy i) => 1 / ↑(Fintype.card (G.strategy i)), ⋯⟩

theorem StrategicGame.uniformMixed_apply {N : Type u_1} {G : StrategicGame N ℚ} {i : N} [Fintype (G.strategy i)] [Nonempty (G.strategy i)] (s : G.strategy i) : ↑uniformMixed s = 1 / ↑(Fintype.card (G.strategy i))

The uniform mixed strategy assigns 1 / card to every pure strategy.

theorem StrategicGame.uniformMixed_pos {N : Type u_1} {G : StrategicGame N ℚ} {i : N} [Fintype (G.strategy i)] [Nonempty (G.strategy i)] (s : G.strategy i) : 0 < ↑uniformMixed s

Every pure strategy has positive probability under the uniform mixed strategy.

theorem StrategicGame.uniformMixed_isCompletelyMixed {N : Type u_1} {G : StrategicGame N ℚ} {i : N} [Fintype (G.strategy i)] [Nonempty (G.strategy i)] : G.IsCompletelyMixed uniformMixed

The uniform mixed strategy is completely mixed on any finite nonempty strategy set.

def StrategicGame.uniformMixedProfile {N : Type u_1} (G : StrategicGame N ℚ) [(i : N) → Fintype (G.strategy i)] [∀ (i : N), Nonempty (G.strategy i)] : G.MixedProfile

The profile where every player uses the uniform mixed strategy.

Equations

• G.uniformMixedProfile i = StrategicGame.uniformMixed

theorem StrategicGame.uniformMixedProfile_isCompletelyMixed {N : Type u_1} (G : StrategicGame N ℚ) [(i : N) → Fintype (G.strategy i)] [∀ (i : N), Nonempty (G.strategy i)] : G.IsCompletelyMixedProfile G.uniformMixedProfile

The uniform mixed profile is completely mixed.

theorem StrategicGame.pureToMixed_not_isCompletelyMixed_of_ne {N : Type u_1} {G : StrategicGame N ℚ} {i : N} [Fintype (G.strategy i)] [DecidableEq (G.strategy i)] {s₀ s₁ : G.strategy i} (h : s₁ ≠ s₀) : ¬G.IsCompletelyMixed (pureToMixed s₀)

A point-mass mixed strategy is not completely mixed when there is another pure strategy available.

def StrategicGame.pureProfileToMixed {N : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] [IsStrictOrderedRing U] {G : StrategicGame N U} [(i : N) → Fintype (G.strategy i)] [(i : N) → DecidableEq (G.strategy i)] (σ : G.Profile) : G.MixedProfile

Embed a pure profile as a mixed profile.

Equations

• StrategicGame.pureProfileToMixed σ i = StrategicGame.pureToMixed (σ i)

Expected payoff

def StrategicGame.expectedPayoff {N : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] (G : StrategicGame N U) [Fintype N] [DecidableEq N] [(i : N) → Fintype (G.strategy i)] (p : G.MixedProfile) (who : N) : U

Expected payoff for player who under mixed profile p.

EU(p, who) = ∑_{σ : Profile} (∏_i p_i(σ_i)) · payoff(σ, who)

Requires [Fintype N] (to sum over all profiles) and [∀ i, Fintype (G.strategy i)] (finite strategy sets).

Equations

• G.expectedPayoff p who = ∑ σ : G.Profile, (∏ i : N, ↑(p i) (σ i)) * G.payoff σ who

def StrategicGame.deviateMixed {N : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] [IsStrictOrderedRing U] (G : StrategicGame N U) [(i : N) → Fintype (G.strategy i)] [DecidableEq N] [(i : N) → DecidableEq (G.strategy i)] (p : G.MixedProfile) (who : N) (s' : G.strategy who) : G.MixedProfile

Deviate player who to pure strategy s', keeping others' mixed strategies.

Equations

• G.deviateMixed p who s' = Function.update p who (StrategicGame.pureToMixed s')

Mixed Nash equilibrium

def StrategicGame.IsMixedNashEq {N : Type u_1} {U : Type u_2} [Field U] [LinearOrder U] [IsStrictOrderedRing U] (G : StrategicGame N U) [Fintype N] [DecidableEq N] [(i : N) → Fintype (G.strategy i)] [(i : N) → DecidableEq (G.strategy i)] (p : G.MixedProfile) : Prop

A mixed profile is a mixed Nash equilibrium if no player can improve their expected payoff by deviating to any pure strategy.

By linearity of expected payoff in each player's mixed strategy, checking pure deviations suffices. [MSZ 5.5, 5.18]

Requires [Fintype N] for expected payoff computation.

Equations

• G.IsMixedNashEq p = ∀ (who : N) (s' : G.strategy who), G.expectedPayoff (G.deviateMixed p who s') who ≤ G.expectedPayoff p who