Expected payoff of a FintypePMF in a Bool-valued game

Infrastructure for minimax analysis over finite Boolean games: boolGamePayoff is the inner-product pairing between a row distribution and an indicator column. Supporting lemmas prove it is [0, 1]-bounded, evaluates correctly on point masses, and implies the minimax value is at most 1.

def ProbabilityTheory.boolGamePayoff {R : Type u_1} {C : Type u_2} [Fintype R] (M : R → C → Bool) (p : FintypePMF R) (c : C) : ℝ

Expected payoff of distribution p against column c in a Bool-valued game defined by M : R → C → Bool.

Equations

• ProbabilityTheory.boolGamePayoff M p c = ∑ r : R, p.prob r * if M r c = true then 1 else 0

theorem ProbabilityTheory.boolGamePayoff_nonneg {R : Type u_1} {C : Type u_2} [Fintype R] (M : R → C → Bool) (p : FintypePMF R) (c : C) : 0 ≤ boolGamePayoff M p c

theorem ProbabilityTheory.boolGamePayoff_le_one {R : Type u_1} {C : Type u_2} [Fintype R] (M : R → C → Bool) (p : FintypePMF R) (c : C) : boolGamePayoff M p c ≤ 1

theorem ProbabilityTheory.boolGamePayoff_pointMass {R : Type u_1} {C : Type u_2} [Fintype R] [DecidableEq R] (M : R → C → Bool) (r₀ : R) (c : C) : boolGamePayoff M (FintypePMF.pointMass r₀) c = if M r₀ c = true then 1 else 0

Payoff on a point mass is the pointwise game value.

theorem ProbabilityTheory.minimax_value_le_one {R : Type u_1} {C : Type u_2} [Fintype R] [Fintype C] [Nonempty C] (M : R → C → Bool) (v : ℝ) (hrow : ∀ (q : FintypePMF C), ∃ (r : R), v ≤ ∑ c : C, q.prob c * if M r c = true then 1 else 0) : v ≤ 1

If a row player can achieve expected payoff at least v against every column mixture, then v ≤ 1.