Lean declarations

def StrategicGame.IsRationalizable EconCSLib @ cef01c7, EconCSLib.GameTheory.StrategicGame.IESDS
A strategy is rationalizable if it survives all rounds.
```
def IsRationalizable (G : StrategicGame N U) (i : N) (s : G.strategy i) : Prop :=
  ∀ n, G.Survives n i s
```

Modules: EconCSLib.GameTheory.StrategicGame.IESDS

Rationalizable Strategy

In a compact continuous game, define $$ S_i(1)=BR_i(S_{-i}) $$ and inductively $$ S_i(k+1)=BR_i(S_{-i}(k)). $$ The rationalizable strategy set of player $i$ is $$ S_i^\infty=\bigcap_{k\ge 1}S_i(k). $$ A profile $s$ is rationalizable if $s_i\in S_i^\infty$ for every player $i$.

Lean scope

Lean's IsRationalizable is defined as surviving iterated elimination of strictly dominated strategies (IESDS — see Iterated Elimination Of Strictly Dominated Strategies), whereas the best-response definition above (iterated elimination of strategies that are never a best response) is the MFoGT formulation. The two coincide for finite two-player games (Pearce's lemma) but differ in general. The Lean port currently formalizes the IESDS version only, so this best-response node stays pending until the best-response characterization is linked or proved.

References

[MFoGT, Section 4.4] Laraki, Renault, and Sorin, Mathematical Foundations of Game Theory. Rationalizability as iterated elimination of strategies that are not best responses.

Rationalizable Strategy

Lean scope

References

Used by

Also in