Read-back: zero_sum_minimax

For every pair of natural numbers $m, n \ge 0$ (so the index sets below have sizes $m+1 \ge 1$ and $n+1 \ge 1$; the degenerate cases are $1\times 1$ matrices, never empty ones) and every real matrix $A$ with rows indexed by $\{0,\dots,m\}$ and columns indexed by $\{0,\dots,n\}$, the theorem asserts the existence of a vector $p \in \Delta_{m+1}$ and a vector $q \in \Delta_{n+1}$, where

$$\Delta_{k} \;=\; \Big\{ x : \{0,\dots,k-1\} \to \mathbb{R} \;\Big|\; x_i \ge 0 \text{ for all } i, \;\sum_{i} x_i = 1 \Big\}$$

is the standard probability simplex (this is the literal content of membership in stdSimplex ℝ (Fin k)), such that the following three statements hold. Throughout, the expression written p ⬝ᵥ A.mulVec q unfolds to the bilinear form

$$p^{\mathsf T} A\, q \;=\; \sum_{i=0}^{m} p_i \left( \sum_{j=0}^{n} A_{ij}\, q_j \right).$$

First conjunct. For every $p' \in \Delta_{m+1}$,

$$\sum_{i,j} p'_i\, A_{ij}\, q_j \;\le\; \sum_{i,j} p_i\, A_{ij}\, q_j,$$

i.e. against this fixed $q$, no distribution over rows achieves a strictly larger value of $x^{\mathsf T} A q$ than $p$ does (a non-strict maximality of $p$).

Second conjunct. For every $q' \in \Delta_{n+1}$,

$$\sum_{i,j} p_i\, A_{ij}\, q_j \;\le\; \sum_{i,j} p_i\, A_{ij}\, q'_j,$$

i.e. against this fixed $p$, no distribution over columns achieves a strictly smaller value of $p^{\mathsf T} A y$ than $q$ does (a non-strict minimality of $q$).

Third conjunct. The pair $(p, q)$, packaged as a strategy profile, satisfies a custom mixed-Nash-equilibrium predicate for a specific two-player game, defined as follows.

The game. The set of players is the two-element type of Booleans, $\{\mathsf{true}, \mathsf{false}\}$. Player $\mathsf{true}$'s pure-strategy set is $\{0,\dots,m\}$ (the row indices of $A$); player $\mathsf{false}$'s pure-strategy set is $\{0,\dots,n\}$ (the column indices). Given a pure profile $s$ assigning row $s_{\mathsf{true}} = i$ and column $s_{\mathsf{false}} = j$, the payoff function (zeroSumPayoff A) gives player $\mathsf{true}$ the payoff $A_{ij}$ and player $\mathsf{false}$ the payoff $-A_{ij}$; so the two payoffs sum to zero at every pure profile, with $A$ read as the payoff matrix of the row player $\mathsf{true}$.

The profile. The profile claimed to be an equilibrium (matrixGameProfile p q) assigns to player $\mathsf{true}$ the weight function $p$ on rows and to player $\mathsf{false}$ the weight function $q$ on columns — exactly the $p, q$ from the existential quantifiers above.

The equilibrium predicate. IsMixedNash for this game demands the conjunction of:

1. Each player's assigned weight function is a lottery: $p_i \ge 0$ for all $i$ with $\sum_i p_i = 1$, and $q_j \ge 0$ for all $j$ with $\sum_j q_j = 1$. (This duplicates the simplex-membership conditions already imposed on $p$ and $q$.)

2. For each player $b \in \{\mathsf{true}, \mathsf{false}\}$ and every lottery $\tau$ over that player's own pure-strategy set (nonnegative weights summing to $1$), the expected payoff to player $b$ under the profile in which $b$'s strategy is replaced by $\tau$ (the other player's strategy left unchanged) is at most the expected payoff to $b$ under the original profile. Here expected payoff to player $b$ under a profile $(\sigma_{\mathsf{true}}, \sigma_{\mathsf{false}})$ means the sum over all pure profiles $(i,j)$, $0 \le i \le m$, $0 \le j \le n$, of the product of the profile's weights times $b$'s payoff:

$$\sum_{i=0}^{m} \sum_{j=0}^{n} \sigma_{\mathsf{true}}(i)\, \sigma_{\mathsf{false}}(j)\, u_b(i,j),$$

where $u_{\mathsf{true}}(i,j) = A_{ij}$ and $u_{\mathsf{false}}(i,j) = -A_{ij}$. Note that this formula is applied as written even when the deviating weight function $\tau$ replaces one factor — the weights need not come from the equilibrium profile.

Concretely, unfolding the expected payoffs, condition 2 says: for every lottery $p'$ on $\{0,\dots,m\}$, $\;p'^{\mathsf T} A\, q \le p^{\mathsf T} A\, q$ (no unilateral deviation improves the row player's expected payoff), and for every lottery $q'$ on $\{0,\dots,n\}$, $\;-\,p^{\mathsf T} A\, q' \le -\,p^{\mathsf T} A\, q$, equivalently $p^{\mathsf T} A\, q \le p^{\mathsf T} A\, q'$ (no unilateral deviation improves the column player's expected payoff, whose payoff is the negation).

All inequalities in the statement are non-strict ($\le$). The theorem claims existence only ($\exists$, not unique existence); nothing is asserted about the value $p^{\mathsf T} A q$ itself (e.g. no minimax/maximin equality is stated explicitly), and nothing constrains $A$ beyond having real entries and the stated dimensions.