5.1 Boolean-matrix zero-sum games
Definition
5.1
Boolean-matrix payoff
Lean: ProbabilityTheory.boolGamePayoff
For a Boolean matrix \(M : R \to C \to \mathrm{Bool}\), a row distribution \(p : \mathrm{FintypePMF}\, R\), and a pure column \(c : C\),
\[ \mathrm{boolGamePayoff}\, M\, p\, c \; :=\; \sum _{r : R} p(r) \cdot [M\, r\, c]. \]
This is the expected \(\{ 0, 1\} \)-gain of the row player, against a pure column play, in the matrix game \(M\) [ 10 ] .
Theorem
5.2
One-sided minimax sanity
Lean: ProbabilityTheory.minimax_value_le_one
If the row player can guarantee value \(v\) against every mixed column (the hrow hypothesis), then \(v \le 1\) [ 10 ] .