110 Learning Theory — Convex Minimax No Regret

110.1 Overview

This module formalises the no-regret proof route for the convex-compact minimax theorem (Cesa-Bianchi–Lugosi Theorem 7.1). Starting from a finite-row sample lower value and the finite minimax theorem, it assembles three ingredients—a finite no-regret bound, a compact approximation step, and uniform equicontinuity—to establish the full minimax equality \(\inf _{x \in X} \sup _{y \in Y} f(x,y) = \sup _{y \in Y} \inf _{x \in X} f(x,y)\) under convexity, concavity, and compactness hypotheses.

110.2 Declarations

Definition 110.1 Finite row sample lower value

✓

Given a payoff \(f : \mathbb {R} \to \mathbb {R} \to \mathbb {R}\) and a finite subset \(u \subseteq X\), the finite row sample lower value is

\[ \sup _{y \in Y} \inf _{x \in u} f(x, y), \]

i.e. the lower value obtained when the row player is restricted to the finite sample \(u\) while the column player still ranges over all of \(Y\).

Definition 110.2 Finite no-regret bound predicate

✓

\(\texttt{OnlineLearning.Theorem71FiniteNoRegretBound}\) is the proposition asserting that for every nonempty finite row sample \(u \subseteq X\),

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

This is the finite-game no-regret ingredient in the Theorem 7.1 proof route.

Definition 110.3 Compact approximation predicate

✓

\(\texttt{OnlineLearning.Theorem71CompactApproximation}\) is the proposition asserting that for every \(\varepsilon \gt 0\) there exists a nonempty finite sample \(u \subseteq X\) such that

\[ \sup _{y \in Y} \inf _{x \in u} f(x, y) \; \le \; \sup _{y \in Y} \inf _{x \in X} f(x, y) + \varepsilon . \]

This encodes the “let the net size go to zero” compactness step of the textbook proof.

Definition 110.4 Uniform equicontinuity in the row variable

✓

\(\texttt{OnlineLearning.Theorem71UniformEquicontinuity}\) holds for \(X\), \(Y\), \(f\) when \(f\) is uniformly equicontinuous in its first argument uniformly over all columns: for every \(\varepsilon \gt 0\) there exists \(\rho \gt 0\) such that for all \(x, x' \in X\) and \(y \in Y\),

\[ \operatorname{dist}(x, x') \lt \rho \; \Longrightarrow \; |f(x,y) - f(x',y)| \lt \varepsilon . \]

Definition 110.5 Finite indexed row sample lower value

✓

For a row sample indexed by \(\mathrm{Fin}\, M\), the finite indexed row sample lower value is

\[ \sup _{y \in Y} \inf _{i \in \mathrm{Fin}\, M} f(x_i, y), \]

where \(x : \mathrm{Fin}\, M \to X\) is the sample. This is a technical variant of \(\texttt{OnlineLearning.finiteRowSampleLowerValue}\) used in intermediate results.

Theorem 110.6 Minimax from the Theorem 7.1 proof route

✓

If the standard convex-compact minimax hypotheses hold, the finite no-regret bound \(\texttt{OnlineLearning.Theorem71FiniteNoRegretBound}\) holds, and the compact approximation property \(\texttt{OnlineLearning.Theorem71CompactApproximation}\) holds, then the minimax equality

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

holds.

Theorem 110.7 Compact approximation from uniform equicontinuity

✓

Under the convex-compact minimax hypotheses, if \(f\) satisfies \(\texttt{OnlineLearning.Theorem71UniformEquicontinuity}\), then \(\texttt{OnlineLearning.Theorem71CompactApproximation}\) holds: a finite cover of the compact set \(X\) together with equicontinuity shows that the finite sample lower value approximates the full lower value to within any \(\varepsilon \gt 0\).

Theorem 110.8 Uniform equicontinuity from joint continuity on compact \(X \times Y\)

✓

If the convex-compact minimax hypotheses hold, \(Y\) is compact, and \((x,y) \mapsto f(x,y)\) is continuous on \(X \times Y\), then \(\texttt{OnlineLearning.Theorem71UniformEquicontinuity}\) holds. The proof applies the Heine–Cantor theorem to upgrade joint continuity on the compact product \(X \times Y\) to uniform continuity, then restricts variation to the first coordinate.

Theorem 110.9 Compact approximation from joint continuity on compact \(X \times Y\)

✓

Under the convex-compact minimax hypotheses, if \(Y\) is compact and \(f\) is jointly continuous on \(X \times Y\), then \(\texttt{OnlineLearning.Theorem71CompactApproximation}\) holds. This is obtained by combining \(\texttt{OnlineLearning.theorem71\_ uniformEquicontinuity\_ of\_ jointContinuous\_ compact}\) with \(\texttt{OnlineLearning.theorem71\_ compactApproximation\_ of\_ uniformEquicontinuity}\).

Theorem 110.10 Finite indexed no-regret bound (normalized)

✓

Under the convex-compact minimax hypotheses and the normalization \(0 \le f \le 1\), for any row sample \(x : \mathrm{Fin}\, M \to X\) with \(M \ge 2\),

\[ \inf _{x' \in X} \sup _{y \in Y} f(x', y) \; \le \; \sup _{y \in Y} \inf _{i \in \mathrm{Fin}\, M} f(x_i, y). \]

The proof constructs a finite matrix game with payoff \(1 - f\) on each finite column subset, applies the finite minimax theorem (via the upstream no-regret development), and uses compactness of \(X\) to pass to all columns.

Theorem 110.11 Finite no-regret bound (normalized, Finset version)

✓

Under the convex-compact minimax hypotheses and \(0 \le f \le 1\), \(\texttt{OnlineLearning.Theorem71FiniteNoRegretBound}\) holds. This removes the artificial \(\mathrm{Fin}\, M\) indexing from \(\texttt{OnlineLearning.theorem71\_ finiteIndexedNoRegretBound\_ normalized}\); the singleton case is handled separately since the finite minimax theorem requires at least two row actions.

Theorem 110.12 No-regret minimax equality (normalized, joint-compact)

✓

Under the convex-compact minimax hypotheses, if additionally \(Y\) is compact, \(f\) is jointly continuous on \(X \times Y\), and \(0 \le f \le 1\), then the minimax equality

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

holds. The proof combines the normalized finite no-regret bound with the compact approximation theorem derived from joint continuity on compact \(X \times Y\), without invoking any separation argument.