Lean declarations

def StrategicGame.Survives EconCSLib @ cef01c7, EconCSLib.GameTheory.StrategicGame.IESDS

def Survives (G : StrategicGame N U) : ℕ → (i : N) → G.strategy i → Prop
  | 0 => fun _ _ => True
  | n + 1 => fun i s =>
      G.Survives n i s ∧
      ¬ ∃ t : G.strategy i, G.Survives n i t ∧
        ∀ σ : G.Profile, (∀ j, G.Survives n j (σ j)) →
          G.payoff (deviate σ i s) i < G.payoff (deviate σ i t) i

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

theorem StrategicGame.Survives.mono EconCSLib @ cef01c7, EconCSLib.GameTheory.StrategicGame.IESDS
Survival is monotone: later rounds ⊆ earlier rounds.
```
theorem Survives.mono {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
```
theorem StrategicGame.Survives.prev EconCSLib @ cef01c7, EconCSLib.GameTheory.StrategicGame.IESDS
Survival at round n+1 implies survival at round n.
```
theorem Survives.prev {G : StrategicGame N U} {n : ℕ} {i : N} {s : G.strategy i}
    (h : G.Survives (n + 1) i s) : G.Survives n i s
```

Modules: EconCSLib.GameTheory.StrategicGame.IESDS

Iterated Elimination Of Strictly Dominated Strategies

Starting from a strategic game, remove all strictly dominated strategies. The remaining strategy sets define a restricted game, in which new strategies may become strictly dominated. Repeating this operation gives an iterated elimination process.

A strategy survives to round $k$ if it has not been eliminated in the first $k$ rounds. The limiting survivor set is the set of strategies that survive all finite rounds.

References

[MFoGT, Section 1.3.3] Laraki, Renault, and Sorin, Mathematical Foundations of Game Theory. Iterated elimination of strictly dominated strategies.

Iterated Elimination Of Strictly Dominated Strategies

References

Also in