EconCSLib.GameTheory.StrategicGame.Dominance

Dominance relations between strategies.

Main definitions

• WeaklyDominates — s yields at least as high payoff as s' against all opponents
• StrictlyDominates — s yields strictly higher payoff than s' against all opponents
• IsWeaklyDominant / IsStrictlyDominant — dominates every alternative

Main results

• T2: IsWeaklyDominant.isBestResponse — a weakly dominant strategy is always a best response

def WeaklyDominates {N : Type u_1} {U : Type u_2} [DecidableEq N] [Preorder U] (G : StrategicGame N U) (i : N) (s s' : G.strategy i) : Prop

Strategy s weakly dominates strategy s' for player i.

Equations

• WeaklyDominates G i s s' = ∀ (σ : G.Profile), G.payoff (StrategicGame.deviate σ i s') i ≤ G.payoff (StrategicGame.deviate σ i s) i

def StrictlyDominates {N : Type u_1} {U : Type u_2} [DecidableEq N] [Preorder U] (G : StrategicGame N U) (i : N) (s s' : G.strategy i) : Prop

Strategy s strictly dominates strategy s' for player i.

Equations

• StrictlyDominates G i s s' = ∀ (σ : G.Profile), G.payoff (StrategicGame.deviate σ i s') i < G.payoff (StrategicGame.deviate σ i s) i

def IsWeaklyDominant {N : Type u_1} {U : Type u_2} [DecidableEq N] [Preorder U] (G : StrategicGame N U) (i : N) (s : G.strategy i) : Prop

Strategy s is weakly dominant for player i.

Equations

• IsWeaklyDominant G i s = ∀ (s' : G.strategy i), WeaklyDominates G i s s'

def IsStrictlyDominant {N : Type u_1} {U : Type u_2} [DecidableEq N] [Preorder U] (G : StrategicGame N U) (i : N) (s : G.strategy i) : Prop

Strategy s is strictly dominant for player i.

Equations

• IsStrictlyDominant G i s = ∀ (s' : G.strategy i), s ≠ s' → StrictlyDominates G i s s'

theorem StrictlyDominates.weakly {N : Type u_1} {U : Type u_2} [DecidableEq N] [Preorder U] {G : StrategicGame N U} {i : N} {s s' : G.strategy i} (h : StrictlyDominates G i s s') : WeaklyDominates G i s s'

Strict dominance implies weak dominance.

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

A strictly dominant strategy is weakly dominant.

theorem IsWeaklyDominant.isBestResponse {N : Type u_1} {U : Type u_2} [DecidableEq N] [Preorder U] {G : StrategicGame N U} {i : N} {s : G.strategy i} (hdom : IsWeaklyDominant G i s) (σ : G.Profile) (hσ : σ i = s) : IsBestResponse G σ i

T2: A weakly dominant strategy is a best response to any profile where player i plays it.