EconCSLib.GameTheory.StrategicGame.BestResponse

Defines IsBestResponse: player i is playing a best response to profile σ if no unilateral deviation improves their payoff.

Key lemma:

• T1 (IsBestResponse.congr_payoff): best response depends only on player i's payoff column.

def IsBestResponse {N : Type u_1} {U : Type u_2} [DecidableEq N] [Preorder U] (G : StrategicGame N U) (σ : G.Profile) (i : N) : Prop

Player i is playing a best response to profile σ in game G if no unilateral deviation to any strategy s' yields a higher payoff.

Equations

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

theorem IsBestResponse.congr_payoff {N : Type u_1} {U : Type u_2} [DecidableEq N] [Preorder U] (G : StrategicGame N U) (σ : G.Profile) (i : N) {payoff' : G.Profile → N → U} (h : ∀ (τ : G.Profile), payoff' τ i = G.payoff τ i) : IsBestResponse G σ i ↔ IsBestResponse { strategy := G.strategy, payoff := payoff' } σ i

T1: Best response depends only on player i's payoff column.