MWU approximate minimax: headline theorem #
The full MWU-based approximate minimax theorem: if every column mixture
admits a pure row with expected payoff at least v, then some row mixture
achieves payoff at least v - ε against every pure column.
Chooses η = ε / 4 and T = max 1 ⌈16 log N / ε²⌉ so that the potential
bound, the hit-rate-from-potential lemma, and the feasibility conditions
combine into the per-column guarantee.
theorem
ProbabilityTheory.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 : FintypePMF C), ∃ (r : R), v ≤ ∑ c : C, q.prob c * if M r c = true then 1 else 0)
:
∃ (p : FintypePMF R), ∀ (c : C), v - ε ≤ boolGamePayoff M p c
MWU approximate minimax. If every column mixture admits a pure row with expected
payoff at least v, then some row mixture achieves payoff at least v - ε against every
pure column.