A finite minimax lemma #
Let finitely many pure strategies x have payoffs f i x against finitely many
constraints i. If every nonnegative combination of the constraints is met by some
pure strategy, then one mixed strategy meets all the constraints at once. The proof
separates the convex hull of the payoff vectors from the closed lower orthant at c.
theorem
Erdos111.exists_mixed_le
{ι : Type u_1}
{X : Type u_2}
[Fintype ι]
[Fintype X]
(f : ι → X → ℝ)
(c : ι → ℝ)
(h : ∀ (ρ : ι → ℝ), (∀ (i : ι), 0 ≤ ρ i) → ∃ (x : X), ∑ i : ι, ρ i * f i x ≤ ∑ i : ι, ρ i * c i)
:
If every nonnegative combination of the constraints f i ≤ c i is met by a pure
strategy, a single mixed strategy meets every constraint.