Covering-based minimax

From the covering-row lemma, construct a row distribution whose payoff is at least 1 / |C| against every column.

theorem ProbabilityTheory.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 : FintypePMF C), ∃ (r : R), v ≤ ∑ c : C, q.prob c * if M r c = true then 1 else 0) : ∃ (p : FintypePMF R), ∀ (c : C), 1 / ↑(Fintype.card C) ≤ boolGamePayoff M p c

Covering-based minimax: if the minimax value is strictly positive, there is a row distribution whose payoff against every column is at least 1 / |C|.