Approximate minimax via the covering argument

A feasibility-style approximate minimax statement: combining covering_minimax with the hypothesis v - ε ≤ 1 / |C| yields a row mixture with payoff at least v - ε against every pure column. Complementary to the MWU-based quantitative bound.

theorem ProbabilityTheory.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 : FintypePMF 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 : FintypePMF R), ∀ (c : C), v - ε ≤ boolGamePayoff M p c

Approximate minimax (covering route). If the minimax value is v, the slack ε is positive, and v - ε ≤ 1 / |C|, then a row mixture exists whose payoff is at least v - ε against every pure column.