EconCSLib.GameTheory.StrategicGame.NashEquilibrium #
A profile is a pure Nash equilibrium if every player is playing a best response.
Main definitions #
IsNashEquilibrium— every player is a best responder
Main results #
- T3:
IsNashEquilibrium.of_dominant— a dominant profile is Nash
def
IsNashEquilibrium
{N : Type u_1}
{U : Type u_2}
[DecidableEq N]
[Preorder U]
(G : StrategicGame N U)
(σ : G.Profile)
:
A profile σ is a pure Nash equilibrium of game G if every player is playing
a best response: no player can profitably deviate.
Equations
- IsNashEquilibrium G σ = ∀ (i : N), IsBestResponse G σ i
Instances For
theorem
IsNashEquilibrium.of_dominant
{N : Type u_1}
{U : Type u_2}
[DecidableEq N]
[Preorder U]
{G : StrategicGame N U}
{σ : G.Profile}
(h : ∀ (i : N), IsWeaklyDominant G i (σ i))
:
T3: If every player has a weakly dominant strategy and σ assigns each player
their dominant strategy, then σ is a Nash equilibrium.