Bridge between game payoff and test expectation

boolGamePayoff M p c (a row-distribution payoff against a fixed column) is the same quantity as boolTestExpectation p (fun r => M r c). The identification lets MWU regret bounds and TV-based transfer results live in a single distributional framework.

theorem ProbabilityTheory.boolGamePayoff_eq_boolTestExpectation {R : Type u_1} [Fintype R] [DecidableEq R] {C : Type u_2} (M : R → C → Bool) (p : FintypePMF R) (c : C) : boolGamePayoff M p c = p.boolTestExpectation fun (r : R) => M r c

Game payoff of a row distribution equals the row-test expectation of the column indicator fun r => M r c.