EconCSLib.GameTheory.StrategicGame.IESDS

Iterated elimination of strictly dominated strategies (IESDS) and rationalizability.

Main definitions

• Survives G n i s — strategy s survives round n of elimination
• IsRationalizable G i s — survives all rounds
• IsDominanceSolvable G — IESDS yields a unique profile

Main results

• survives_mono — survival is monotone decreasing in rounds
• nash_implies_rationalizable — Nash strategies are rationalizable [MSZ 4.31]

References

• [MSZ] Section 4.2, Theorems 4.31, 4.33, 4.37

def StrategicGame.Survives {N : Type u_1} {U : Type u_2} [DecidableEq N] [Preorder U] (G : StrategicGame N U) : ℕ → (i : N) → G.strategy i → Prop

A strategy survives round n of iterated strict dominance elimination. Round 0: all strategies survive. Round n+1: s survives if it survived round n and is not strictly dominated by any round-n survivor.

Equations

• One or more equations did not get rendered due to their size.
• G.Survives 0 = fun (x : N) (x_1 : G.strategy x) => True

theorem StrategicGame.Survives.prev {N : Type u_1} {U : Type u_2} [DecidableEq N] [Preorder U] {G : StrategicGame N U} {n : ℕ} {i : N} {s : G.strategy i} (h : G.Survives (n + 1) i s) : G.Survives n i s

Survival at round n+1 implies survival at round n.

theorem StrategicGame.Survives.mono {N : Type u_1} {U : Type u_2} [DecidableEq N] [Preorder U] {G : StrategicGame N U} {m n : ℕ} (hmn : m ≤ n) {i : N} {s : G.strategy i} (h : G.Survives n i s) : G.Survives m i s

Survival is monotone: later rounds ⊆ earlier rounds.

def StrategicGame.IsRationalizable {N : Type u_1} {U : Type u_2} [DecidableEq N] [Preorder U] (G : StrategicGame N U) (i : N) (s : G.strategy i) : Prop

A strategy is rationalizable if it survives all rounds.

Equations

• G.IsRationalizable i s = ∀ (n : ℕ), G.Survives n i s

theorem StrategicGame.IsNashEquilibrium.survives {N : Type u_1} {U : Type u_2} [DecidableEq N] [Preorder U] {G : StrategicGame N U} {σ : G.Profile} (hN : IsNashEquilibrium G σ) (n : ℕ) (i : N) : G.Survives n i (σ i)

Nash equilibrium strategies survive all rounds. [MSZ 4.31]

theorem StrategicGame.IsNashEquilibrium.isRationalizable {N : Type u_1} {U : Type u_2} [DecidableEq N] [Preorder U] {G : StrategicGame N U} {σ : G.Profile} (hN : IsNashEquilibrium G σ) (i : N) : G.IsRationalizable i (σ i)

Nash strategies are rationalizable.

def StrategicGame.IsDominanceSolvable {N : Type u_1} {U : Type u_2} [DecidableEq N] [Preorder U] (G : StrategicGame N U) : Prop

A game is dominance-solvable if IESDS yields a unique surviving profile.

Equations

• G.IsDominanceSolvable = ∃! σ : G.Profile, ∀ (i : N) (n : ℕ), G.Survives n i (σ i)