Definition Weakly Dominant Strategy

definition admitted

#

Lean declarations

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

Strategy `s` is weakly dominant for player `i`.

def IsWeaklyDominant (G : StrategicGame N U) (i : N) (s : G.strategy i) : Prop :=
  ∀ s' : G.strategy i, WeaklyDominates G i s s'

theorem IsWeaklyDominant.isBestResponse EconCSLib @ cef01c7, EconCSLib.GameTheory.StrategicGame.Dominance
T2: A weakly dominant strategy is a best response to any profile where player `i` plays it.
```
theorem IsWeaklyDominant.isBestResponse {G : StrategicGame N U} {i : N} {s : G.strategy i}
    (hdom : IsWeaklyDominant G i s) (σ : G.Profile) (hσ : σ i = s) :
    IsBestResponse G σ i
```

Modules: EconCSLib.GameTheory.StrategicGame.Dominance

Weakly Dominant Strategy

A strategy $s_i$ is weakly dominant for player $i$ if it weakly dominates every other strategy available to $i$:

$$\forall s'_i \in S_i, \quad s_i \text{ weakly dominates } s'_i.$$

References

[MSZ, Chapter 2, Section 2.3] Maschler, Solan, and Zamir, Game Theory. Definition of weakly dominant strategy.

Used by

Also in