EconCSLib.GameTheory.StrategicGame.CorrelatedEq #

Correlated equilibrium: a distribution over strategy profiles where no player benefits from deviating from the recommendation.

Main definitions #

IsDegenerateCorrelatedEq — a degenerate correlated equilibrium supported on one profile

Main results #

nash_iff_degenerate_ce — a point-mass correlated equilibrium is exactly a Nash equilibrium

References #

[MSZ] Chapter 8

source

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

Prop

A degenerate correlated equilibrium supported on a single profile.

This is the only honest correlated-equilibrium notion currently formalized in this file: the mediator recommends one fixed profile with probability 1. In that case, obedience is exactly the Nash condition.

Equations

G.IsDegenerateCorrelatedEq σ = IsNashEquilibrium G σ

Instances For

source

theorem StrategicGame.nash_iff_degenerate_ce {N : Type u_1} {U : Type u_2} [DecidableEq N] [Preorder U] (G : StrategicGame N U) (σ : G.Profile) :

IsNashEquilibrium G σ ↔ G.IsDegenerateCorrelatedEq σ

A profile is a "degenerate" correlated equilibrium (point mass on one profile) if and only if it is a Nash equilibrium.