EconCSLib.GameTheory.StrategicGame.ZeroSum.Learning.Robinson

Robinson's admissible-sequence lemma (Robinson 1951; MFoGT Section 2.8, Exercise 12): for every matrix game A, every ε > 0, and every admissible sequence on A, the cumulative duality gap μ(t) is eventually ≤ ε·t.

This module defines the objects used by that argument. The proof targets remain recorded in the knowledge blueprint until formal proofs are added.

Main definitions

• AdmissibleSequence A — a sequence of cumulative counterfactual payoff vectors (α(t), β(t)) on A satisfying the Robinson update rule.
• AdmissibleSequence.mu — the cumulative duality gap max_i β^i - min_j α^j.
• MatrixGame.normMax — ‖A‖ = max_{i,j} |A i j|.

noncomputable def MatrixGame.normMax {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) : ℝ

‖A‖ := max_{i,j} |A_{i,j}|, the entrywise sup norm of the payoff matrix.

Field-generic in the abstract, but the Robinson analysis is stated over ℝ (needed for the asymptotic o(t) formulation).

Equations

• A.normMax = Finset.univ.sup' ⋯ fun (i : I) => Finset.univ.sup' ⋯ fun (j : J) => |A.g i j|

structure MatrixGame.AdmissibleSequence {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] (A : MatrixGame I J ℝ) : Type (max u_1 u_2)

An admissible sequence on a matrix game A (Robinson 1951 setup).

Records cumulative counterfactual payoff vectors α(t) : J → ℝ (payoff to playing column j against the actual row sequence) and β(t) : I → ℝ (payoff to playing row i against the actual column sequence), together with the row/column choice sequences and the admissibility conditions:

• init_bracket — min_j α^j(0) = max_i β^i(0) (the bracket-start condition, MFoGT (i)).
• iSeq_best, jSeq_best — at each step the chosen row is in argmax β(t) and the chosen column is in argmin α(t).
• α_step, β_step — the cumulative-payoff update by the chosen pure actions, MFoGT (ii).

This is the cumulative-payoff encoding of a fictitious-play realisation; see MatrixGame.IsFictitiousPlay for the empirical-frequency formulation, and the blueprint node for the correspondence α(t)/t = x(t) A, β(t)/t = A y(t) (plus the negligible boundary).

• α : ℕ → J → ℝ
• β : ℕ → I → ℝ
• iSeq : ℕ → I
• jSeq : ℕ → J
• init_bracket : Finset.univ.inf' ⋯ (self.α 0) = Finset.univ.sup' ⋯ (self.β 0)
• iSeq_best (t : ℕ) (i' : I) : self.β t i' ≤ self.β t (self.iSeq t)
• jSeq_best (t : ℕ) (j' : J) : self.α t (self.jSeq t) ≤ self.α t j'
• α_step (t : ℕ) (j : J) : self.α (t + 1) j = self.α t j + A.g (self.iSeq t) j
• β_step (t : ℕ) (i : I) : self.β (t + 1) i = self.β t i + A.g i (self.jSeq t)

noncomputable def MatrixGame.AdmissibleSequence.mu {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] {A : MatrixGame I J ℝ} (s : A.AdmissibleSequence) (t : ℕ) : ℝ

Cumulative duality gap μ(t) := max_i β^i(t) - min_j α^j(t).

Equations

• s.mu t = Finset.univ.sup' ⋯ (s.β t) - Finset.univ.inf' ⋯ (s.α t)

def MatrixGame.AdmissibleSequence.IsRowUsefulInWindow {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] {A : MatrixGame I J ℝ} (s : A.AdmissibleSequence) (start length : ℕ) (i : I) : Prop

A pure row i is useful in the window [s, s + t*] if there is a step inside the window at which i is among the row player's argmax choices.

Equations

• s.IsRowUsefulInWindow start length i = ∃ (k : ℕ), start ≤ k ∧ k < start + length ∧ s.iSeq k = i

def MatrixGame.AdmissibleSequence.IsColUsefulInWindow {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [Nonempty I] [Nonempty J] {A : MatrixGame I J ℝ} (s : A.AdmissibleSequence) (start length : ℕ) (j : J) : Prop

A pure column j is useful in the window [s, s + t*] analogously.

Equations

• s.IsColUsefulInWindow start length j = ∃ (k : ℕ), start ≤ k ∧ k < start + length ∧ s.jSeq k = j