Machine Learning

Motivation

Reinforcement learning formalizes a scenario supervised learning cannot: an agent that actively interacts with an environment, choosing actions that change both the state it observes next and the reward it receives, rather than passively receiving an i.i.d. labeled sample. Every practical treatment of this scenario — from classical dynamic programming to modern deep reinforcement learning — is built on the Markov decision process (MDP), a model in which the effect of an action depends only on the current state, not on the full history that led to it. Two questions define the theory this mission covers: given a fixed way of acting (a policy), what value does it obtain, and how is that value actually computed rather than merely characterized as the solution of a fixed-point equation? Mohri, Rostamizadeh and Talwalkar's chapter 17 answers both for the stationary, infinite-horizon discounted case, and this mission targets its two central results: that a fixed policy's value is not just characterized but uniquely determined by a linear system with an explicit closed-form solution (Theorem 17.10), and that the optimal value function — obtained instead by choosing the best action at every state — can be computed by an iterative algorithm guaranteed to converge regardless of where it starts (Theorem 17.11).

Setting

A (finite) Markov decision process consists of a finite set of states $S$, a finite set of actions $A$, a transition kernel $P[s'\mid s,a]$ giving the distribution over the next state $s'$ after taking action $a$ at state $s$, and an expected reward $\mathbb E[r(s,a)]$ for that transition. A (stationary) policy $\pi:S\to\Delta(A)$ assigns each state a distribution over actions — possibly, but not necessarily, a point mass on a single action. Fixing $\pi$ turns the MDP into an ordinary Markov chain on $S$: at each step the agent is at some state $s$, draws $a\sim\pi(s)$, receives (expected) reward $\mathbb E[r(s,a)]$, and moves to a state drawn from $P[\cdot\mid s,a]$. For a discount factor $\gamma\in[0,1)$, the value of $\pi$ at $s$ is the expected discounted sum of future rewards starting from $s$,

$$V_\pi(s) = \mathbb E_{a_t\sim\pi(s_t)}\Big[\sum_{t=0}^{+\infty}\gamma^t r(s_t,a_t) \;\Big|\; s_0=s\Big],$$

and the state-action value function $Q_\pi(s,a)$ is the analogous quantity for taking $a$ at $s$ and then following $\pi$. Marginalizing the raw kernel and reward over the mixed action $\pi(s)$ gives the induced transition matrix $P_{s,s'}=P[s'\mid s,\pi(s)]=\sum_a \pi(s)(a) P[s'\mid s,a]$ and induced reward vector $R_s=\mathbb E[r(s,\pi(s))]=\sum_a\pi(s)(a)\,\mathbb E[r(s,a)]$ — the objects that turn $\pi$'s value into a genuinely linear-algebraic quantity. A policy $\pi^*$ is optimal if $V_{\pi^*}(s)\ge V_\pi(s)$ for every policy $\pi$ and every state $s$; write $V^*$ for its value function.

Formalization targets

Theorem 17.10 (goal). For a finite MDP and a fixed policy $\pi$, the matrix $I-\gamma P$ (with $P$ the policy-induced transition matrix) is invertible, and $\pi$'s value function is the unique solution of the Bellman equations, given in closed form by

$$V_\pi = (I-\gamma P)^{-1} R.$$

Proposition 17.9 (milestone). The value function itself satisfies the linear system that Theorem 17.10 solves:

$$\forall s\in S,\quad V_\pi(s) = \mathbb E_{a\sim\pi(s)}[r(s,a)] + \gamma\sum_{s'} P[s'\mid s,\pi(s)]\,V_\pi(s').$$

Theorem 17.7 (milestone). A policy $\pi$ is optimal if and only if it places probability only on $Q_\pi$-maximizing actions: for every $(s,a)$ with $\pi(s)(a)>0$, $a\in \operatorname{argmax}_{a'} Q_\pi(s,a')$.

Theorem 17.11 (milestone). The Bellman optimality operator $\Phi$, $[\Phi(V)](s)=\max_{a} \{\mathbb E[r(s,a)]+\gamma\sum_{s'}P[s'\mid s,a]V(s')\}$, is a $\gamma$-contraction for $\lVert\cdot\rVert_\infty$; consequently, for any starting vector $V_0$, the value-iteration sequence $V_{n+1}=\Phi(V_n)$ converges to a fixed point of $\Phi$.

Significance

Theorem 17.10 is what makes policy evaluation on a finite MDP an exact, finite computation rather than an infinite limit: instead of summing an infinite discounted series or solving an implicit fixed-point equation numerically, a single $|S|\times|S|$ matrix inversion gives the policy's value at every state simultaneously. It is also the base case every planning algorithm in the chapter builds on: policy iteration alternates optimizing a policy with exactly this evaluation step. Theorem 17.11 gives the complementary guarantee for the harder problem of finding the optimal value function directly, without fixing a policy first: value iteration converges from any starting point, with a convergence rate ($O(\log(1/\epsilon))$ iterations for $\epsilon$-accuracy) that follows from the same contraction argument. Together, the two results are the mathematical content behind why dynamic-programming planning for finite MDPs is tractable at all — the discount factor $\gamma<1$, not any structural assumption on rewards or transitions, is what buys both the uniqueness in Theorem 17.10 and the convergence in Theorem 17.11. Formalizing them requires reproducing this linear-algebraic and metric content precisely, not just asserting the conclusions: an invertibility claim asserted without the operator-norm argument, or a convergence claim without the contraction property, would state something true by fiat rather than the book's actual result. No faithful prior art exists on the platform for this exact model (see Formalization scope).

Difficulty

The obvious shortcut for Theorem 17.10 is to assert $I-\gamma P$ is invertible without proof — true, but not what the book does, and not informative about why it holds. The genuine content is that $P$, being row-stochastic (every row of $P$ sums to exactly $1$, since $\pi(s)$ and $P[\cdot\mid s,a]$ are both proper distributions), has operator norm $\lVert P\rVert_\infty=1$ exactly, so $\lVert\gamma P\rVert_\infty=\gamma<1$ strictly; this rules out $1$ as an eigenvalue of $\gamma P$, which is exactly what invertibility of $I-\gamma P$ requires. The same $\gamma<1$ fact, applied differently, drives Theorem 17.11: showing $\Phi$ is $\gamma$-Lipschitz requires bounding $\Phi(V)(s)-\Phi(U)(s)$ by comparing the maximizing action for $V$ against the same action's value under $U$ (not $U$'s own maximizer), since the two suprema need not be attained at the same action — a step easy to state incorrectly as a direct comparison of two maxima. Both theorems fail if $\gamma=1$ is allowed: the discounted setting's central asset, a strict contraction, disappears exactly at that boundary.

Formalization scope

States and actions are modeled as finite types (Fintype S, Fintype A); the raw kernel and reward P : S → A → S → ℝ, Er : S → A → ℝ are unconstrained functions, with IsTransitionKernel asserting the required distribution property explicitly rather than assuming it silently. A policy is π : S → A → ℝ with IsPolicy π asserting π s is a distribution over A for every s — deliberately not π : S → A or a PMF-valued function, since Theorem 17.7's own quantifier ("for any pair (s,a) with π(s)(a) > 0") requires treating π(s) as a genuine mixture. PolicyValue is defined as the actual infinite discounted expectation (via an explicit state-occupation-distribution recursion), not as the Bellman fixed point — so that Proposition 17.9 (the value function satisfies the linear system) and Theorem 17.10 (that system has a unique, invertible-matrix solution) are both non-vacuous claims about the same object, rather than one being definitionally true of the other. The trivializing formalization this rules out is asserting IsUnit (1 - γ • P) as a bare hypothesis, or defining V_π as (1-γP)⁻¹R and calling the resulting identity a theorem; both would erase the mission's actual content. Two platform modules model related MDPs (BertsekasSSPModel, a stochastic-shortest-path model with a termination-probability deficit rather than exact row-stochasticity, and FoundationsRL.RLBasics, a finite-horizon episodic model indexed by layer) — neither specializes exactly to this chapter's stationary, always-continuing, infinite-horizon discounted convention, so every definition here is drafted fresh rather than imported. This chunk covers §17.2–17.4.2 (the MDP model, policy value, Bellman's equations, value and policy iteration); §17.4.3 (the linear-programming formulation) and §17.5 (stochastic-approximation learning algorithms — TD(0), Q-learning, SARSA) are out of scope, since they require a stochastic-approximation convergence substrate this mission does not build.

Selected references

• Mohri, M., Rostamizadeh, A., and Talwalkar, A. Foundations of Machine Learning, 2nd ed., chapter 17. MIT Press, 2018.
• Bellman, R. Dynamic Programming. Princeton University Press, 1957.
• Puterman, M. L. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, 1994.

Motivation

Ranking is the learning problem behind search engines, recommendation systems and fraud-alert triage: what matters is not a single classification decision but the relative order the system assigns to a set of items, because a user or analyst can only act on the very top of a ranked list. Chapter 10 develops margin-based generalization theory for the score-based ranking setting, transplanting chunk 05-svm's single-sample Rademacher-complexity machinery to a genuinely two-sample structure: a ranking example is a pair of points, one drawn from each of two positions, and the chapter's bound must therefore control two marginal complexities rather than one. It also introduces RankBoost, the ranking analogue of AdaBoost, with a boosting-style empirical-error guarantee proved by the same normalization-factor telescoping argument as chunk 07's AdaBoost bound, adapted to RankBoost's own pairwise per-round quantities.

Setting

A ranking example is a pair (x,x') drawn from a distribution D over X×X, labeled by a preference function f; restricted to {-1,+1} labels (the simplification §10.2 adopts), a scoring function h:X→ℝ misranks (x,x') when f(x,x')(h(x')-h(x)) ≤ 0 (Eq. 10.1/10.2). The empirical margin loss R̂_{S,ρ}(h) (Eq. 10.3) uses the same Φ_ρ (Definition 5.5) as chunk 05-svm, restated locally here. Writing S1, S2 for the two coordinate projections of a pair sample S, and D1, D2 for the corresponding marginals of D, R_m^{D1}(H) and R_m^{D2}(H) are the Rademacher complexities of H under each marginal (p. 241). Theorem 10.1 bounds R(h) in terms of these two Rademacher-complexity terms, both in their population form (R_m^{D1}, R_m^{D2}) and their empirical form (R̂_{S1}, R̂_{S2}), via chunk 03's Theorem 3.3 applied through an auxiliary hypothesis family H̃ = {((x,x'),y) ↦ y[h(x')-h(x)]}. Corollary 10.2 specializes this to kernel-based linear scoring hypotheses; §10.4 introduces RankBoost (Figure 10.1), whose per-round weighted pairwise-outcome fractions ε_t^+, ε_t^- (Eq. 10.11) play the role AdaBoost's single ε_t plays in chunk 07, and Theorem 10.3 bounds RankBoost's empirical error in terms of them. Corollary 10.4 combines Theorem 10.1 with Lemma 7.4 (the convex hull of H has the same empirical Rademacher complexity as H, restated as a standing fact of the boosting series) to give RankBoost's own margin-based guarantee.

Formalization targets

Theorem 10.1 — the mission's goal. For H a set of real-valued functions, ρ>0, δ>0, with probability at least 1-δ, for all h∈H:

$$R(h) \le \hat R_{S,\rho}(h) + \tfrac2\rho(R_m^{D_1}(H)+R_m^{D_2}(H)) + \sqrt{\tfrac{\log(1/\delta)}{2m}}$$ $$R(h) \le \hat R_{S,\rho}(h) + \tfrac2\rho(\hat R_{S_1}(H)+\hat R_{S_2}(H)) + 3\sqrt{\tfrac{\log(2/\delta)}{2m}}.$$

Corollary 10.2 (milestone). For a PDS kernel K with r an upper bound on K(x,x), feature map Φ, and H = {x↦w·Φ(x) : ‖w‖≤Λ}, fixed ρ>0: R(h) ≤ R̂_{S,ρ}(h) + 4√(r²Λ²/ρ²/m) + √(log(1/δ)/(2m)).

Theorem 10.3 (milestone). RankBoost's empirical error verifies R̂_S(f) ≤ exp(-2∑_t((ε_t^+-ε_t^-)/2)²), and ≤ exp(-2γ²T) if the edge is uniformly at least γ>0.

Corollary 10.4 (milestone). Theorem 10.1's first bound, applied to h∈conv(H).

Significance

Theorem 10.1's proof is the chapter's genuine new technique, not a restatement of chunk 05's Theorem 5.8: the two-sample decomposition (splitting the supremum over H̃ into a term on x' alone and a term on x alone, each bounded by the Rademacher complexity under its own marginal) is what the 2/ρ · (R_m^{D1}+R_m^{D2}) structure expresses, and collapsing it to a single-sample bound would either be false or silently assume D1=D2 (which only holds for a symmetric D, an assumption the theorem does not make). Corollary 10.2 is the direct theoretical basis for the ranking SVM algorithm §10.3 derives. Theorem 10.3 mirrors chunk 07-boosting's Theorem 7.2 almost line for line in its proof technique (the same telescoping product of normalization factors Z_t), but with genuinely different per-round quantities (ε_t^+, ε_t^- rather than a single ε_t) that must not be conflated with AdaBoost's own, per BRIEF.md's pitfall note. Corollary 10.4 is what makes RankBoost's output (a linear, not convex, combination — normalized by ‖α‖_1) provably generalize independently of the number of boosting rounds T, the ranking analogue of chunk 07's Corollary 7.5. No prior art exists on the platform: GET /theorems?q=ranking%20loss returns zero hits.

Difficulty

Theorem 10.1's proof needs the two-sample structure carried through explicitly: H̃'s Rademacher complexity splits, via the sub-additivity of sup and the fact that y_iσ_i and σ_i have the same distribution, into a term on S2 alone and a term on S1 alone — treating a ranking sample as an ordinary single sample (chunk 03's single-hypothesis-set machinery applied naively) would drop this structure entirely and is exactly the pitfall BRIEF.md names. Theorem 10.3's proof requires Z_t = ε_t^0 + 2√(ε_t^+ε_t^-) be bounded via the identity 4ε_t^+ε_t^- = (1-ε_t^0)^2 - (ε_t^+-ε_t^-)^2 and the inequality 1-x ≤ e^{-x} — the same telescoping-normalizer technique as AdaBoost's Theorem 7.2, but RankBoost's own D_t, ε_t^+, ε_t^- genuinely differ (they are defined via pairwise outcomes y_i(h(x'_i)-h(x_i)) ∈ {-1,0,+1}, not a single-point disagreement h(x_i)≠y_i) and must be modeled as their own recursively-defined algorithm state, not obtained by substitution into chunk 07's AdaBoost Lean.

Formalization scope

MarginLossFunction restates chunk 05-svm's Definition 5.5; EmpiricalRademacherComplexity/ RademacherComplexity restate chunk 03-rademacher-vc's Definitions 3.1/3.2; IsPDS restates chunk 06-kernels's PDS-kernel definition; ConvHull restates chunk 07-boosting's convex-hull definition — all duplicated rather than imported since a draft item cannot import another chunk's draft module, and none is listed as reusable in missions/README.md's "Published definitions" table at the time of this session. D1, D2 are computed directly as Measure.map Prod.fst D/Measure.map Prod.snd D rather than posited via a separate marginal hypothesis, so the theorem statement itself pins down that they are genuinely the marginals of the sampling distribution D, not independent parameters. Corollary 10.2's r is an explicit upper bound on K(x,x) (hrK : ∀ x, K x x ≤ r) rather than a literal sSup, per BRIEF.md's pitfall note about the possibly-infinite supremum — the theorem's conclusion is monotonic in r, so this is not a weakening. RankBoost's D_t, ε_t^+, ε_t^-, α_t, Z_t and returned function f are modeled as their own recursively-defined algorithm state (mirroring chunk 07's AdaBoostDist/AdaBoostEpsilon/AdaBoostEnsemble pattern exactly, but built from RankBoost's own pairwise-outcome quantities, never by substituting into the AdaBoost Lean, per BRIEF.md's pitfall note) — RankBoostEpsilonPlus/RankBoostEpsilonMinus are already tied to RankBoost's own D_t and selected base ranker, so Theorem 10.3 needs no separate hypothesis connecting them (the same trivialization guard chunk 07's own Theorem 7.2 documents). No numerical constant is altered from the book in any of the four theorems.

Not formalized: §10.3's ranking-SVM primal/dual optimization problems (an algorithm derived from Corollary 10.2, not a generalization-theoretic result); §10.4.2 (RankBoost as coordinate descent, an algorithmic-equivalence argument, not a generalization bound); §10.5 (bipartite ranking, its own distinct problem formulation with a different generalization error, Eq. 10.20, explicitly out of scope per BRIEF.md); §10.6-10.7 (preference-based ranking, other criteria), out of scope per BRIEF.md. The uniform-over-ρ extension mentioned after both Theorem 10.1's and Corollary 10.2's proofs (referencing Theorem 5.9's technique from a different chapter) is not drafted, matching chunk 09-multiclass's identical scope decision for the analogous remark.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 10 (§10.1-10.4).
• Y. Freund, R. Iyer, R. E. Schapire, Y. Singer, "An efficient boosting algorithm for combining preferences," JMLR 4, 2003 (RankBoost's origin).
• C. Cortes, M. Mohri, "AUC optimization vs. error rate minimization," NeurIPS 2003 (the ranking-SVM connection §10.3 develops).

Motivation

Every convergence-rate result in the preceding chapters is an upper bound: some specific estimator (the Lasso, PCA, kernel ridge regression) achieves a given error rate. A natural and much harder question is the complementary one: is that rate actually the best any procedure could achieve, no matter its computational cost? Answering this requires a theory of lower bounds that holds simultaneously for every conceivable estimator — a fundamentally different kind of argument from constructing and analyzing one particular algorithm. Wainwright's High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 15, develops this theory, unifying classical techniques (Le Cam, Assouad, Fano) under one reduction: converting continuous estimation into discrete hypothesis testing.

Setting

Let $\mathcal X$ be a sample space and $\mathcal P$ a class of probability distributions on $\mathcal X$. A functional $\theta: \mathcal P \to \Omega$ assigns each distribution a parameter of interest. An estimator is a measurable map $\hat\theta: \mathcal X \to \Omega$. Fix a semi-metric $\rho:\Omega\times\Omega\to[0,\infty)$ — symmetric, triangle-inequality-satisfying, $\rho(\theta,\theta)=0$, but possibly $\rho(\theta,\theta')=0$ for $\theta\ne\theta'$ — and an increasing $\Phi:[0,\infty)\to[0,\infty)$. The minimax risk is

$$\mathfrak M\bigl(\theta(\mathcal P); \Phi\circ\rho\bigr) \;:=\; \inf_{\hat\theta} \sup_{P\in \mathcal P} \mathbb E_P\bigl[\Phi\bigl(\rho(\hat\theta, \theta(P))\bigr)\bigr],$$

the smallest worst-case expected loss achievable by any measurable estimator (Eq. (15.2)).

Given a 2δ-separated set $\{\theta_1,\dots,\theta_M\} \subseteq \theta(\mathcal P)$ (every pair satisfies $\rho(\theta_j,\theta_k)\ge 2\delta$) with representative distributions $P_{\theta_1},\dots,P_{\theta_M}$, Wainwright constructs a testing problem: sample $J$ uniformly from $[M]$, then $Z\sim P_{\theta_J}$; write $Q$ for the resulting joint law of $(J,Z)$. A test function $\psi:\mathcal X\to[M]$ attempts to recover $J$ from $Z$; its error probability is $Q[\psi(Z)\ne J]$.

Formalization targets

Goal (Proposition 15.1, "From estimation to testing")

For any increasing $\Phi$ and any 2δ-separated set with its induced joint testing measure $Q$,

$$\mathfrak M\bigl(\theta(\mathcal P); \Phi\circ\rho\bigr) \;\ge\; \Phi(\delta) \inf_{\psi} Q\bigl[\psi(Z)\ne J\bigr].$$

This mission formalizes Proposition 15.1 alone (see Formalization scope below for why, and what a follow-up mission would add to reach Fano's method proper, Proposition 15.12).

Significance

Proposition 15.1 is the single reduction every subsequent technique in the chapter specializes: Le Cam's two-point method (Lemma 15.9, $M=2$, bounding the testing error via total variation distance), Fano's method (Proposition 15.12, bounding it via mutual information $I(Z;J)$ and Fano's inequality), and Assouad's method (a different, hypercube-based packing). Formalizing it in full generality — general $\Phi$, general semi-metric, general $M$-ary packing set — gives a single reusable lemma that a future mission proving any of these specific bounds can build on directly, rather than re-deriving the reduction each time.

The theorem is already proved in the source; this mission's contribution is a machine-checked formal statement (and, eventually, proof) of the reduction, in a form composing with any future formalization of the chapter's testing-error bounds (total variation, Fano, or otherwise).

Difficulty

The proof combines two ingredients that must each be kept in their sharpest form: Markov's inequality applied to $\Phi(\rho(\hat\theta,\theta))$ (which only needs $\Phi$ increasing, not convex or any specific shape — a premature specialization to $\Phi(t)=t^2$ would silently prove a weaker, less reusable statement), and the reduction of any estimator to a test via nearest- packing-point assignment (Eq. (15.4)), which uses the triangle inequality on $\rho$ in a specific direction (bounding $\rho(\theta_k,\hat\theta)$ from below via $\rho(\theta_j,\theta_k)$ and $\rho(\theta_j,\hat\theta)$) to show that a small estimation error forces the induced test to be correct. Getting the direction and strictness of every inequality right — non-strict separation, but strict distance in the "test is correct" event — is where a naive restatement goes wrong.

Formalization scope

$\mathcal X$, $\Omega$ are arbitrary measurable spaces; the distribution class $\mathcal P$ is realized as an indexed family measure : Idx → Measure 𝒳 rather than a bare set of measures, composing directly with θ : Idx → Ω. The semi-metric $\rho$ is a bare function with explicit nonnegativity/reflexivity/symmetry/triangle-inequality hypotheses, matching the book's own footnote definition, rather than Mathlib's PseudoMetricSpace typeclass (kept self-contained, no extra instance machinery). The minimax risk is valued in ENNReal via the lower Lebesgue integral ∫⁻, not the Bochner integral, specifically to avoid the non-integrable-loss junk value 0 that a Bochner-integral formalization would silently introduce — a trivializing formalization would use ∫ (Bochner) here, letting a non-integrable loss vanish and making the inequality easier to satisfy than the book's actual claim; this mission does not do that. The joint testing measure $Q$ is characterized by its slice-measure equations directly on the product space $[M]\times\mathcal X$, avoiding Mathlib's general conditional/disintegration machinery while remaining exactly equivalent to "$J$ uniform, $Z\mid J=j\sim P_{\theta_j}$".

Disclosed major scope decision. BRIEF.md recommended Proposition 15.12 (the Fano bound itself, Φ(δ)(1 - (I(Z;J)+\log 2)/\log M)) as this mission's goal. That statement requires, in addition to everything above, a formalized notion of mutual information $I(Z;J)$ between a finite-valued and a general (possibly continuous) random variable, and its use of a Fano-type inequality (Eq. (15.31), itself deferred by the book to "Section 15.4" and not fully quoted in the brief). Building a faithful mutual-information formalization general enough for this setting (finite $J$, arbitrary measurable $Z$) — matching Mathlib's or this repo's existing, narrower information-theoretic developments (SourceCoding.*, built for a different, channel-coding purpose per BRIEF.md's own prior-art note) or building one from scratch — is substantially more than this session's remaining budget after building and self-reviewing 08-pca and 07-sparse-linear. This mission instead formalizes Proposition 15.1, the foundational reduction Proposition 15.12 itself specializes (via a particular bound on $\inf_\psi Q[\psi(Z)\ne J]$), so that a follow-up mission can add the mutual-information/Fano step on top of HighDimStat.Minimax.estimation_to_testing without redoing this reduction. This mission's name, fixed from missions/README.md, still names "Fano's Method" as the series slot this chunk occupies; its actual content is the reduction step every method in that family (including Fano's) shares — recorded explicitly here and in STATUS.md, not left implicit.

Selected references

• Wainwright, M. J. High-Dimensional Statistics: A Non-Asymptotic Viewpoint. Cambridge University Press, 2019. Chapter 15. DOI: 10.1017/9781108627771.
• Le Cam, L. "Convergence of estimates under dimensionality restrictions." Annals of Statistics, 1(1), 1973, 38–53.
• Fano, R. M. Transmission of Information: A Statistical Theory of Communications. MIT Press, 1961.
• Yu, B. "Assouad, Fano, and Le Cam." In Festschrift for Lucien Le Cam, Springer, 1997, 423–435.

Motivation

Every convex optimization algorithm in machine learning — from projected gradient descent to support vector machines to the mirror-descent methods of later chapters of this book — is justified by a small set of optimality certificates: a checkable condition on a candidate solution that guarantees it actually solves the problem, without searching the whole feasible set. The most widely used such certificate is the Karush–Kuhn–Tucker (KKT) system: a set of gradient and complementary-slackness equations that a solution of a convex program with differentiable data must satisfy, and that (under a mild constraint qualification) is also sufficient. It is the tool a practitioner reaches for to check optimality of a numerical solver's output, and the tool a theorist reaches for to derive an algorithm (dual ascent, augmented Lagrangian, interior point methods) in the first place. Every convex machine learning model introduced in Chapter 1 of this book — regularized least squares, support vector machines, logistic regression with constraints — is an instance of the general convex program these milestones analyze.

The result traces back to Kuhn and Tucker's 1951 paper Nonlinear Programming, with Karush's 1939 unpublished thesis establishing the same conditions independently and earlier; Slater's 1950 unpublished note is the source of the constraint qualification that bears his name and that makes the necessity direction possible. Lan's Chapter 2 gives a compact, modern, purely finite-dimensional derivation of the whole chain — separation, duality, saddle points, KKT — from first principles, self-contained in about twenty pages, aimed squarely at the convex programs that appear in machine learning.

Setting

Fix $n, m, p \in \mathbb{N}$ and work in $\mathbb{R}^n$ with its standard inner product $\langle \cdot,\cdot\rangle$. A convex program (2.3.16) is

$$f^* \equiv \min_{x \in X} f(x) \quad \text{s.t.} \quad g_i(x) \le 0\ (i=1,\dots,m), \quad h_j(x) = 0\ (j=1,\dots,p),$$

where $X \subseteq \mathbb{R}^n$ is a nonempty closed convex set, $f, g_1,\dots,g_m : X \to \mathbb{R}$ are convex, and $h_1,\dots,h_p$ are affine. A point $x \in X$ is feasible if it satisfies every $g_i(x)\le 0$ and $h_j(x)=0$; $x^*$ is optimal if it is feasible and $f(x^*)\le f(x)$ for every feasible $x$.

The normal cone of $X$ at $x$ is $N_X(x) := \{w \in \mathbb{R}^n : \langle w, y-x\rangle \le 0 \ \forall y \in X\}$ — the set of directions that make an obtuse angle with every direction into $X$ from $x$; it is $\{0\}$ when $X = \mathbb{R}^n$, recovering unconstrained first-order optimality. The Lagrangian is $L(x,\lambda,y) := f(x) + \sum_i \lambda_i g_i(x) + \sum_j y_j h_j(x)$ for multipliers $\lambda \ge 0$, $y \in \mathbb{R}^p$; the Lagrange dual value is $\varphi(\lambda,y) := \min_{x\in X} L(x,\lambda,y)$, and the Lagrange dual problem is $\varphi^* := \max_{\lambda\ge 0,\,y}\varphi(\lambda,y)$. Weak duality, $\varphi^*\le f^*$, holds unconditionally by construction. Slater's condition asks for $\bar x \in \operatorname{int} X$ with $g(\bar x) < 0$, $h(\bar x)=0$; the restricted Slater condition weakens the interior requirement to the relative interior $\operatorname{rint} X$ while keeping strict inequality for every (here: every) nonlinear constraint.

Formalization targets

Goal — Theorem 2.8(b), KKT necessity

$$x^* \text{ optimal (with a restricted-Slater point)} \implies \exists\, \lambda^*\ge 0,\, y^*: \ \nabla f(x^*) + \sum_i \lambda_i^* \nabla g_i(x^*) + \sum_j y_j^* \nabla h_j(x^*) \in N_X(x^*), \ \lambda_i^* g_i(x^*) = 0\ \forall i.$$

Companion — Theorem 2.8(a), KKT sufficiency

$$\exists\, \lambda^* \ge 0,\, y^* \text{ satisfying stationarity and complementary slackness at a feasible, differentiable } x^* \implies x^* \text{ optimal.}$$

Supporting milestones, in attack order

• Theorem 2.1 (separation): a point outside a closed convex set is strictly separated from it by a hyperplane.
• Proposition 2.9 (Convex Theorem on Alternative): insolvability of a strict-inequality system, plus a Slater point, forces solvability of a dual multiplier system.
• Theorem 2.6 (strong duality): under Slater's condition, $\varphi^* = f^*$ and the dual is solvable.
• Theorem 2.7(a)/(b) (saddle points): $x^*$ is optimal iff it extends to a saddle point of $L$ (the "only if" needs Slater's condition; the "if" needs nothing beyond the saddle inequalities).

Each of these five is stated the way the book states it — no constant is hard-coded, no O(·) is involved, and every hypothesis (closedness, convexity, Slater/restricted-Slater) is exactly the one the corresponding proof uses.

Significance

The KKT system is the interface between convex optimization theory and every algorithm that exploits it: primal-dual methods track approximate KKT residuals as a stopping criterion, and the derivation of the Lagrange dual (used throughout the book's later treatment of composite and constrained problems) rests on strong duality, milestone strong_duality here. The saddle-point characterization (saddle_point_sufficient/saddle_point_necessary) is the standard route to designing an algorithm: a method that provably drives a pair $(x_k,\lambda_k)$ to a saddle point of $L$ is provably convergent to an optimal $x^*$, without ever needing to verify optimality directly against the primal problem.

None of the six substantive results here has a machine-checked proof on Prove2Me. The platform holds a genuinely weaker unconstrained-in-$K$ condition (OnlineConvexOpt.ConvexBasics. kkt_optimality, Hazan's Theorem 2.2: $\langle\nabla f(x^*), y-x^*\rangle \ge 0$ for $y \in K$, with no inequality/equality constraints or multipliers at all) and a structurally different, strictly more general cone-based Lagrange-duality development (VectorSpaceOpt.lagrange_duality and VectorSpaceOpt.lagrangian_saddle_sufficient_pointed, from Luenberger, which bundle all constraints into a single map into a convex cone in a general normed space, rather than Lan's explicit $\mathbb{R}^m$ inequality / $\mathbb{R}^p$ equality split). Formalizing this mission produces the finite-dimensional convex-program version of KKT in exactly the shape it is used and taught: separate multiplier vectors for inequality and equality constraints, an explicit normal cone rather than a cone-map abstraction, and both directions of the necessity/sufficiency split.

Difficulty

The separation theorem (Theorem 2.1) itself is routine once the projection onto a closed convex set is available. The real difficulty is entirely in the direction of the Convex Theorem on Alternative that Proposition 2.9 states: the naive idea — "insolvability of (I) should give a separating hyperplane between $\{x : f(x)<c\}$ and $\{x: g(x)\le 0\}$ directly" — fails, because these are sets in $\mathbb{R}^n$ and separating them there does not produce a sign-definite multiplier vector. Lan's proof instead lifts to $\mathbb{R}^{m+1}$ and separates the epigraph-like set $T = \{u : \exists x\in X,\ f(x)\le u_0, g(x)\le u_{1:m}\}$ from the open orthant-like set $S = \{u: u_0<c, u_{1:m}\le 0\}$; only in this lifted space does the separating normal's sign constraint (forced by $S$'s unboundedness in the positive directions) translate into $\lambda \ge 0$. Getting the sign of the $0$-th coordinate strictly positive — needed to normalize and divide — is itself a small separate argument using the Slater subsystem's solution. The KKT necessity direction (the goal) then chains three of these already-nontrivial results (separation → CTA → strong duality → saddle necessity) before translating the saddle-point condition on $L$ into the gradient/normal-cone form via differentiability of $f, g$ at $x^*$.

Formalization scope

All milestones are stated over EuclideanSpace ℝ (Fin n) with Convex/ConvexOn from Mathlib. Affine equality constraints $h_j$ are represented by explicit witnesses $w_j \in \mathbb{R}^n, b_j \in \mathbb{R}$ with $h_j(x) = \langle w_j, x\rangle + b_j$, so that $\nabla h_j = w_j$ is available without a separate affine-differentiability lemma. The normal cone $N_X^*(x)$ is Lan's own primal-space object (normalCone); the restricted Slater condition uses Mathlib's intrinsicInterior ℝ X for $\operatorname{rint} X$, distinct from the plain interior X used by the un-restricted Slater condition of Theorems 2.6/2.7(b). Primal optimal values and Lagrange dual values are stated via IsGLB/pointwise-inequality forms rather than raw sInf, so that no hypothesis is silently made true by an empty or unbounded set defaulting sInf to a junk value — in every milestone here the relevant set is guaranteed nonempty by the Slater-point hypothesis already present.

A trivializing formalization this mission rules out: stating kkt_necessary/kkt_sufficient with $X = \mathbb{R}^n$ (no set constraint) and empty $g, h$ (no functional constraints) would collapse the normal-cone condition to $\nabla f(x^*) = 0$ and make the whole KKT apparatus vacuous of any duality content; the milestones here keep $X$, $g$ and $h$ as genuine free parameters (the theorems are stated for arbitrary m, p : ℕ, including but not restricted to the degenerate case) so that the constrained content of Lan's theorem is what gets proved.

Reusable beyond this mission: normalCone and lagrangian are generic enough that any later chapter of this book needing Lagrangian duality or normal-cone stationarity (none of the current first-wave chapters 03/06 needs them directly) could import them once published rather than redeclaring. Contributions most welcome on the two hardest milestones, cta_solvable_of_insolvable and kkt_necessary, since they carry the mission's real difficulty; separation_point_closed can likely be discharged quickly via Mathlib's geometric_hahn_banach_point_closed.

Selected references

• G. Lan, First-Order and Stochastic Optimization Methods for Machine Learning, Springer Series in the Data Sciences, Springer 2020, Chapter 2. https://doi.org/10.1007/978-3-030-39568-1
• H. W. Kuhn and A. W. Tucker, "Nonlinear Programming," Proceedings of the Second Berkeley Symposium on Mathematical Statistics and Probability, 1951, pp. 481–492.
• W. Karush, "Minima of Functions of Several Variables with Inequalities as Side Constraints," M.Sc. thesis, University of Chicago, 1939.
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (standard modern reference for the separation theorem and Lagrangian duality used throughout).

Motivation

Every statistical guarantee for a learning algorithm ultimately rests on a concentration inequality: a bound on how far an empirical average can stray from its expectation. For real-valued averages, Bernstein's inequality (1924, refined through the 20th century) is the classical tool — sharper than Hoeffding's inequality whenever the summands' variance is small compared to their range. Modern learning theory, however, frequently needs to control averages of objects that are not real numbers but elements of a Hilbert space: feature vectors $\Phi(x_i)y_i$, gradients of a loss, or the values a kernel machine's empirical risk functional takes. Steinwart & Christmann, Support Vector Machines (Springer 2008, Information Science and Statistics), Chapter 6, develop exactly the vector-valued extension needed for the book's own SVM consistency proofs: Theorem 6.14, Bernstein's inequality for independent random variables taking values in a separable Hilbert space, and its corollaries.

Setting

Fix a probability space $(\Omega,\mathcal A,P)$ and a separable real Hilbert space $H$. Random variables $\xi_1,\dots,\xi_n : \Omega \to H$ are independent if the family is mutually independent (not merely pairwise), and $\xi_i$ has essential supremum bound $B$, $\|\xi_i\|_\infty \le B$, if $\|\xi_i(\omega)\|_H \le B$ for $P$-almost every $\omega$. Writing $\mathbb E$ for $\mathbb E_P$, the quantities of interest are the mean $\mathbb E\,\xi_i \in H$ (a Bochner integral) and the variance bound $\sigma^2$, an upper bound on $\mathbb E\,\|\xi_i\|_H^2$.

The classical scalar case (Theorem 6.12, itself a refinement of Hoeffding's inequality, Theorem 6.10) bounds $P\big(\frac1n\sum_i \xi_i \ge \varepsilon\big)$ for real-valued, mean-zero, range- and variance-bounded $\xi_i$. The tool behind both the scalar and the vector-valued case is a general exponential-moment inequality (Theorem 6.13) valid for independent, integrable random variables taking values in any separable Banach space $E$:

$$P\Big(\Big\|\sum_{i=1}^n \xi_i\Big\| \ge \varepsilon n\Big) \le \exp\Big(-t\varepsilon n + t\,\mathbb E\Big\|\sum_{i=1}^n \xi_i\Big\| + \sum_{i=1}^n \mathbb E\big(e^{t\|\xi_i\|}-1-t\|\xi_i\|\big)\Big), \qquad \varepsilon,t \ge 0.$$

Formalization targets

Goal: Theorem 6.14 (Bernstein's inequality in Hilbert spaces)

$$P\left(\Big\|\frac1n\sum_{i=1}^n \xi_i\Big\|_H \ge \sqrt{\frac{2\sigma^2\tau}{n}} + \sqrt{\frac{\sigma^2}{n}} + \frac{2B\tau}{3n}\right) \le e^{-\tau}, \qquad \tau>0,$$

for independent, mean-zero $\xi_1,\dots,\xi_n : \Omega \to H$ with $\|\xi_i\|_\infty \le B$ and $\mathbb E\|\xi_i\|_H^2 \le \sigma^2$. This is the weakest stable form of the claim: it is stated for a general separable Hilbert space (not a fixed finite dimension), with the tail written as a sum of three explicit terms rather than folded into an unspecified constant, so it survives specialization to any concrete $H$ without modification.

Supporting facts

Theorem 6.13 (above) is the direct tool Theorem 6.14's own proof invokes ("we will prove the assertion by applying Theorem 6.13"); Theorem 6.12 is the scalar analogue Theorem 6.14 generalizes, included to make the generalization's exact form (three terms, not two) checkable against its source; Corollary 6.15, Hoeffding's inequality in Hilbert spaces, is the immediate mean-free-of-a-variance-bound consequence of Theorem 6.14 obtained by centering, reused directly in the book's own oracle-inequality proof (§6.4).

Significance

Theorem 6.14 is the concentration inequality behind the book's later empirical-process arguments for SVMs: whenever an SVM's analysis needs to bound the deviation of an empirical average of Hilbert-space-valued quantities (feature-map evaluations, loss gradients) from its mean, this is the tool invoked, via Corollary 6.15 in the book's own oracle-inequality derivation. Its distinct contribution over simply applying the scalar Theorem 6.12 coordinate-by-coordinate (which is not available without a fixed, finite orthonormal basis, and even then would produce dimension- dependent bounds) is that the bound here is entirely dimension-free: it depends on $H$ only through the variance bound $\sigma^2$ and the range bound $B$, not through $\dim H$.

The scalar Bernstein inequality is classical (Bernstein 1924, refined by Bennett 1962 and others to the sharper multiplicative form used here); its Banach- and Hilbert-space generalizations (via the martingale-difference / Yurinskii-type argument Theorem 6.13's proof uses) are standard in the empirical-process-theory literature by the time of this book (see, e.g., Pinelis 1994 for closely related Banach-space martingale inequalities). No machine-checked Lean proof of the Hilbert-space form is known to exist on the platform at the time of writing (the platform's own HighDimProb.Concentration.bernstein_unweighted, from the Vershynin series, is a different, sub-exponential-norm scalar statement — see Formalization scope); this mission asks for the book's own bounded-summand, explicit-constant Hilbert-space form.

Difficulty

The natural first attempt generalizes the scalar proof's Markov-inequality argument directly: bound $\mathbb E\,e^{t\|\sum_i\xi_i\|}$ using independence. This breaks immediately because $\|\cdot\|_H$ is not linear, so $e^{t\|\sum_i \xi_i\|}$ does not factor over $i$ the way $e^{t\sum_i \xi_i}$ does in the scalar case — there is no vector-valued analogue of the moment generating function that tensorizes under independence directly. Theorem 6.13's proof resolves this with a martingale-difference decomposition (writing the deviation as a telescoping sum of conditional-expectation differences $X_k$ across the filtration generated by $\xi_1,\dots,\xi_k$) rather than a direct product-of-moment-generating-functions argument, at the cost of needing $E$ separable (for the conditional expectations and the resulting sums to be well-defined and measurable). Deriving Theorem 6.14 from Theorem 6.13 then requires controlling the two extra terms Theorem 6.13 introduces (the mean-norm term and the per-summand correction) using only the Hilbert-space-specific facts $\mathbb E\langle\xi_i,\xi_j\rangle=0$ for $i\ne j$ (from independence and mean-zero) and the scalar bound on $\mathbb E\|\xi_i\|^2$ — which is exactly where the tail's extra $\sqrt{\sigma^2/n}$ term originates, and is not obtainable by naively reusing the scalar Theorem 6.12's two-term optimization over $t$ unchanged.

Formalization scope

$H$ (and, for Theorem 6.13, $E$) is an arbitrary separable real (Hilbert, resp. Banach) space — not fixed to a Euclidean space of any dimension — matching the book's own generality, which is essential since the theorem's dimension-independence is part of its content. $\|\xi_i\|_\infty \le B$ is formalized as the almost-sure bound ∀ᵐ ω ∂P, ‖ξ i ω‖ ≤ B, matching the book's $L^\infty(P)$ convention rather than requiring the bound to hold for literally every $\omega$. Independence is the mutual independence of the whole family (Mathlib's iIndepFun), matching Theorem 6.13's proof, which uses independence of $\xi_k$ from $\sum_{i\ne k}\xi_i$ for every $k$ simultaneously, not merely pairwise independence.

A trivializing formalization would state the conclusion in terms of the scalar random variable $\|\xi_i\|_H$ rather than the vector-valued average's norm $\big\|\frac1n\sum_i \xi_i\big\|_H$ — this would collapse the theorem to an easier scalar statement about a nonnegative random variable and lose the whole point of the vector-valued generalization; it is ruled out here by writing the norm of the sum (not a sum of norms) inside the probability. Likewise, dropping the $\sqrt{\sigma^2/n}$ middle term of the tail bound (present here, absent from the scalar Theorem 6.12) would silently understate the genuine dimension-independent cost of vector-valued concentration; all three terms are kept.

Theorem 6.13's general Banach-space statement, and the scalar Theorem 6.12, are reusable beyond this mission (Theorem 6.13 is the tool any future Banach-space-valued concentration mission in this series would reach for first). The platform's existing HighDimProb.Concentration. bernstein_unweighted/hoeffding_rademacher (Vershynin series) are not reused as kind: reference items here: they use a sub-Gaussian/sub-exponential-Orlicz-norm parameterization and a universal (unspecified) constant, a genuinely different hypothesis structure from this chapter's explicit $L^\infty$-bounded, exact-constant form — reusing them would misrepresent this chapter's own, sharper statement. Completing the four sorrys (Theorems 6.12-6.14, Corollary 6.15) is welcome; the martingale-difference argument behind Theorem 6.13 is the natural starting point, since the other three all reduce to it directly.

Selected references

• I. Steinwart & A. Christmann, Support Vector Machines, Springer, Information Science and Statistics, 2008. https://doi.org/10.1007/978-0-387-77242-4 (Chapter 6, §6.2, pp. 210-217).
• S. Bernstein, "On a modification of Chebyshev's inequality and of the error formula of Laplace," Ann. Sci. Inst. Sav. Ukraine, Sect. Math. 1(4), 1924 (original scalar inequality).
• G. Bennett, "Probability inequalities for the sum of independent random variables," Journal of the American Statistical Association 57(297), 1962, pp. 33-45. https://doi.org/10.1080/01621459.1962.10482149
• I. Pinelis, "Optimum bounds for the distributions of martingales in Banach spaces," Annals of Probability 22(4), 1994, pp. 1679-1706. https://doi.org/10.1214/aop/1176988477

Motivation

Von Neumann's minimax theorem (Chapter VIII) settles two-player zero-sum games with scalar payoffs. In 1956, Blackwell asked the natural generalization: what can a player guarantee in a repeated game with vector-valued payoffs, where "winning" means driving the average payoff into a target set rather than above a target value? For decades the resulting theory — approachability — and the regret-minimization theory this book develops were believed to be different, with approachability seen as the stronger notion. Chapter 13 closes that gap: approachability and online convex optimization are shown to be algorithmically equivalent, each reducible to the other with no loss of efficiency, and along the way this equivalence yields a constructive, rate-quantified proof of Blackwell's own theorem.

Setting

A generalized vector game (Definition 13.2) is given by bounded convex closed decision sets $K_1,K_2$ and a vector payoff $u:K_1\times K_2\to\mathbb R^d$. A set $S$ is approachable (Definition 13.3) if some non-anticipating algorithm, playing in $K_1$ against any sequence $y_1,y_2,\dots\in K_2$, drives the average payoff's distance to $S$ to zero. Blackwell's theorem (13.4) characterizes exactly which $S$ are approachable via a purely geometric condition: every column-player strategy $y$ admits a row-player best response $x$ landing the payoff in $S$.

Section 13.2 constructs an explicit approachability algorithm from any OCO algorithm: given a best-response oracle realizing Blackwell's condition, Algorithm 37 runs the OCO algorithm on the proxy losses $f_t(w) = w^\top u_{t-1} - h_S(w)$ (the support function $h_S(w)=\max_{x\in S}\{w^\top x\}$ letting distance-to-$S$ be written, via Lemma 13.5's minimax duality, as a convex optimization problem over the unit ball), queries the oracle at the OCO algorithm's play $w_t$, and averages the resulting rewards.

Formalization targets

Theorem 13.7 (OCO-to-approachability rate, milestone)

$$\mathrm{Dist}(\bar u_T, S) \le \frac{\mathrm{Regret}_T(A)}{T}.$$

Theorem 13.4 — the mission's goal (sufficiency direction only)

$$\big(\forall y\in K_2,\ \exists x\in K_1,\ u(x,y)\in S\big) \implies S\ \text{is approachable}.$$

Significance

This chapter's headline claim — approachability and OCO are equivalent — is proved in two directions in the book (§13.2 and §13.3); this mission drafts the direction the book itself foregrounds as "the more interesting implication" and constructively proves: any sublinear-regret OCO algorithm converts directly into an explicit approachability algorithm with an explicit convergence rate, giving a self-contained, algorithmic proof of a 1956 game-theory theorem using 1990s–2000s online-learning machinery. Historically, this equivalence resolved a standing misconception (approachability believed strictly stronger) and reframes Blackwell's theorem as a special case of regret minimization rather than a separate theory requiring its own toolkit. No prior art was found on the platform for Blackwell approachability (planning search: q=Blackwell — the one hit, PRNGCompression.prng_no_free_lunch's cousin, an unrelated Rao-Blackwellization result, is not a substitute); this mission drafts both items fresh.

Difficulty

Theorem 13.4's statement is a clean geometric implication, but the book is explicit that its proof is entirely carried by Theorem 13.7 plus an unstated "explicit conclusion" left as an exercise (the passage from a finite-horizon rate bound to the asymptotic Dist → 0 claim, using any of the book's own sublinear-regret OCO algorithms as a witness). Theorem 13.7's own proof combines three nontrivial facts: Lemma 13.5's minimax-duality rewriting of $\mathrm{Dist}(\cdot, S)$ as a linear optimization over the unit ball (itself proved via Sion's minimax theorem, not excerpted here), the best-response oracle's defining inequality (13.2) applied pointwise at each round's $w_t$, and the OCO algorithm's own regret guarantee applied to the specific proxy-loss sequence $f_t$ built from the realized game trajectory — a genuine composition of three separate pieces of machinery from earlier in the book (Chapters III–VIII), not a routine substitution.

Formalization scope

IsApproachable is declared as its own definition (per BRIEF.md's explicit instruction, since Theorem 13.4 depends on it), with the non-anticipation clause made explicit (matching the series' IsOnlineAlgorithm convention from Chunk 03) even though the book's own Definition 13.3 states it only informally ("x_t ← A(y_1,\dots,y_{t-1})"). SupportFunction is h_S exactly as displayed, as a real supremum (a genuine maximum given the chapter's standing "closed, bounded" hypothesis on S). $\mathrm{Dist}(\cdot,S)$ throughout is Euclidean distance, rendered as Mathlib's Metric.infDist — confirmed the chapter uses no other distance notion (checked §13.1-13.3 directly, per the pitfall BRIEF.md flags). Theorem 13.7 transcribes Algorithm 37's $f_t(w)=w^\top u_{t-1}-h_S(w)$ construction faithfully, including its one-round offset (using the previous round's realized reward to build the current round's proxy loss, while the conclusion averages the current round's rewards) — exactly as the book's own pseudocode has it, not smoothed over.

Scope decision on Theorem 13.4's biconditional. The book states Theorem 13.4 as an ↔ but proves, and explicitly flags as proved, only the sufficiency direction (←): "The necessity of this condition is left as an exercise... Our reductions henceforth give an explicit proof of Blackwell's theorem [meaning: of the sufficiency direction]." Per CAPTAIN_BRIEF.md rule 6 and BRIEF.md's explicit instruction, this mission drafts only that direction, named as such in the goal item's own docstring; see STATUS.md.

Not formalized (out of scope for this mission, given the remaining budget and the explicit "exercise" status of several results on these pages): the necessity direction of Theorem 13.4; Lemma 13.5 (minimax duality for Dist, itself relying on Sion's theorem, not separately formalized here); Lemma 13.6 (the equivalent best-response-oracle condition); §13.3's entire approachability-to-OCO direction (Theorem 13.9, Lemma 13.8, the cone/polar-cone machinery of §13.3.1) and §13.3.3 (existence of a best-response oracle for the constructed set); the "explicit conclusion" of Blackwell's theorem from Theorem 13.7, left as an exercise by the book itself.

Selected references

• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., arXiv:1909.05207v3, Chapter 13.
• D. Blackwell, "An analog of the minimax theorem for vector payoffs," Pacific Journal of Mathematics 6(1), 1956, 1-8.
• N. Abernethy, P. Bartlett, E. Hazan, "Blackwell approachability and no-regret learning are equivalent," COLT 2011.