Lean declarations

def StrictlyDominates EconCSLib @ cef01c7, EconCSLib.GameTheory.StrategicGame.Dominance

Strategy `s` strictly dominates strategy `s'` for player `i`.

def StrictlyDominates (G : StrategicGame N U) (i : N) (s s' : G.strategy i) : Prop :=
  ∀ σ : G.Profile, G.payoff (deviate σ i s') i < G.payoff (deviate σ i s) i

theorem StrictlyDominates.weakly EconCSLib @ cef01c7, EconCSLib.GameTheory.StrategicGame.Dominance

Strict dominance implies weak dominance.

theorem StrictlyDominates.weakly {G : StrategicGame N U} {i : N} {s s' : G.strategy i}
    (h : StrictlyDominates G i s s') : WeaklyDominates G i s s'

theorem IsStrictlyDominant.isWeaklyDominant EconCSLib @ cef01c7, EconCSLib.GameTheory.StrategicGame.Dominance

A strictly dominant strategy is weakly dominant.

theorem IsStrictlyDominant.isWeaklyDominant {G : StrategicGame N U} {i : N} {s : G.strategy i}
    [DecidableEq (G.strategy i)]
    (h : IsStrictlyDominant G i s) : IsWeaklyDominant G i s

Modules: EconCSLib.GameTheory.StrategicGame.Dominance

Strict Dominance

A strategy $s_i$ strictly dominates another strategy $s'_i$ for player $i$ if, for every profile $\sigma$ of the other players, playing $s_i$ yields strictly higher payoff:

$$\forall \sigma, \quad u_i(\sigma[i \mapsto s'_i]) < u_i(\sigma[i \mapsto s_i]).$$

References

[MSZ, Chapter 2, Section 2.3] Maschler, Solan, and Zamir, Game Theory. Definition of strict dominance.

Used by

Strictly Dominant Strategy

Strict Dominance

References

Used by

Also in