135 Learning Theory — Convex Minimax Separation
135.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)\).
135.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.
Let \(X, Y \subseteq \mathbb {R}\), let \(f : \mathbb {R}\to \mathbb {R}\to \mathbb {R}\) be a payoff function, and let \(u\) be a finite sample of columns from \(Y\). If \(X\) is nonempty, then the finite upper image \(U(X,f,u)\) is nonempty; that is, there exists a vector \(z : u \to \mathbb {R}\) for which some \(x \in X\) satisfies \(f(x,y) \lt z_y\) for every \(y \in u\).
Let \(X, Y \subseteq \mathbb {R}\), let \(f : \mathbb {R}\to \mathbb {R}\to \mathbb {R}\) be a payoff, and let \(u\) be a finite sample of columns from \(Y\). If \(X\) is convex and, for every \(y \in Y\), the map \(x \mapsto f(x,y)\) is convex on \(X\), then the finite upper image \(U(X,f,u)\) is a convex subset of \(u \to \mathbb {R}\).
Let \(X, Y \subseteq \mathbb {R}\), let \(f : \mathbb {R}\to \mathbb {R}\to \mathbb {R}\) be a payoff, and let \(u\) be a finite sample of columns from \(Y\). If a vector \(z : u \to \mathbb {R}\) belongs to the finite upper image \(U(X,f,u)\), and \(z' : u \to \mathbb {R}\) satisfies \(z_y \le z'_y\) for every \(y \in u\), then \(z'\) also belongs to \(U(X,f,u)\).
Let \(X, Y \subseteq \mathbb {R}\), let \(f : \mathbb {R}\to \mathbb {R}\to \mathbb {R}\) be a payoff function, and let \(u\) be a finite sample of columns from \(Y\). Then the finite upper image
is an open subset of the space \(u \to \mathbb {R}\) of vectors indexed by \(u\).
Let \(\iota \) be a finite index set and let \(L \colon \mathbb {R}^{\iota } \to \mathbb {R}\) be a continuous linear functional. Writing \(e_i\) for the standard basis vector whose \(i\)-th coordinate is \(1\) and whose other coordinates are \(0\), every vector \(z \in \mathbb {R}^{\iota }\) satisfies
Let \(X, Y \subseteq \mathbb {R}\), let \(f : \mathbb {R}\to \mathbb {R}\to \mathbb {R}\) be a payoff, let \(u\) be a finite sample of columns from \(Y\), and let \(c : u \to \mathbb {R}\) be a fixed vector. Suppose \(X\) is nonempty and \(L : (u \to \mathbb {R}) \to \mathbb {R}\) is a continuous linear functional such that \(L(z) \lt L(c)\) for every \(z\) in the finite upper image \(U(X,f,u)\). Then for each coordinate \(y \in u\) one has \(L(e_y) \le 0\), where \(e_y \in (u \to \mathbb {R})\) is the standard basis vector taking the value \(1\) at \(y\) and \(0\) elsewhere.
Let \(X, Y \subseteq \mathbb {R}\), let \(f : \mathbb {R}\to \mathbb {R}\to \mathbb {R}\) be a payoff, and let \(u\) be a finite sample of columns drawn from \(Y\), with \(X\) nonempty. Fix a vector \(c : u \to \mathbb {R}\) and a continuous linear functional \(L : (u \to \mathbb {R}) \to \mathbb {R}\). If \(L(z) \lt L(c)\) for every \(z\) in the finite upper image \(U(X,f,u)\), then \(L\) is not the zero functional.
Let \(X, Y \subseteq \mathbb {R}\), let \(f : \mathbb {R}\to \mathbb {R}\to \mathbb {R}\) be a payoff function, and let \(u\) be a finite sample of columns drawn from \(Y\). Suppose \(X\) is nonempty, fix a vector \(c \in \mathbb {R}^u\), and let \(L : \mathbb {R}^u \to \mathbb {R}\) be a continuous linear functional that strictly separates \(c\) from the finite upper image \(U(X,f,u)\), in the sense that \(L(z) \lt L(c)\) for every \(z \in U(X,f,u)\). Writing \(e_y \in \mathbb {R}^u\) for the standard basis vector supported at coordinate \(y\), one then has
Let \(X, Y \subseteq \mathbb {R}\) and \(f : \mathbb {R}\times \mathbb {R}\to \mathbb {R}\) satisfy the convex-compact minimax hypotheses, and write \(v = \sup _{y \in Y} \inf _{x \in X} f(x,y)\) for the lower value of the payoff. Then for every \(\varepsilon \gt 0\) and every finite set \(u\) of columns chosen from \(Y\), there is a row \(x \in X\) with \(f(x,y) \le v + \varepsilon \) simultaneously for all \(y \in u\); equivalently, the intersection over \(y \in u\) of the sublevel sets \(\{ x \in X : f(x,y) \le v + \varepsilon \} \) is nonempty.
Let \(X, Y \subseteq \mathbb {R}\) with \(X\) and \(Y\) nonempty, \(X\) compact and convex, and \(Y\) convex, and let \(f : \mathbb {R}\times \mathbb {R}\to \mathbb {R}\) be bounded above and below on \(X \times Y\), with \(f(\cdot , y)\) continuous and convex on \(X\) for every \(y \in Y\) and \(f(x, \cdot )\) concave on \(Y\) for every \(x \in X\). Write \(v = \sup _{y \in Y} \inf _{x \in X} f(x,y)\) for the lower value, and suppose that for every \(\varepsilon \gt 0\) and every finite set \(u\) of column points from \(Y\), the set
is nonempty. Then the minimax equality
holds.
Let \(X, Y \subseteq \mathbb {R}\) be nonempty sets with \(X\) compact and both \(X\) and \(Y\) convex, and let \(f : \mathbb {R}\times \mathbb {R}\to \mathbb {R}\) be a payoff function that is bounded above and below on \(X \times Y\). Suppose that for every \(y \in Y\) the section \(x \mapsto f(x,y)\) is continuous and convex on \(X\), while for every \(x \in X\) the section \(y \mapsto f(x,y)\) is concave on \(Y\). Then the minimax equality
holds.
135.3 Additional declarations
Let \(X, Y \subseteq \mathbb {R}\), let \(f : \mathbb {R}\to \mathbb {R}\to \mathbb {R}\) be a payoff, let \(u\) be a finite sample of columns from \(Y\), and let \(c \in \mathbb {R}\). Suppose \(L : \mathbb {R}^u \to \mathbb {R}\) is a continuous linear functional separating the constant vector \((c,\dots ,c)\) from the finite upper image, i.e. \(L(z) \lt L(c,\dots ,c)\) for every \(z \in U(X,f,u)\), and that the total weight \(W = \sum _{y \in u} \bigl(-L(e_y)\bigr)\) is strictly positive, where \(e_y\) is the standard basis vector at \(y\). Then for every row \(x \in X\),
that is, \(c\) is at most the payoff of \(x\) averaged under the normalized weights \(-L(e_y)/W\).