zetesis-puremath Blueprint

5.3 Approximate minimax

Theorem 5.8 Approximate minimax via MWU

Lean: ProbabilityTheory.mwu_approx_minimax

Fix \(\varepsilon {\gt} 0\), set \(\eta = \varepsilon /4\) and \(T = \max \{ 1, \lceil 16 \log N / \varepsilon ^2 \rceil \} \) where \(N = |C|\). If the row player can guarantee value \(v\) against every mixed column, then the empirical row mixture produced by \(T\) rounds of MWU achieves

\[ v - \varepsilon \; \le \; \mathrm{boolGamePayoff}\, M\, p\, c \qquad \text{for every pure $c \in C$.} \]

This is the Freund-Schapire constructive minimax [ 10 , Thm 3 ] ; [ 3 , § 3.1 ] unifies this with general online learning.

Theorem 5.9 Covering-based minimax existence

Lean: ProbabilityTheory.covering_minimax

Given the hrow hypothesis, there exists a mixed-row PMF whose payoff against every pure column is at least \(1 / |C|\). Proof by pigeonhole-averaging over per-column pure-row witnesses extracted via ProbabilityTheory.exists_covering_row [ 10 ] .

Theorem 5.10 \(\varepsilon \)-approximate finite minimax

Lean: ProbabilityTheory.finite_approx_minimax

Under a feasibility side-condition \(v - \varepsilon \le 1/|C|\), the covering-based mixed-row strategy from Theorem 5.9 achieves payoff \(\ge v - \varepsilon \) against every pure column. This is the logical dual of the quantitative MWU bound in Theorem 5.8 [ 10 ] , [ 3 , § 3.1 ] .