139 Learning Theory — Minimax

139.1 Overview

This module is the public entry point for the convex-compact minimax theorem: it gathers the finite minimax, coarse correlated equilibrium, core, separation, and no-regret components and exposes a single top-level statement asserting equality of the upper and lower values of a convex-concave payoff function on subsets of \(\mathbb {R}\).

139.2 Declarations

Theorem 139.1 Convex-compact minimax theorem

✓

Let \(X, Y \subseteq \mathbb {R}\) and \(f : \mathbb {R}\to \mathbb {R}\to \mathbb {R}\) satisfy the bundled hypotheses \(\texttt{OnlineLearning.ConvexCompactMinimaxHypotheses}\): \(X\) is nonempty, compact and convex, \(Y\) is nonempty and convex, \(f\) is bounded above and below on \(X \times Y\), convex and continuous in the row variable for each \(y \in Y\), and concave in the column variable for each \(x \in X\). Then the minimax identity \(\texttt{OnlineLearning.ConvexCompactMinimaxStatement}\) holds:

\[ \inf _{x \in X} \sup _{y \in Y} f(x,y) \; =\; \sup _{y \in Y} \inf _{x \in X} f(x,y). \]

This is the public form of the theorem for the project; it hides the choice of proof route from downstream files.