Approximate Minimax for Finite Boolean Games

Infrastructure for the minimax theorem in finite Boolean games: PMF construction utilities, payoff analysis, covering arguments, and MWU potential bounds.

Main definitions

• normalizeToPMF : normalize a positive weight vector to FinitePMF
• pointMassPMF : point mass distribution on a single element
• uniformPMF : uniform distribution over a Fintype
• empiricalPMF : empirical distribution of a finite sequence
• boolGamePayoff : expected payoff of a distribution in a Boolean game
• MWUConfig : multiplicative weights update state

Main results

• exists_covering_row : if minimax value > 0, every column has a covering row
• covering_minimax : ∃ p, ∀ c, 1/|C| ≤ boolGamePayoff(p, c)
• finite_approx_minimax : approximate minimax for finite Boolean games
• mwu_potential_T_bound : after T MWU rounds, Φ_T ≤ |C| · (1 - ηv)^T

References

• Arora, Hazan, Kale, "The Multiplicative Weights Update Method", ToC 8(1), 2012

PMF Construction Utilities

noncomputable def normalizeToPMF {C : Type u_1} [Fintype C] [Nonempty C] (w : C → ℝ) (hw : ∀ (c : C), 0 < w c) : FinitePMF C

Normalize a strictly positive weight vector to a FinitePMF.

Equations

• normalizeToPMF w hw = { prob := fun (c : C) => w c / ∑ c' : C, w c', prob_nonneg := ⋯, prob_sum_one := ⋯ }

theorem normalizeToPMF_prob {C : Type u_1} [Fintype C] [Nonempty C] (w : C → ℝ) (hw : ∀ (c : C), 0 < w c) (c : C) : (normalizeToPMF w hw).prob c = w c / ∑ c' : C, w c'

def pointMassPMF {C : Type u_1} [Fintype C] [DecidableEq C] (c₀ : C) : FinitePMF C

Point mass PMF at a single element.

Equations

• pointMassPMF c₀ = { prob := fun (c : C) => if c = c₀ then 1 else 0, prob_nonneg := ⋯, prob_sum_one := ⋯ }

noncomputable def uniformPMF (C : Type u_1) [Fintype C] [Nonempty C] : FinitePMF C

Uniform PMF over a nonempty Fintype.

Equations

• uniformPMF C = normalizeToPMF (fun (x : C) => 1) ⋯

noncomputable def empiricalPMF {α : Type u_1} [Fintype α] [DecidableEq α] {T : ℕ} (hT : 0 < T) (rs : Fin T → α) : FinitePMF α

Build FinitePMF from empirical frequencies of a finite sequence.

Equations

• empiricalPMF hT rs = { prob := fun (a : α) => ↑{t : Fin T | rs t = a}.card / ↑T, prob_nonneg := ⋯, prob_sum_one := ⋯ }

Boolean Game Payoff

def boolGamePayoff {R : Type u_1} {C : Type u_2} [Fintype R] (M : R → C → Bool) (p : FinitePMF R) (c : C) : ℝ

Expected payoff of distribution p against column c in a Boolean game.

Equations

• boolGamePayoff M p c = ∑ r : R, p.prob r * if M r c = true then 1 else 0

theorem boolGamePayoff_nonneg {R : Type u_1} {C : Type u_2} [Fintype R] (M : R → C → Bool) (p : FinitePMF R) (c : C) : 0 ≤ boolGamePayoff M p c

theorem boolGamePayoff_le_one {R : Type u_1} {C : Type u_2} [Fintype R] (M : R → C → Bool) (p : FinitePMF R) (c : C) : boolGamePayoff M p c ≤ 1

theorem boolGamePayoff_pointMass {R : Type u_1} {C : Type u_2} [Fintype R] [DecidableEq R] (M : R → C → Bool) (r₀ : R) (c : C) : boolGamePayoff M (pointMassPMF r₀) c = if M r₀ c = true then 1 else 0

Point mass payoff equals the game value at that row-column pair.

theorem minimax_value_le_one {R : Type u_1} {C : Type u_2} [Fintype R] [Fintype C] [Nonempty C] (M : R → C → Bool) (v : ℝ) (hrow : ∀ (q : FinitePMF C), ∃ (r : R), v ≤ ∑ c : C, q.prob c * if M r c = true then 1 else 0) : v ≤ 1

The minimax value of a Boolean game is at most 1.

Covering Row Lemma

theorem exists_covering_row {R : Type u_1} {C : Type u_2} [Fintype R] [Fintype C] [DecidableEq C] [Nonempty C] (M : R → C → Bool) (v : ℝ) (hv : 0 < v) (hrow : ∀ (q : FinitePMF C), ∃ (r : R), v ≤ ∑ c : C, q.prob c * if M r c = true then 1 else 0) (c₀ : C) : ∃ (r : R), M r c₀ = true

If minimax value > 0, every column has a row with M(r,c) = true.

Covering Minimax Theorem

theorem covering_minimax {R : Type u_1} {C : Type u_2} [Fintype R] [Fintype C] [Nonempty C] [DecidableEq R] [DecidableEq C] (M : R → C → Bool) (v : ℝ) (hv : 0 < v) (hrow : ∀ (q : FinitePMF C), ∃ (r : R), v ≤ ∑ c : C, q.prob c * if M r c = true then 1 else 0) : ∃ (p : FinitePMF R), ∀ (c : C), 1 / ↑(Fintype.card C) ≤ boolGamePayoff M p c

Covering-based minimax: if the minimax value > 0, there exists a row distribution with payoff ≥ 1/|C| against every column.

Proof: for each column c, pick a row r_c with M(r_c, c) = true (guaranteed by exists_covering_row). The empirical distribution of these rows gives payoff ≥ 1/|C| against every column, since each column c₀ is covered by at least one row (namely r_c₀).

Approximate Minimax Theorem

theorem finite_approx_minimax {R : Type u_1} {C : Type u_2} [Fintype R] [Fintype C] [Nonempty C] [Nonempty R] [DecidableEq R] [DecidableEq C] (M : R → C → Bool) (v ε : ℝ) (hε : 0 < ε) (hrow : ∀ (q : FinitePMF C), ∃ (r : R), v ≤ ∑ c : C, q.prob c * if M r c = true then 1 else 0) (hε_feasible : v - ε ≤ 1 / ↑(Fintype.card C)) : ∃ (p : FinitePMF R), ∀ (c : C), v - ε ≤ boolGamePayoff M p c

Approximate minimax for finite Boolean games.

If for every column mixture q, the row player has a pure best response with expected payoff ≥ v, then there exists a row mixture p such that every pure column gets payoff ≥ v - ε.

This version uses the covering argument (payoff ≥ 1/|C| for all columns) combined with the feasibility condition v - ε ≤ 1/|C|.

MWU Infrastructure

Multiplicative Weights Update state and potential analysis. The potential bound is the core analytic result: after T rounds, Φ_T ≤ |C| · (1 - ηv)^T.

structure MWUConfig (C : Type u_1) [Fintype C] : Type u_1

MWU config: weight vector with positivity proof.

• weights : C → ℝ
• weights_pos (c : C) : 0 < self.weights c

def MWUConfig.potential {C : Type u_1} [Fintype C] (cfg : MWUConfig C) : ℝ

Potential = sum of weights.

Equations

• cfg.potential = ∑ c : C, cfg.weights c

theorem MWUConfig.potential_pos {C : Type u_1} [Fintype C] [Nonempty C] (cfg : MWUConfig C) : 0 < cfg.potential

def mwuInit (C : Type u_1) [Fintype C] : MWUConfig C

Initial config: all weights = 1.

Equations

• mwuInit C = { weights := fun (x : C) => 1, weights_pos := ⋯ }

theorem mwuInit_potential (C : Type u_1) [Fintype C] : (mwuInit C).potential = ↑(Fintype.card C)

noncomputable def MWUConfig.toPMF {C : Type u_1} [Fintype C] [Nonempty C] (cfg : MWUConfig C) : FinitePMF C

Normalize config to PMF.

Equations

• cfg.toPMF = normalizeToPMF cfg.weights ⋯

def mwuUpdateWeights {C : Type u_1} [Fintype C] {R : Type u_2} (M : R → C → Bool) (η : ℝ) (hη1 : η < 1) (cfg : MWUConfig C) (r : R) : MWUConfig C

One MWU update step on weights.

Equations

• mwuUpdateWeights M η hη1 cfg r = { weights := fun (c : C) => cfg.weights c * if M r c = true then 1 - η else 1, weights_pos := ⋯ }

theorem best_response_payoff_weights {R : Type u_1} {C : Type u_2} [Fintype R] [Fintype C] [Nonempty C] (M : R → C → Bool) (v : ℝ) (hrow : ∀ (q : FinitePMF C), ∃ (r : R), v ≤ ∑ c : C, q.prob c * if M r c = true then 1 else 0) (cfg : MWUConfig C) : v * cfg.potential ≤ ∑ c : C, cfg.weights c * if M ⋯.choose c = true then 1 else 0

Best response payoff ≥ v · Φ in terms of weights.

theorem potential_one_step_bound {R : Type u_1} {C : Type u_2} [Fintype R] [Fintype C] [Nonempty C] (M : R → C → Bool) (η : ℝ) (hη : 0 ≤ η) (hη1 : η < 1) (v : ℝ) (hrow : ∀ (q : FinitePMF C), ∃ (r : R), v ≤ ∑ c : C, q.prob c * if M r c = true then 1 else 0) (cfg : MWUConfig C) : (mwuUpdateWeights M η hη1 cfg ⋯.choose).potential ≤ cfg.potential * (1 - η * v)

Potential bound after one step: Φ' ≤ Φ · (1 - η·v).

def mwuRun {R : Type u_1} {C : Type u_2} [Fintype R] [Fintype C] [Nonempty C] (M : R → C → Bool) (η : ℝ) (hη1 : η < 1) (v : ℝ) (hrow : ∀ (q : FinitePMF C), ∃ (r : R), v ≤ ∑ c : C, q.prob c * if M r c = true then 1 else 0) (T : ℕ) : MWUConfig C × (Fin T → R)

MWU run: iterate T steps, returning final config and row sequence.

Equations

• mwuRun M η hη1 v hrow 0 = (mwuInit C, Fin.elim0)
• mwuRun M η hη1 v hrow T.succ = match mwuRun M η hη1 v hrow T with | (cfg, rows) => have r := ⋯.choose; (mwuUpdateWeights M η hη1 cfg r, Fin.snoc rows r)

@[reducible, inline]

noncomputable abbrev mwuConfig {R : Type u_1} {C : Type u_2} [Fintype R] [Fintype C] [Nonempty C] (M : R → C → Bool) (η : ℝ) (hη1 : η < 1) (v : ℝ) (hrow : ∀ (q : FinitePMF C), ∃ (r : R), v ≤ ∑ c : C, q.prob c * if M r c = true then 1 else 0) (T : ℕ) : MWUConfig C

The MWU config after T steps.

Equations

• mwuConfig M η hη1 v hrow T = (mwuRun M η hη1 v hrow T).1

@[reducible, inline]

noncomputable abbrev mwuRows {R : Type u_1} {C : Type u_2} [Fintype R] [Fintype C] [Nonempty C] (M : R → C → Bool) (η : ℝ) (hη1 : η < 1) (v : ℝ) (hrow : ∀ (q : FinitePMF C), ∃ (r : R), v ≤ ∑ c : C, q.prob c * if M r c = true then 1 else 0) (T : ℕ) : Fin T → R

The MWU row sequence after T steps.

Equations

• mwuRows M η hη1 v hrow T = (mwuRun M η hη1 v hrow T).2

theorem mwu_potential_T_bound {R : Type u_1} {C : Type u_2} [Fintype R] [Fintype C] [Nonempty C] (M : R → C → Bool) (η : ℝ) (hη : 0 ≤ η) (hη1 : η < 1) (v : ℝ) (hrow : ∀ (q : FinitePMF C), ∃ (r : R), v ≤ ∑ c : C, q.prob c * if M r c = true then 1 else 0) (T : ℕ) : (mwuConfig M η hη1 v hrow T).potential ≤ ↑(Fintype.card C) * (1 - η * v) ^ T

Potential bound after T steps: Φ_T ≤ |C| · (1 - ηv)^T.

This is the core MWU guarantee. Combined with individual weight lower bounds (w_T(c) = (1-η)^{losses(c)}), it yields the regret bound.

MWU Individual Weight Tracking + Regret Extraction

theorem mwu_approx_minimax {R : Type u_1} {C : Type u_2} [Fintype R] [Fintype C] [Nonempty R] [Nonempty C] [DecidableEq R] [DecidableEq C] (M : R → C → Bool) (v ε : ℝ) (hε : 0 < ε) (hrow : ∀ (q : FinitePMF C), ∃ (r : R), v ≤ ∑ c : C, q.prob c * if M r c = true then 1 else 0) : ∃ (p : FinitePMF R), ∀ (c : C), v - ε ≤ boolGamePayoff M p c

Genuine approximate minimax via MWU regret extraction. If every column mixture admits a pure row with expected payoff ≥ v, then there is a row mixture with payoff ≥ v - ε against every column.