EconCSLib.GameTheory.StrategicGame.ESS

Evolutionarily stable strategies (ESS) for symmetric two-player games.

Main definitions

• IsESS — evolutionarily stable strategy [Maynard Smith-Price 1973]
• IsNSS — neutrally stable strategy

Main results

• ess_implies_nss
• strict_nash_implies_ess
• ess_is_symmetric_nash — ESS implies symmetric Nash [MSZ 5.51]
• ess_isolation — distinct ESS are strictly separated

References

• [MSZ] Section 5.6
• Maynard Smith, J. and Price, G.R. (1973). "The Logic of Animal Conflict".

Definitions

def IsESS {S : Type u_1} (u : S → S → ℝ) (s : S) : Prop

A strategy s is an evolutionarily stable strategy (ESS) if:

1. u(s,s) ≥ u(t,s) for all t (Nash condition)
2. If u(s,s) = u(t,s) then u(s,t) > u(t,t) (invasion barrier) [MSZ 5.50]

Equations

• IsESS u s = ((∀ (t : S), u s s ≥ u t s) ∧ ∀ (t : S), u s s = u t s → s ≠ t → u s t > u t t)

def IsNSS {S : Type u_1} (u : S → S → ℝ) (s : S) : Prop

A strategy s is neutrally stable (NSS) if:

1. u(s,s) ≥ u(t,s) for all t
2. If u(s,s) = u(t,s) then u(s,t) ≥ u(t,t)

Equations

• IsNSS u s = ((∀ (t : S), u s s ≥ u t s) ∧ ∀ (t : S), u s s = u t s → u s t ≥ u t t)

Theorems

theorem IsESS.isNSS {S : Type u_1} {u : S → S → ℝ} {s : S} (h : IsESS u s) : IsNSS u s

Every ESS is neutrally stable.

theorem strict_nash_implies_ess {S : Type u_1} {u : S → S → ℝ} {s : S} (hstrict : ∀ (t : S), t ≠ s → u s s > u t s) : IsESS u s

A strict symmetric Nash equilibrium is automatically ESS.

theorem IsESS.nash_condition {S : Type u_1} {u : S → S → ℝ} {s : S} (h : IsESS u s) (t : S) : u s s ≥ u t s

An ESS satisfies the symmetric Nash condition. [MSZ 5.51]

theorem IsESS.strict_against_other {S : Type u_1} {u : S → S → ℝ} {s t : S} (hs : IsESS u s) (ht : IsESS u t) (hne : s ≠ t) : u s s > u t s

Distinct ESS are strictly separated: if s ≠ t are both ESS, then u(s,s) > u(t,s).