EconCSLib.GameTheory.StrategicGame.ZeroSum.Learning.FictitiousPlay

Fictitious play for a finite zero-sum matrix game over ℝ. This module introduces the basic vocabulary used throughout the Robinson 1951 convergence analysis:

• empiricalFrequency — the empirical distribution of the first n pure actions of an infinite sequence.
• IsFictitiousPlay — predicate on pairs (iSeq, jSeq) : (ℕ → I) × (ℕ → J) asserting that at every step both players best-respond to the opponent's empirical frequency so far.

The Robinson induction-on-matrix-size proof itself lives in StrategicGame/FictitiousPlay/Robinson.lean; the Cesàro payoff convergence in StrategicGame/FictitiousPlay/Cesaro.lean; the main convergence theorem in StrategicGame/FictitiousPlay/Convergence.lean; the continuous-time variant in StrategicGame/FictitiousPlay/Continuous.lean.

References

• [MFoGT] Laraki, Renault, Sorin, Mathematical Foundations of Game Theory, Definition 2.7.1 and Theorem 2.7.2.
• [Robinson 1951] J. Robinson, "An iterative method of solving a game", Annals of Mathematics 54 (1951), 296–301.

Blueprint

• docs/knowledge/staged/zero_sum/empirical_frequency.md
• docs/knowledge/staged/zero_sum/fictitious_play.md

noncomputable def MatrixGame.empiricalFrequency {I : Type u_1} [Fintype I] [Nonempty I] [DecidableEq I] (a : ℕ → I) (n : ℕ) : ↑(stdSimplex ℝ I)

Empirical frequency of the first n pure actions of a sequence a : ℕ → I. For n = 0 we fall back to the uniform distribution so the function is total; the FP statements always require 0 < n.

Equations

• MatrixGame.empiricalFrequency a n = if hn : 0 < n then ⟨fun (i : I) => ↑{s ∈ Finset.range n | a s = i}.card / ↑n, ⋯⟩ else ⟨fun (x : I) => (↑(Fintype.card I))⁻¹, ⋯⟩

def MatrixGame.IsFictitiousPlay {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] [DecidableEq I] [DecidableEq J] (A : MatrixGame I J ℝ) (iSeq : ℕ → I) (jSeq : ℕ → J) : Prop

Fictitious play realisation on a matrix game A. At every step n + 1, the row player picks a pure row best-responding to the column player's empirical frequency y_n, and dually for the column player. The n = 0 "warm-up" step is unconstrained (the empirical frequency is undefined before any play has occurred).

Equations

• One or more equations did not get rendered due to their size.