140 Learning Theory — Convex Minimax Separation
140.1 Overview
This module proves the convex-compact minimax theorem by a Hahn–Banach separation route. For each finite sample \(u\) of columns it forms the upper image of the payoff on that sample, separates the constant vector \((v+\varepsilon ,\dots ,v+\varepsilon )\) from it by a continuous linear functional, and normalizes the coordinates of that functional into a mixed column strategy. This yields the finite sublevel intersection property, which combined with compactness of the row set gives the minimax identity \(\inf _{x} \sup _{y} f(x,y) = \sup _{y} \inf _{x} f(x,y)\).
140.2 Declarations
For sets \(X, Y \subseteq \mathbb {R}\), a payoff \(f : \mathbb {R}\to \mathbb {R}\to \mathbb {R}\), and a finite sample \(u\) of columns from \(Y\), the finite upper image is the set
of vectors that strictly dominate the payoff vector of some row on the sample \(u\). This set is written \(\texttt{OnlineLearning.finiteUpperImage}\) in Lean.
If \(X\) is nonempty, then for every finite column sample \(u\) the upper image \(U(X,f,u)\) is nonempty.
If \(X\) is convex and \(x \mapsto f(x,y)\) is convex on \(X\) for every \(y \in Y\), then \(U(X,f,u)\) is a convex subset of \(u \to \mathbb {R}\) for every finite column sample \(u\).
If \(z \in U(X,f,u)\) and \(z_y \le z'_y\) for all \(y \in u\), then \(z' \in U(X,f,u)\) as well; that is, the upper image is closed under coordinatewise increase.
For every finite column sample \(u\), the upper image \(U(X,f,u)\) is an open subset of \(u \to \mathbb {R}\).
Let \(\iota \) be a finite type and \(L\) a continuous linear functional on \(\iota \to \mathbb {R}\). Then for every \(z : \iota \to \mathbb {R}\),
where \(e_i\) is the standard basis vector \(\mathrm{Pi.single}\, i\, 1\).
Assume \(X\) is nonempty and \(L\) is a continuous linear functional on \(u \to \mathbb {R}\) with \(L(z) \lt L(c)\) for every \(z \in U(X,f,u)\), where \(c\) is a fixed vector. Then \(L(e_y) \le 0\) for every coordinate \(y \in u\).
Under the same separation hypothesis \(L(z) \lt L(c)\) for all \(z\) in the upper image, with \(X\) nonempty, the functional \(L\) is not the zero functional.
Under the same separation hypothesis, with \(X\) nonempty,
Consequently the negated coordinates can be normalized to a probability vector on the sampled columns.
Assume the convex-compact minimax hypotheses \(\texttt{OnlineLearning.ConvexCompactMinimaxHypotheses}\) for \(X\), \(Y\), \(f\). Then for every \(\varepsilon \gt 0\) and every finite column sample \(u \subseteq Y\), the set
is nonempty, the inner sets being the sublevel sets \(\texttt{OnlineLearning.minimaxSublevel}\); i.e. some row \(x \in X\) satisfies \(f(x,y) \le v + \varepsilon \) simultaneously for all sampled columns \(y \in u\).
Assume the hypotheses \(\texttt{OnlineLearning.ConvexCompactMinimaxHypotheses}\) for \(X\), \(Y\), \(f\), and suppose that for every \(\varepsilon \gt 0\) and every finite \(u \subseteq Y\) the intersection of \(X\) with the sublevel sets \(\texttt{OnlineLearning.minimaxSublevel}\) at level \(v + \varepsilon \) over \(y \in u\) is nonempty, where \(v = \sup _{y \in Y} \inf _{x \in X} f(x,y)\). Then the minimax identity \(\texttt{OnlineLearning.ConvexCompactMinimaxStatement}\) holds for \(X\), \(Y\), \(f\), i.e.
Under the convex-compact minimax hypotheses \(\texttt{OnlineLearning.ConvexCompactMinimaxHypotheses}\) for \(X\), \(Y\), \(f\), the minimax identity \(\texttt{OnlineLearning.ConvexCompactMinimaxStatement}\) holds:
This is the final form of the theorem obtained via the finite-column separation route.