Empirical payoff of the MWU row sequence

Bridges the empirical FintypePMF of the MWU row sequence to the column-level hit counter: the payoff boolGamePayoff M (empirical hT rows) c equals hitCount T c / T. Used to convert the analytic T-step potential bound into a per-column payoff statement for the final approximate-minimax theorem.

theorem ProbabilityTheory.boolGamePayoff_empirical_eq_avg {R : Type u_1} {C : Type u_2} [Fintype R] [DecidableEq R] {T : ℕ} (hT : 0 < T) (rs : Fin T → R) (M : R → C → Bool) (c : C) : boolGamePayoff M (FintypePMF.empirical hT rs) c = (∑ t : Fin T, if M (rs t) c = true then 1 else 0) / ↑T

The empirical FintypePMF payoff equals the average indicator along the sequence.

theorem ProbabilityTheory.boolGamePayoff_empirical_eq_hitCount {R : Type u_1} {C : Type u_2} [Fintype R] [Fintype C] [Nonempty C] [DecidableEq R] (M : R → C → Bool) (η : ℝ) (hη1 : η < 1) (v : ℝ) (hrow : ∀ (q : FintypePMF C), ∃ (r : R), v ≤ ∑ c : C, q.prob c * if M r c = true then 1 else 0) {T : ℕ} (hT : 0 < T) (c : C) : boolGamePayoff M (FintypePMF.empirical hT (mwuRows M η hη1 v hrow T)) c = ↑(mwuHitCount M η hη1 v hrow T c) / ↑T

Empirical payoff of the MWU row sequence equals the normalized hit count.