EconCSLib.GameTheory.StrategicGame.Checker

Executable Nash equilibrium checker for finite strategic games.

Main definitions

• isNashEq — Bool-valued Nash checker
• isNashEq_iff — soundness and completeness: isNashEq G σ = true ↔ IsNashEquilibrium G σ

def isNashEq {N : Type u_1} {U : Type u_2} [DecidableEq N] [Preorder U] [DecidableRel fun (x1 x2 : U) => x1 ≤ x2] [Fintype N] (G : StrategicGame N U) [(i : N) → Fintype (G.strategy i)] (σ : G.Profile) : Bool

Executable Nash equilibrium checker. Returns true iff σ is a pure Nash equilibrium of G.

Equations

• isNashEq G σ = decide (∀ (i : N) (s' : G.strategy i), G.payoff (StrategicGame.deviate σ i s') i ≤ G.payoff σ i)

theorem isNashEq_iff {N : Type u_1} {U : Type u_2} [DecidableEq N] [Preorder U] [DecidableRel fun (x1 x2 : U) => x1 ≤ x2] [Fintype N] (G : StrategicGame N U) [(i : N) → Fintype (G.strategy i)] (σ : G.Profile) : isNashEq G σ = true ↔ IsNashEquilibrium G σ

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