Lean declarations

def IsNashEquilibrium EconCSLib @ cef01c7, EconCSLib.GameTheory.StrategicGame.NashEquilibrium

def IsNashEquilibrium (G : StrategicGame N U) (σ : G.Profile) : Prop :=
  ∀ i : N, IsBestResponse G σ i

def isNashEq EconCSLib @ cef01c7, EconCSLib.GameTheory.StrategicGame.Checker

def isNashEq [Fintype N] (G : StrategicGame N U) [∀ i, Fintype (G.strategy i)]
    (σ : G.Profile) : Bool :=
  decide (∀ i : N, ∀ s' : G.strategy i, G.payoff (deviate σ i s') i ≤ G.payoff σ i)

theorem isNashEq_iff EconCSLib @ cef01c7, EconCSLib.GameTheory.StrategicGame.Checker

T6: The checker correctly decides Nash equilibrium (soundness and completeness).

theorem isNashEq_iff [Fintype N] (G : StrategicGame N U) [∀ i, Fintype (G.strategy i)]
    (σ : G.Profile) :
    isNashEq G σ = true ↔ IsNashEquilibrium G σ

Modules: EconCSLib.GameTheory.StrategicGame.NashEquilibrium, EconCSLib.GameTheory.StrategicGame.Checker

Nash Equilibrium

A strategy profile $\sigma$ is a Nash equilibrium if every player is playing a best response to the strategies of the other players:

$$\forall i \in I, \quad \sigma_i \text{ is a best response to } \sigma.$$

Equivalently, no player can improve their payoff by a unilateral deviation.

References

[MSZ, Chapter 2, Section 2.4] Maschler, Solan, and Zamir, Game Theory. Definition of Nash equilibrium in pure strategies.

Nash Equilibrium

References

Used by

Also in