EconCSLib.GameTheory.StrategicGame.PotentialGame

Potential games: games admitting a potential function that captures all unilateral incentives.

Main definitions

• IsExactPotential — exact potential function
• IsOrdinalPotential — ordinal potential function

Main results

• IsExactPotential.maximizer_is_nash — maximizer of an exact potential is Nash
• IsOrdinalPotential.isNash_iff_localMax — Nash ↔ local max of ordinal potential

References

• [AGT] Chapter 18
• Monderer, D. and Shapley, L.S. (1996). "Potential Games".

def StrategicGame.IsExactPotential {N : Type u_1} {U : Type u_2} [DecidableEq N] [Sub U] (G : StrategicGame N U) (Φ : G.Profile → U) : Prop

An exact potential function: the change in Φ equals the change in the deviating player's payoff.

Equations

• G.IsExactPotential Φ = ∀ (i : N) (σ : G.Profile) (s' : G.strategy i), G.payoff (StrategicGame.deviate σ i s') i - G.payoff σ i = Φ (StrategicGame.deviate σ i s') - Φ σ

def StrategicGame.IsOrdinalPotential {N : Type u_1} {U : Type u_2} [DecidableEq N] [Preorder U] (G : StrategicGame N U) (Φ : G.Profile → U) : Prop

An ordinal potential function: a unilateral deviation improves payoff iff it increases Φ.

Equations

• G.IsOrdinalPotential Φ = ∀ (i : N) (σ : G.Profile) (s' : G.strategy i), G.payoff (StrategicGame.deviate σ i s') i > G.payoff σ i ↔ Φ (StrategicGame.deviate σ i s') > Φ σ

theorem StrategicGame.IsExactPotential.maximizer_is_nash {N : Type u_1} {U : Type u_2} [DecidableEq N] [Field U] [LinearOrder U] [IsStrictOrderedRing U] {G : StrategicGame N U} {Φ : G.Profile → U} (hΦ : G.IsExactPotential Φ) {σ : G.Profile} (hmax : ∀ (τ : G.Profile), Φ σ ≥ Φ τ) : IsNashEquilibrium G σ

A profile maximizing an exact potential is a Nash equilibrium.

theorem StrategicGame.IsOrdinalPotential.isNash_iff_localMax {N : Type u_1} {U : Type u_2} [DecidableEq N] [Field U] [LinearOrder U] [IsStrictOrderedRing U] {G : StrategicGame N U} {Φ : G.Profile → U} (hΦ : G.IsOrdinalPotential Φ) {σ : G.Profile} : IsNashEquilibrium G σ ↔ ∀ (i : N) (s' : G.strategy i), Φ σ ≥ Φ (deviate σ i s')

Nash ↔ local maximizer of ordinal potential.