Machine Learning

Motivation

Best subset selection fits a linear model using at most $k$ of $p$ available predictors: it minimizes the residual sum of squares $\|y-X\beta\|^2$ over all $\beta$ with at most $k$ nonzero coordinates. It is the classical benchmark for sparse regression, and mixed-integer optimization has made it computable at scales that used to be out of reach (Bertsimas, King & Mazumder, 2016). When the signal-to-noise ratio is low, however, best subsets overfits, and Mazumder, Radchenko & Dedieu propose to add a shrinkage penalty $\lambda\|\beta\|_q$ ($q\in\{1,2\}$) to it. Their oracle inequalities for the penalized estimators hold for a fixed model size $k$, and the practitioner still has to choose $k$.

§3.5 of the paper removes that choice. It replaces the cardinality constraint with BIC-type penalties that depend on the candidate model size, and Theorem 5 shows that the resulting estimators satisfy oracle inequalities for the expected prediction error over all of $\mathbb R^p$, with no condition on the design beyond the normalization of its columns. This mission formalizes Theorem 5 and the steps of its printed proof.

Setting

We observe $y=f^*+\epsilon\in\mathbb R^n$. The mean $f^*\in\mathbb R^n$ is deterministic and unknown, and $\epsilon$ has independent $N(0,\sigma^2)$ entries with $\sigma>0$. The design $X\in\mathbb R^{n\times p}$ is deterministic, with $p\ge1$ and columns of unit Euclidean norm. The prediction error of an estimate $\hat\beta$ is $\|f^*-X\hat\beta\|^2$. For $\beta\in\mathbb R^p$, $\|\beta\|$ is the Euclidean norm, $\|\beta\|_1=\sum_j|\beta_j|$, and $\|\beta\|_0$ is the number of nonzero coordinates.

For nonnegative tuning parameters $a$ and $b$, the data-dependent penalties are

$$\lambda_\beta=a\sqrt{\|\beta\|_0\log(ep/\|\beta\|_0)},\qquad \mu_\beta=b\log(ep/\|\beta\|_0),$$

with the convention $0\cdot\infty=0$, so the empty model is not penalized. The BIC-type estimators are

$$\hat\beta^B_2\in\arg\min_{\beta}\ \|y-X\beta\|^2+\lambda_\beta\|\beta\|+\mu_\beta\|\beta\|_0,\qquad \hat\beta^B_1\in\arg\min_{\beta}\ \|y-X\beta\|^2+\lambda\|\beta\|_1+\mu_\beta\|\beta\|_0,$$

where $\lambda\ge0$ is a fixed number. Both are unconstrained problems. Solving them is equivalent to solving the constrained problems with $\|\beta\|_0\le k$ for each $k$ and then choosing $k$ by the penalty. A minimizer exists but need not be unique.

The proof works on events of the noise vector. For an integer $s$ and $\delta_0\in(0,1]$ the event $G'_s$ requires

$$\epsilon^\top Xu\le\sigma\sqrt{5s\log(ep/s)+3\log(1/\delta_0)}\,\|Xu\|\qquad\text{for every }u\text{ with }\|u\|_0\le s .$$

Formalization targets

Goal: Theorem 5 (p. 21)

There exist universal constants $a_0,b_0,c_0$ such that, if $a\ge a_0\sigma$ or $b\ge b_0\sigma^2$,

$$\mathbb E\|f^*-X\hat\beta^B_2\|^2\lesssim\inf_{\beta\in\mathbb R^p}\Big[\|f^*-X\beta\|^2+\lambda_\beta\|\beta\|+\mu_\beta\|\beta\|_0\Big]+\sigma^2,$$

and, if $\lambda\ge c_0\sigma\sqrt{\log(ep)}$ or $b\ge b_0\sigma^2$,

$$\mathbb E\|f^*-X\hat\beta^B_1\|^2\lesssim\inf_{\beta\in\mathbb R^p}\Big[\|f^*-X\beta\|^2+\lambda\|\beta\|_1+\mu_\beta\|\beta\|_0\Big]+\sigma^2 .$$

Here $\lesssim$ hides one universal multiplicative constant. The constants are not specified, so the goal records the shape of the bound and is not invalidated by later improvements of the constants.

Milestones (proof of Theorem 5, B.13, and B.5)

1. (51): the deterministic basic inequality for $\hat\beta^B_2$.
2. (54): for $a\gtrsim\sigma$, with probability at least $1-\delta_0/2$, $\|f^*-X\hat\beta\|^2+\mu_{\hat\beta}\|\hat\beta\|_0\lesssim\|f^*-X\beta\|^2+\lambda_\beta\|\beta\|+\sigma^2\log(1/\delta_0)+\mu_\beta\|\beta\|_0$.
3. The union bound over model sizes: with $G=\bigcap_{s=1}^pG'_s$, where $G'_s$ is taken at $\delta_0=(s/[ep])^s\epsilon_0$, we have $P(G^c)\le\epsilon_0$.
4. (55): for $b\gtrsim\sigma^2$, the analogue of (54) with probability at least $1-\epsilon_0$.
5. (56): under either condition, the high-probability oracle inequality with $\inf_\beta$ and $\sigma^2\log(1/\delta_0)$.
6. The tail-to-expectation step of B.5: if $W\le\kappa\log(1/\delta_0)$ with probability at least $1-\delta_0/2$, then $\mathbb EW^+\le\kappa/2$.
7. (58): the high-probability counterpart of (56) for $\hat\beta^B_1$.

Significance

The result. Theorems 2 and 3 of the paper give oracle inequalities only over the sparsity class $\{\|\beta\|_0\le k\}$ for a $k$ fixed in advance. Theorem 5 makes the model size data-driven. Its bounds hold over all of $\mathbb R^p$ and need no restricted-eigenvalue or sparse-eigenvalue condition on $X$. Corollary 6 of the paper deduces from it that the estimators attain the error rates of Corollaries 3 and 4 while selecting models of the same order as the true model size. The paper also notes that the slow-rate bound for $\hat\beta^B_1$ with $b=0$ is a bound for the Lasso.

Formalizing it. Theorem 5 is a published result with a printed proof (Supplement B.13). The proof is written up to unspecified universal constants, and it defers two steps to other parts of the paper ("repeating the argument after inequality (32)" and "repeating the argument in the proof of Corollary 3"). A formal proof makes every constant and every deferred step explicit. No part of the paper has been machine-checked, to the best of our search.

Difficulty

The argument is long rather than deep. The obvious first attempt fixes the selected model size $\hat k=\|\hat\beta\|_0$ and applies a high-probability bound for that size. This fails because $\hat k$ is random and depends on $\epsilon$, so a bound for each fixed $s$ says nothing about the random $\hat k$. The noise term must be controlled simultaneously over all model sizes, at a total failure probability that does not grow with $p$. The second obstacle is the passage from high-probability bounds, which hold for every $\delta_0$ and grow like $\log(1/\delta_0)$, to a bound in expectation. That passage needs the high-probability statement with a constant that is uniform in $\delta_0$.

Formalization scope

• Representation. Vectors are Fin n → ℝ and Fin p → ℝ, and the design is a Matrix (Fin n) (Fin p) ℝ.

  • The norms $\|\cdot\|$, $\|\cdot\|_1$ and $\|\cdot\|_0$ are explicit definitions (l2, l1, l0), because Mathlib's norm on Fin m → ℝ is the sup norm.
  • The noise law is the product of $n$ centred Gaussians with variance $\sigma^2$ (noiseLaw).
  • Logarithms are natural, and $e=\exp(1)$.

• Model. The standing hypotheses are:

  • unit-norm columns of $X$;
  • $\sigma>0$ and $p\ge1$;
  • $a,b\ge0$, and $\lambda\ge0$ for $\hat\beta^B_1$.

  The quantities $X$, $f^*$, $\sigma$, $a$, $b$, $\lambda$ and the penalties are inputs. The randomness is the law of $\epsilon$ alone, and $y=f^*+\epsilon$.

• Estimators are argmin predicates IsBIC2, IsBIC1: "$\hat\beta$ minimizes the objective over all of $\mathbb R^p$". Every statement holds for every minimizer.

  • In Theorem 5 an estimator is a measurable map $y\mapsto\hat\beta(y)$ that is a minimizer for every $y$, and the bound is claimed for every such selection.
  • The expectation is a lower Lebesgue integral in $[0,\infty]$, so a non-integrable error cannot make the bound vacuous.

• Constants.

  • "$\lesssim$" is one universal constant $C>0$, quantified before every other parameter.
  • "$\inf_\beta[\dots]$" is written as "for every $\beta$".
  • "With probability at least $1-\delta$" is the existence of a measurable event of probability at least $1-\delta$ on which the inequality holds.
  • The constants $a_0$, $b_0$ and $c_0$ carry no sign, as on the page.

• Correction. Theorem 1 of the paper states $P(G_s)\ge1-\delta_0$ for an event with coefficient $1$ on $\log(1/\delta_0)$. That bound is false for small $\delta_0$ (already for $n=p=s=1$). The union bound here uses the corrected event $G'_s$ with coefficient $3$, which inside $\lesssim$ changes nothing downstream.

• Ruled out. None of the following counts as a formalization of the goal:

  • an arbitrary or non-measurable selection of the minimizer;
  • a Bochner integral, which is $0$ for a non-integrable error;
  • a constant that depends on $n$, $p$, $\delta_0$ or the design;
  • a fixed $\delta_0$ or $\epsilon_0$.

• Not formalized here. The fixed-$k$ oracle inequalities (Theorems 2 and 3), the noise events of Theorem 1, the lower bound (Theorem 4), Corollaries 1–6 and the numerical study are not part of this mission. Some of them are the subjects of the other missions of this series. The proof of Theorem 5 needs the probability bounds for the events $F$ and $G'_s$ of Theorem 1 and the deterministic arguments of Theorems 2 and 3. A solver may prove them here or import them once they are published.

• Contributions welcome.

  • Gaussian chi-square tail bounds (Laurent–Massart);
  • the bound for the sorted-$\ell_1$ event $F$ (Bellec, Lecué & Tsybakov);
  • the existence of measurable selections of the argmin;
  • the layer-cake step.

  These are reusable well beyond this paper.

Selected references

• R. Mazumder, P. Radchenko, A. Dedieu, Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low, arXiv:1708.03288v4, 2022; Operations Research, 2023. https://arxiv.org/abs/1708.03288
• D. Bertsimas, A. King, R. Mazumder, Best subset selection via a modern optimization lens, Annals of Statistics 44(2), 2016. https://doi.org/10.1214/15-AOS1388
• P. C. Bellec, G. Lecué, A. B. Tsybakov, Slope meets Lasso: improved oracle bounds and optimality, Annals of Statistics 46(6B), 2018. https://doi.org/10.1214/17-AOS1670
• B. Laurent, P. Massart, Adaptive estimation of a quadratic functional by model selection, Annals of Statistics 28(5), 2000. https://doi.org/10.1214/aos/1015957395
• L. Birgé, P. Massart, Gaussian model selection, Journal of the European Mathematical Society 3, 2001. https://doi.org/10.1007/s100970100031

Motivation

An online classifier must predict a label before learning the correct answer. Its errors matter directly: a low numerical loss is useful only if it controls the number of wrong predictions. Chapter 8 of Orabona's textbook examines this connection for linear classification, where a vector of weights produces a score by taking an inner product with the incoming example. The Perceptron is a particularly spare example: it changes its weights only after a mistake, and it needs no learning rate or chosen comparator. This makes its guarantee a useful point of contact between classification mistakes and the convex losses used elsewhere in online optimization.

Theorem 8.2 compares the Perceptron's mistake count with a whole family of comparator losses, indexed by a real exponent $q\ge1$. The theorem is a known result in the book, not an unsolved conjecture. The mission concerns a faithful Lean statement and, subsequently, its machine-checked proof. The distinction matters because other Perceptron bounds on the platform address batch separability, multiclass prediction, or a hinge loss only on update rounds; those results do not state this theorem with its constants and quantifiers.

Setting

Fix a dimension $d$ and a sequence of feature vectors $z_t\in\mathbb R^d$ with binary labels $y_t\in\{-1,1\}$, for rounds $t=1,\ldots,T$. The Perceptron begins at $x_1=0$. At round $t$ it predicts $\widetilde y_t=\operatorname{sign}(\langle z_t,x_t\rangle)$, where $\operatorname{sign}(0)=0$. It records a mistake when $y_t\widetilde y_t\le0$ and, on exactly those rounds, adds $y_tz_t$ to its weights. Write $\tau_t=\mathbf 1\{y_t\widetilde y_t\le0\}$ and $M=\sum_{t=1}^T\tau_t$. A zero score is a mistake even though it is not a strict sign disagreement.

For a score $m\in\mathbb R$, a label $y\in\{-1,1\}$, and a real power $q\ge1$, the hinge-power loss is $\ell_q(m,y)=\max(1-ym,0)^q$. A fixed competitor $u\in\mathbb R^d$ has cumulative loss $L_q(u)=\sum_{t=1}^T\ell_q(\langle z_t,u\rangle,y_t)$. The loss is zero when $u$ gives every example the correct sign with margin at least one. The book assumes the input vectors obey $\|z_t\|_2\le R$; $R$ is a nonnegative radius. The sequence is arbitrary, so the result includes examples chosen with knowledge of earlier predictions.

Formalization targets

Perceptron mistake guarantee

The goal is Theorem 8.2, p. 144 of Orabona. For every $u\in\mathbb R^d$ and every real $q\ge1$,

$$M-L_q(u)\le\frac{q^2R^2\|u\|_2^2}{2} +qR\|u\|_2\sqrt{\frac{q^2R^2\|u\|_2^2}{4}+L_q(u)}.$$

All constants and the full family of powers are part of the target. For a competitor with $L_q(u)=0$, choosing $q=1$ yields the finite mistake bound $M\le R^2\|u\|_2^2$, as the book explains on p. 144. For a nonseparable sequence, the same statement measures mistakes relative to the competitor's nonzero loss.

Milestone statements

The milestone list follows the book's named ingredients: Lemma 4.29 converts an implicit square-root inequality into an explicit one; the constant-step clause of Theorem 2.13 gives the linear-loss gradient bound; and displays (8.4) and (8.5) relate the Perceptron updates to the comparator and to the hinge loss. Theorem 2.13 is stated in the linear, whole-space case used on p. 145. The printed (8.4) has an invalid extra term on its left; the milestone retains the printed text for provenance, while the Lean statement gives the valid comparator inequality used by (8.5). The correction is described in the item and moderation notes.

Significance

The guarantee answers a practical question about a simple online rule: how many classification errors can it make when a fixed linear predictor has small convex loss? The answer has explicit dependence on the feature radius, comparator norm, loss exponent, and comparator loss. It contains the separable margin case and also applies when no comparator classifies every example with margin one. The quantifier over all $u$ permits a later analyst to choose a competitor after seeing the sequence without changing the algorithm or the theorem.

A complete formalization would provide a reusable account of a deterministic online classifier, its exact zero-score convention, and the passage from update counts to a family of hinge losses. The local Lean declarations currently compile as statements with proof placeholders; compilation does not establish the mathematical inequalities. A proof of the goal and milestones remains to be supplied and checked. In particular, the correction to (8.4) should be made explicit in any downstream development so that later results never depend on the false printed left side.

Difficulty

The mistake count is discontinuous in the prediction score, while the competitor is measured by a smooth family of convex surrogates. A direct comparison of their per-round losses does not give the theorem's constants. The update rule also depends on its own current score, so its condition must be tied to the weight sequence generated by earlier rounds. Treating the update indicators as free variables, or counting only rounds with a strictly negative score, changes the statement.

The book's proof passes through an implicit inequality involving $\sqrt M$. That relation alone is weaker than the displayed goal until its constants and nonnegative domains are handled precisely. Real powers require special attention at a zero hinge value. The printed (8.4) introduces an additional difficulty: with $u=0$ and two one-dimensional examples $z_1=1$, $z_2=-1$ carrying positive labels, its left side is positive while its right side is zero. The valid comparator inequality has to be distinguished from that printed display.

Formalization scope

Lean uses EuclideanSpace ℝ (Fin d) for $\mathbb R^d$, its Euclidean inner product and norm, and sequences indexed by natural numbers with active rounds $1,\ldots,T$. Index zero carries no data requirement. A total recursive definition fixes $x_1=0$ and every later Perceptron update. Mathlib's Real.sign supplies $\operatorname{sign}(0)=0$; an indicator records both a wrong sign and a zero score. The comparator loss uses a maximum with zero before taking a real power. No probability space is needed because Algorithm 8.2 is deterministic.

The Lean theorems explicitly require binary labels on the active rounds, $q\ge1$ for the goal, $R\ge0$, and $\|z_t\|_2\le R$. They allow $T=0$, $d=0$, and $R=0$; the formulas remain meaningful in these cases. The set $X$ in the book's theorem is omitted because the assertion uses only the given feature sequence and its norm bound. The constant-step milestone requires $\eta>0$ because its formula divides by $\eta$. The definitions include a mistake count, hinge-power loss, cumulative comparator loss, and the fixed algorithm; the theorem layer can reuse Mathlib's inner-product and real-analysis results. Contributions toward these statements, the algebraic milestone, or the full theorem proof are in scope. A run that can skip a zero-score update or whose iterates are chosen independently of the recursion is outside this mission.

Selected references

• Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026, Chapter 8, pp. 141–146; Lemma 4.29, p. 45; Theorem 2.13, p. 13. arXiv PDF.

Motivation

In online convex optimization, a learner selects a point before seeing the current loss. A useful guarantee compares the learner's accumulated loss with that of a single fixed point chosen in hindsight. A step size chosen from a preannounced bound on all future gradients can be wasteful when the realized gradients are small. Chapter 4 of Orabona's online learning text studies step sizes determined from the gradients observed so far. Its adaptive online subgradient descent bound uses the actual sum of squared subgradient norms, without requiring that sum in advance (Theorem 4.14, p. 40).

The chapter then asks for a more informative guarantee when the losses have small values at a good competitor. For self-bounded losses, a small loss at a point limits the size of its subgradients. Theorem 4.30 on p. 45 turns that relation into a bound in terms of the competitor's cumulative loss. This is useful for problems such as the squared hinge loss discussed immediately after the theorem: if one feasible comparator has zero loss on every round, the regret bound becomes independent of the number of rounds. These are known textbook results. The goal here is a machine-checked formulation and, eventually, a proof of the stated constants.

Setting

Fix a finite horizon $T\ge1$ and a nonempty, closed, convex decision set $V\subseteq\mathbb R^d$. Its Euclidean diameter is at most $D$: every $a,b\in V$ satisfy $\|a-b\|_2\le D$. In round $t\in\{1,\ldots,T\}$, the learner plays $x_t\in V$ and receives a convex loss $\ell_t$. The loss sequence is arbitrary. A subgradient $g_t$ of $\ell_t$ at $x_t$ satisfies $\ell_t(y)\ge\ell_t(x_t)+\langle g_t,y-x_t\rangle$ for every $y\in\mathbb R^d$. The regret against a fixed competitor $u\in V$ is

$$\operatorname{Regret}_T(u)=\sum_{t=1}^{T}\bigl(\ell_t(x_t)-\ell_t(u)\bigr).$$

The learner uses projected online subgradient descent. After observing $g_t$, it sets

$$\eta_t=\frac{\sqrt2D}{2\sqrt{\sum_{i=1}^{t}\|g_i\|_2^2}}, \qquad x_{t+1}=\Pi_V(x_t-\eta_tg_t)$$

when $g_t\ne0$. If $g_t=0$, the algorithm leaves $x_{t+1}=x_t$. Here $\Pi_V$ is a Euclidean nearest point in $V$. The current gradient appears in the sum defining $\eta_t$ because the update is made after that gradient is observed. The initial point $x_1$ is any member of $V$, and every admissible choice of subgradient is allowed.

A loss $f$ is $s$-self-bounded on $V$ when it is bounded below, has a subgradient at each point of $V$, and every subgradient $g$ at every $x\in V$ satisfies

$$\|g\|_2^2\le 2s\left(f(x)-\inf_{y\in\mathbb R^d}f(y)\right).$$

The infimum is over the whole ambient space. The target theorem additionally assumes that each loss is nonnegative everywhere. The $s$ in these formulas is nonnegative. These conventions follow Definition 4.26 and Theorem 4.30 of the pinned preprint.

Formalization targets

Adaptive gradient bound

The first milestone is Theorem 4.14. Under the setting above, for every $u\in V$,

$$\operatorname{Regret}_T(u)\le D\sqrt{2\sum_{t=1}^{T}\|g_t\|_2^2}.$$

This bound depends on the gradient sequence encountered by the algorithm. The printed theorem also equates this expression with a minimum over constant positive step sizes. At zero accumulated gradient energy that minimum is an unattained infimum, so the formal milestone states the regret inequality in every case and the identity with the minimum only when the accumulated squared gradient norm is positive.

Self-bounded loss bound

The goal is Theorem 4.30. If every loss is nonnegative, convex, and $s$-self-bounded on $V$, then for every fixed $u\in V$,

$$\operatorname{Regret}_T(u) \le 4sD^2+2D\sqrt{s\sum_{t=1}^{T}\ell_t(u)}.$$

The target includes the intermediate displayed bound on p. 45 and Lemma 4.29 as milestones. Their statements capture the passage from a regret bound involving the learner's cumulative loss to one involving the competitor's cumulative loss. The constants $4$ and $2$ are those printed in the theorem; the goal does not replace them with asymptotic notation.

Significance

Theorem 4.14 provides a guarantee without supplying a gradient bound or the horizon-dependent sum of squared gradients to the learner. Theorem 4.30 sharpens the interpretation when the losses are self-bounded: for a comparator with $\sum_t\ell_t(u)=0$, the regret is at most $4sD^2$. For larger comparator losses, the bound changes continuously with their accumulated value. The guarantee holds against each competitor, not merely one selected by an infimum over $V$.

A formal development would make the algorithm's timing, its zero-gradient branch, the ambient-space infimum, and the exact numerical constants explicit. These details are reusable in later analyses of adaptive step sizes and small-loss bounds. The proposal contains open Lean theorem statements and a compiled definitions file; it does not claim that these results already have machine-checked proofs in this mission. The metric projection relation is reused from an existing published definition, and the intended work is proving the open statements and developing their supporting inequalities.

Difficulty

A fixed step size can be selected after looking at all gradients, but that selection does not define an online update. The adaptive step size must use only gradients observed through the current round. The zero-gradient case needs an explicit update rule because its displayed quotient has a zero denominator on an all-zero prefix. These issues already appear in the first milestone.

For the goal, the self-bounded inequality controls subgradient norms using loss at the learner's own points. Substituting that control into the gradient bound yields a right-hand side containing $\sum_t\ell_t(x_t)$, although the desired statement is expressed using $\sum_t\ell_t(u)$. The intermediate estimate on p. 45 is therefore implicit. The square-root inequality of Lemma 4.29 supplies the separate arithmetic statement needed to express the final result with the printed constants. A direct substitution that treats the learner's loss as the competitor's loss would not justify the theorem.

Formalization scope

The Lean carrier is EuclideanSpace ℝ (Fin d), including dimension zero; the theorem remains valid there. Rounds are indexed from one, with index zero unused, and sums range over Finset.Icc 1 T. The loss functions are real-valued on the whole Euclidean space. The book permits extended-real losses that take $+\infty$ outside their domain; this formalization addresses the real-valued case. Full-space subgradients retain the source's definition. Convexity and nonnegativity hold on the whole Euclidean space, and self-boundedness holds at every feasible point, for each round through $T$.

The adaptive run is a relation covering every legal selection of subgradients and projections. It requires the update after every nonzero gradient and the unchanged point after a zero gradient. The closed, convex, nonempty set assumptions ensure that Euclidean projection is meaningful. The diameter condition is written as $\|a-b\|_2\le D$ for all feasible $a,b$, so it also covers any valid upper bound on the diameter. Self-boundedness uses the real infimum of the full range of each loss, together with boundedness below; global nonnegativity in the goal guarantees that condition. The explicit $T\ge1$ and $s\ge0$ conditions prevent boundary values from silently changing the meaning of a quotient or a square root.

The goal must hold for every comparator $u\in V$ and every admissible run. A definition that checks self-boundedness only at $u$, or permits arbitrary next decisions, would lose the algorithmic guarantee. The reusable components are the regret and gradient-energy definitions, the adaptive run relation, the self-boundedness predicate, and the scalar inequality in Lemma 4.29. Contributions that establish the projection analysis and the three listed milestones directly support the goal.

Selected references

• Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026, Chapter 4, pp. 34–49. arXiv

Why online gradient descent matters

In online learning, a decision is made before the loss for that round is revealed. The learner cannot optimize a known objective once and use its minimizer forever: the sequence of objectives may be arbitrary. A basic performance measure is regret, the learner's total loss minus the loss of one fixed decision chosen with hindsight. A regret bound that grows more slowly than the number of rounds shows that the learner's average excess loss vanishes. Orabona's introduction develops this measure and derives a bound for projected online gradient descent without requiring advance knowledge of the loss sequence (Orabona, Chapter 1 and Theorem 2.13).

The result is useful because it separates the geometry of the feasible set from the size of the gradients seen during play. It also supports step sizes that change with time, which matters when a learner adjusts its updates as more rounds pass. The exact endpoint term in the theorem records information that would be discarded by a coarser regret estimate (Orabona, Theorem 2.13 and the discussion on p. 14).

Decisions, losses, and projection

Let $V$ be a nonempty closed convex set in a real inner-product space. At round $t=1,\ldots,T$, the learner chooses $x_t\in V$, receives a differentiable convex loss function $\ell_t$, and incurs $\ell_t(x_t)$. For a fixed competitor $u\in V$, the book's regret is

$$\operatorname{Regret}_T(u)=\sum_{t=1}^{T}\bigl(\ell_t(x_t)-\ell_t(u)\bigr).$$

The competitor stays fixed through all $T$ rounds; it is not the best separate decision for each round. The losses may differ on every round, and their sequence is arbitrary (Orabona, p. 2).

A metric projection $\Pi_V(z)$ is a point of $V$ nearest to $z$ in Euclidean distance. Convexity makes the projection single valued when $V$ is nonempty and closed. Projected online gradient descent, Algorithm 2.1, starts from an arbitrary $x_1\in V$, chooses positive step sizes $\eta_t$, forms $g_t=\nabla\ell_t(x_t)$, and sets

$$x_{t+1}=\Pi_V(x_t-\eta_t g_t).$$

The projection keeps the next decision feasible even when the unconstrained gradient step leaves $V$ (Orabona, Algorithm 2.1, p. 12). The first-order optimality condition of Theorem 2.8, the projection inequality of Proposition 2.11, and the one-round inequality of Lemma 2.12 are the numbered milestones leading to the main statement. Lemma 2.31 records the parallel one-round statement for subgradients (Orabona, pp. 11–13, 19).

Formalization targets

For $V$ of finite diameter $D=\sup_{x,y\in V}\|x-y\|_2$, positive nonincreasing step sizes, and any $u\in V$, the main target is the complete first inequality of Theorem 2.13:

$$\operatorname{Regret}_T(u)\le \frac{D^2}{2\eta_T} +\sum_{t=1}^{T}\frac{\eta_t}{2}\|g_t\|_2^2 -\frac{\|x_{T+1}-u\|_2^2}{2\eta_T}.$$

The negative terminal term is part of the target. The constant-step clause of the same theorem is a separate companion item. If $\eta_t=\eta>0$ on every round, it states

$$\operatorname{Regret}_T(u)\le \frac{\|u-x_1\|_2^2}{2\eta} +\frac{\eta}{2}\sum_{t=1}^{T}\|g_t\|_2^2 -\frac{\|x_{T+1}-u\|_2^2}{2\eta}.$$

This clause has no finite-diameter hypothesis, so it applies on unbounded feasible sets as well (Orabona, Theorem 2.13, p. 13).

What the bound supplies

The theorem gives a deterministic guarantee against every fixed feasible competitor, for every loss sequence and every valid run of the algorithm. It exposes the cumulative effect of the gradient magnitudes and the step sizes. Its constant-step form uses the distance from the initial decision to the comparator rather than the diameter of the whole set. The bound is therefore informative on some unbounded sets where the diameter term has no finite value (Orabona, Theorem 2.13 and p. 14).

This is a known textbook theorem, not an open conjecture. The mission asks for machine-checked proofs of the source statements in a reusable Lean interface: a fixed-comparator regret definition, a finite-horizon run predicate, and the projection and one-step results. The published metric-projection predicate is reused, while the one-based regret and run definitions are specific to this book's convention.

Where the argument is delicate

An immediate attempt to sum the one-round estimate leaves squared-distance terms with different coefficients when the step size varies. They do not cancel as they would with a fixed coefficient. The theorem's monotonicity condition on the step sizes and the finite diameter of $V$ are what make a uniform bound possible; omitting either changes the first displayed claim. Keeping the final negative squared-distance term also requires more care than proving only the weaker bound obtained by dropping it. On the nonsmooth side, an arbitrary vector cannot replace a subgradient: its defining inequality supplies the link between a loss difference and the linearized direction (Orabona, Lemmas 2.12 and 2.31, Theorem 2.13).

Formalization scope

Lean uses a complete real inner-product space, covering the book's $\mathbb R^d$ and using only the geometry needed by this chapter. Time remains one based: round zero is unused, sums run from $1$ through $T$, and the output after the last round is $x_{T+1}$. The horizon satisfies $T\ge1$, so the last step size and the terminal iterate are part of an actual run. The run predicate requires a gradient and a metric projection at every round through $T$; it does not select a favorable projection after seeing the comparator. The theorem requires each loss to be convex and differentiable on an open neighborhood containing $V$, as in Algorithm 2.1.

The diameter in the main target is Mathlib's real Metric.diam V, with boundedness imposed so that it is the finite supremum in the book. The constant-step clause has no boundedness requirement. The projection relation is the published OnlineConvexOpt.FirstOrder.IsMetricProjection: it includes membership in $V$ and minimal distance to the point being projected. Thus, the update cannot be satisfied by an arbitrary point of $V$. Every regret claim quantifies over a comparator $u\in V$; extending the quantifier outside $V$ would assert a different result.

For Lemma 2.31, losses are real valued on $V$, and the stated subgradient inequality is relative to $V$. The book defines a full-space subgradient for an extended-real-valued function; every such subgradient gives the relative inequality used here. This is the precise convention for that milestone and is disclosed in its item description. Contributions that establish the projection inequality, the single-round inequalities, and either complete form of Theorem 2.13 fit the mission. The regret and run definitions can be reused in later deterministic online optimization results, while the projection predicate is already shared with another textbook development.

Selected references

• Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv preprint arXiv:1912.13213v10, 2026. Pinned preprint

Motivation

When the players of a game repeatedly adjust their strategies with no-regret learning algorithms, the empirical distribution of play converges to a coarse correlated equilibrium, and in smooth games the average social welfare approaches the price-of-anarchy guarantee of the game (Roughgarden 2009). For generic no-regret algorithms such as Hedge the convergence rate is $O(1/\sqrt T)$, because each player's regret after $T$ rounds is of order $\sqrt T$ in the worst case, against an adversary.

Other players are not adversaries: they are also learning, and their strategies change slowly. Syrgkanis, Agarwal, Luo and Schapire (NIPS 2015, arXiv:1507.00407v5) identify a property of learning algorithms, regret bounded by variation in utilities (RVU), under which this predictability can be exploited in general multi-player games, and show that a natural class of algorithms has it. This mission formalizes their first main consequence: if every player uses optimistic follow the regularized leader (OFTRL), the sum of all players' regrets stays bounded by a constant independent of $T$, so the average welfare converges at rate $O(1/T)$.

Timeline. Rakhlin and Sridharan (COLT 2013; NIPS 2013) introduced optimistic mirror descent and showed $O(\log T / T)$ convergence to the minimax value in two-player zero-sum games when both players use it. Syrgkanis et al. (2015) extend the fast-rate phenomenon to general $n$-player games and arbitrary no-regret algorithms with the RVU property (Theorem 4), and establish RVU for OFTRL (Proposition 7), giving Corollary 8.

Setting

A game has $n$ players. Each player $i$ has a finite strategy set $S_i$ with $|S_i| = d$, and a utility $u_i(s) \in [0,1]$ for each pure profile $s = (s_1, \dots, s_n)$. A mixed strategy is a point $w_i$ of the probability simplex $\Delta = \Delta(S_i) \subset \mathbb R^d$, and a mixed profile $w = (w_1, \dots, w_n)$ induces the product distribution on pure profiles.

The game is played for $T$ rounds. At round $t$ each player picks $w_i^t \in \Delta$ and then observes the utility vector $u_i^t \in \mathbb R^d$ with entries

$$u^t_{i,x} = \mathbb E_{s_{-i}\sim w^t_{-i}}\big[u_i(x, s_{-i})\big], \qquad x \in S_i ,$$

so that $\langle w_i^t, u_i^t\rangle$ is the expected utility of player $i$ at round $t$. The regret of player $i$ is

$$r_i(T) = \sup_{w^* \in \Delta} \sum_{t=1}^T \langle w^* - w_i^t, u_i^t\rangle .$$

The primal norm is $\|v\| = \|v\|_1$ and its dual is $\|v\|_* = \|v\|_\infty$. A regularizer $\mathcal R : \Delta \to \mathbb R$ is 1-strongly convex if $\mathcal R(\tfrac{a+b}{2}) \le \tfrac{\mathcal R(a) + \mathcal R(b)}{2} - \tfrac{\|a-b\|_1^2}{8}$ for all $a, b \in \Delta$, and $R$ denotes a bound on its range, $\mathcal R(f) - \mathcal R(g) \le R$ on $\Delta$. Optimistic FTRL with step size $\eta > 0$ and predictors $M^t_i$ plays $w_i^0 = \operatorname{argmin}_\Delta \mathcal R$ and, for $T \ge 1$,

$$w_i^T \in \operatorname*{argmax}_{w \in \Delta}\ \Big\langle w, \sum_{t=1}^{T-1} u_i^t + M_i^T\Big\rangle - \frac{\mathcal R(w)}{\eta}.$$

With one-step recency bias, $M_i^T = u_i^{T-1}$: the algorithm bets that the next utility vector equals the last one.

An algorithm has the RVU property with constants $\alpha > 0$, $0 < \beta \le \gamma$ if for every utility sequence

$$\sum_{t=1}^T\langle w^* - w^t, u^t\rangle \le \alpha + \beta\sum_{t=1}^T \|u^t - u^{t-1}\|_*^2 - \gamma \sum_{t=1}^T \|w^t - w^{t-1}\|^2 .$$

Formalization targets

Goal: Corollary 8

If every player runs OFTRL with $M_i^t = u_i^{t-1}$ and $\eta = 1/(2(n-1))$, $n \ge 2$, then for every $T$

$$\sum_{i} r_i(T) \le \frac{nR}{\eta} = 2n(n-1)R .$$

Milestones

1. Theorem 19 (supp. p. 3): the regret of OFTRL with any predictor sequence is at most $R/\eta + \sum_t \|u^t - M^t\|_*\|w^t - g^t\| - \frac{1}{2\eta}\sum_t(\|w^t - g^t\|^2 + \|w^t - g^{t-1}\|^2)$, where $g^t$ is the leader sequence.
2. Lemma 20 (supp. p. 4): $\|w^t - g^t\| \le \eta\|M^t - u^t\|_*$ and $\|g^t - w^{t+1}\| \le \eta\|M^{t+1}\|_*$.
3. Proposition 7 (p. 5): OFTRL with $M^t = u^{t-1}$ has RVU with $\alpha = R/\eta$, $\beta = \eta$, $\gamma = 1/(4\eta)$.
4. Display (2) (p. 4): $\|u_i^t - u_i^{t-1}\|_*$ is at most the total variation between the opponents' product distributions, which is at most $\sum_{j \ne i}\|w_j^t - w_j^{t-1}\|_1$.
5. The variation bound (p. 4): $\sum_i \|u^t_i - u^{t-1}_i\|_*^2 \le (n-1)^2 \sum_i \|w_i^t - w_i^{t-1}\|_1^2$.
6. Theorem 4 (p. 4): if every player satisfies RVU with $\beta \le \gamma/(n-1)^2$ and $\|\cdot\| = \|\cdot\|_1$, then $\sum_i r_i(T) \le \alpha n$.

A companion statement, Proposition 2 (p. 3), turns a regret bound into a welfare bound in a $(\lambda,\mu)$-smooth game: $\frac1T\sum_t W(w^t) \ge \frac{\lambda}{1+\mu}\mathrm{OPT} - \frac{1}{1+\mu}\frac1T\sum_i r_i(T)$.

Significance

Corollary 8 says that uncoupled learning dynamics, in which each player sees only its own utility vectors, can keep the total regret of all players bounded by a constant in an arbitrary finite game. By Proposition 2 this gives $O(1/T)$ convergence of the average welfare to the price-of-anarchy bound in smooth games, against $O(1/\sqrt T)$ for generic no-regret algorithms. The RVU framework has since become a standard tool in the analysis of optimistic learning in games, and Theorem 4 decouples the game-level argument from the choice of algorithm.

The paper's proofs are in its supplementary material (App. A and C). None of the results here has a machine-checked proof to our knowledge. A complete formalization produces a reusable layer: utility vectors of mixed profiles, total-variation subadditivity for finite product distributions, and the regret analysis of optimistic FTRL under an $\ell_1$-strongly convex regularizer.

Difficulty

The game-level step (Theorem 4) is short once display (2) is available, but (2) itself, subadditivity of total variation over products of $n-1$ finite distributions, is not available in Mathlib in this form.

The core is the single-player analysis. Theorem 19 and Lemma 20 compare the iterates with the leader sequence, an object the algorithm never computes, and both rest on the quadratic-growth fact that a maximizer $w$ of a $1/\eta$-strongly concave function $F$ satisfies $F(w) \ge F(g) + \frac{1}{2\eta}\|w - g\|^2$. Footnote 3's midpoint inequality does not give the constant $\frac{1}{2\eta}$ in a single application; it has to be upgraded to the standard form of strong convexity first.

Formalization scope

Players are Fin n, strategies Fin d; time keeps the paper's indices $t = 1, \dots, T$ with $w^0$ and $u^0$. $u_i^0$ is the utility vector against $w^0_{-i}$, the formula of p. 2 at $t = 0$, which the paper uses but never writes. Mixed profiles and expectations come from the published definition agt_games. $\|\cdot\|_1$ is defined explicitly and $\|\cdot\|_*$ is Mathlib's sup norm. Regret and $R$ are never written as suprema: a bound on $\sum_i r_i(T)$ is stated for every profile of comparators in $\Delta$, and $R$ is any upper bound on the range of every regularizer.

Added hypotheses, each disclosed in its statement:

• each regularizer is continuous on $\Delta$, which makes footnote 3 equivalent to standard strong convexity;
• $n \ge 2$ in the goal;
• Theorem 4's condition is written as $\beta(n-1)^2 \le \gamma$, so $n = 1$ involves no division by zero;
• RVU is assumed in Theorem 4 only on the realized play, a weaker hypothesis than the paper's;
• $T \ge 1$ and $1 + \mu > 0$ in Proposition 2;
• per-player regularizers $\mathcal R_i$ (footnote 2).

Theorem 19, Lemma 20 and Proposition 7 are stated for $\ell_1$; the paper allows any norm.

OFTRL is an argmax predicate, so the goal holds for every trajectory the dynamics can produce, not for a chosen one. It is not the entropic closed form (Optimistic Hedge). The utility bound $u_i \in [0,1]$ is kept, since the game-level statements are false without it. A sanity file shows that $\mathcal R(w) = \frac d2\sum_x w_x^2$ satisfies the strong-convexity hypothesis and that OFTRL runs exist, so the hypotheses are satisfiable.

Contributions are welcome for each milestone. The quadratic-growth lemma for midpoint strongly convex continuous functions on the simplex and the total-variation bound for products are reusable beyond this mission.

Selected references

• V. Syrgkanis, A. Agarwal, H. Luo, R. E. Schapire, Fast Convergence of Regularized Learning in Games, NIPS 2015. arXiv:1507.00407v5. https://arxiv.org/abs/1507.00407
• A. Rakhlin, K. Sridharan, Online Learning with Predictable Sequences, COLT 2013. https://arxiv.org/abs/1208.3728
• A. Rakhlin, K. Sridharan, Optimization, Learning, and Games with Predictable Sequences, NIPS 2013. https://arxiv.org/abs/1311.1869
• T. Roughgarden, Intrinsic Robustness of the Price of Anarchy, STOC 2009. https://doi.org/10.1145/1536414.1536485

Motivation

Reinforcement learning with large or continuous state spaces is done in practice with function approximation: the agent represents value functions in a low-dimensional parametric family instead of a table indexed by states. For tabular Markov decision processes, regret bounds of order $\sqrt{H^2SAT}$ have been known since the work on UCRL and UCBVI, but they scale with the number of states $S$ and actions $A$ and say nothing when $S$ is infinite. Before 2019, provable guarantees for function approximation either needed a simulator, assumed deterministic transitions, or had regret exponential in the horizon.

Jin, Yang, Wang and Jordan, Provably Efficient Reinforcement Learning with Linear Function Approximation (arXiv:1907.05388, COLT 2020), identified a model, the linear MDP, in which an optimistic version of least-squares value iteration has regret polynomial in the feature dimension $d$ and the horizon $H$ and independent of $S$ and $A$. The model and the algorithm, LSVI-UCB, became a standard reference point for the theory of RL with function approximation.

Timeline:

• 2017–2018: Azar, Osband, Munos (arXiv:1703.05449) and Jin, Allen-Zhu, Bubeck, Jordan (arXiv:1807.03765) give near-optimal $\sqrt T$ regret for tabular episodic MDPs.
• 2019: Yang and Wang (arXiv:1902.04779) study linear transition models with a simulator; Jin, Yang, Wang, Jordan prove Theorem 3.1 below without a simulator.
• 2020: Zanette, Lazaric, Kochenderfer, Brunskill (arXiv:2003.00153) improve the dependence on $d$ under a low inherent Bellman error assumption.

Setting

An episodic MDP $\mathrm{MDP}(\mathcal S,\mathcal A,H,\mathbb P,r)$ has a measurable state space $\mathcal S$, a finite action set $\mathcal A$, a horizon $H$, transition kernels $\mathbb P_h(\cdot\mid x,a)$ and deterministic rewards $r_h(x,a)\in[0,1]$ for steps $h=1,\dots,H$. A policy $\pi(x,h)$ chooses an action at each state and step. Its value functions satisfy the Bellman equation $Q^\pi_h=r_h+\mathbb P_hV^\pi_{h+1}$, $V^\pi_h(x)=Q^\pi_h(x,\pi(x,h))$, $V^\pi_{H+1}=0$, where $\mathbb P_hV(x,a)=\int V\,d\mathbb P_h(\cdot\mid x,a)$; the optimal values $V^\star_h$, $Q^\star_h$ satisfy the same recursion with a maximum over actions.

The MDP is linear (Assumption A) with feature map $\phi:\mathcal S\times\mathcal A\to\mathbb R^d$ if $\|\phi\|\le1$ and for each step there are signed measures $\boldsymbol\mu_h=(\mu_h^{(1)},\dots,\mu_h^{(d)})$ and a vector $\theta_h$ with

$$\mathbb P_h(\cdot\mid x,a)=\langle\phi(x,a),\boldsymbol\mu_h(\cdot)\rangle,\qquad r_h(x,a)=\langle\phi(x,a),\theta_h\rangle,$$

and $\|\theta_h\|\le\sqrt d$, $\|(|\mu_h^{(1)}|(\mathcal S),\dots,|\mu_h^{(d)}|(\mathcal S))\|\le\sqrt d$.

In each episode $k=1,\dots,K$ an adversary chooses the initial state $x^k_1$; the agent then plays $H$ steps, the next state $x^k_{h+1}$ being drawn from $\mathbb P_h(\cdot\mid x^k_h,a^k_h)$. LSVI-UCB (Algorithm 1) computes, backwards over $h$, the Gram matrix $\Lambda^k_h=\sum_{\tau<k}\phi^\tau_h(\phi^\tau_h)^\top+\lambda I$ of the past features $\phi^\tau_h=\phi(x^\tau_h,a^\tau_h)$, the ridge-regression weight $w^k_h$ for the targets $r_h+\max_aQ^k_{h+1}$, and the optimistic estimate

$$Q^k_h(x,a)=\min\Big\{(w^k_h)^\top\phi(x,a)+\beta\sqrt{\phi(x,a)^\top(\Lambda^k_h)^{-1}\phi(x,a)},\ H\Big\},$$

and then plays greedily with respect to $Q^k_h$. Its policy in episode $k$ is $\pi_k$, and the regret is

$$\mathrm{Regret}(K)=\sum_{k=1}^K\big[V^\star_1(x^k_1)-V^{\pi_k}_1(x^k_1)\big],\qquad T=KH.$$

Formalization targets

Goal: Theorem 3.1

There are absolute constants $c,C>0$ such that for every linear MDP, every $p\in(0,1)$ and every run of LSVI-UCB with $\lambda=1$ and $\beta=c\cdot dH\sqrt\iota$, $\iota=\log(2dT/p)$,

$$\mathbb P\Big(\mathrm{Regret}(K)\le C\sqrt{d^3H^3T\iota^2}\Big)\ge1-p .$$

Milestones

The milestones follow Appendix B of the paper: linearity of $Q^\pi$ (Proposition 2.3) and the weight bounds (Lemmas B.1, B.2, with Lemma D.1); the covering bound for the value class (Lemma D.6, with the Euclidean-ball covering of Lemma D.5); the uniform self-normalized concentration (Lemma D.4, with Theorem D.3) and the good event (Lemma B.3); the error propagation (Lemma B.4), optimism (Lemma B.5) and the recursion (Lemma B.6); and the bonus-sum bound (17)–(18), with Lemma D.2. Lemma D.2, Theorem D.3 and Lemma D.5 are already on the platform and are referenced.

A companion statement, not a milestone, formalizes Proposition 5.1 (§5): on a finite state space with non-degenerate features, if the Bellman operators $\mathbb T^\pi_h$ of (8) map linear action-value functions to linear ones for every policy, then $\mathbb P_h$ is linear in $\phi$.

Significance

The theorem shows that exploration with function approximation can be sample-efficient without a simulator: the regret depends on the intrinsic dimension $d$ of the features and polynomially on $H$, not on the size of the state space. Its analysis, a uniform concentration bound over a data-dependent class of value functions combined with optimism, is the template for a large later literature: misspecified and low-rank MDPs, kernel and neural function approximation, and reward-free exploration.

The result has a published proof, but no machine-checked one. A formalization supplies the measure-theoretic episodic MDP on a general state space, an interaction protocol with adaptive initial states, the LSVI-UCB algorithm, and a checked chain from self-normalized martingale bounds to the regret theorem. The formal statements also record two points where the printed paper is imprecise: the normalization of the measures $\boldsymbol\mu_h$ (see Formalization scope) and the existential reading of the weights in Lemma B.1.

Difficulty

The regression targets $r_h+\max_aQ^k_{h+1}(x^\tau_{h+1},\cdot)$ depend on all past data through $Q^k_{h+1}$. The self-normalized bound for vector-valued martingales (Theorem D.3) therefore cannot be applied to them directly: the natural first idea, conditioning on the past and treating $V^k_{h+1}$ as fixed, fails because $V^k_{h+1}$ is not measurable with respect to the past at the time $x^\tau_{h+1}$ is drawn. The concentration must hold uniformly over a function class, which requires a covering-number bound for a class parametrized by vectors and matrices (Lemma D.6) and a union bound in the right scale.

A second difficulty is formal: the probabilistic protocol mixes an adversary, a learning algorithm reading its own past outputs, and transition kernels on a general measurable space, and the martingale argument (Azuma–Hoeffding over the $KH$ steps) needs every object to be measurable with respect to the right σ-algebra.

Formalization scope

• Model. $\mathcal S$ is any measurable space; $\mathcal A$ is a finite nonempty type with its discrete σ-algebra and a linear order used only to break ties in the argmax. Steps and episodes are 1-based. $V^\pi$, $Q^\pi$, $V^\star$, $Q^\star$ are defined by the Bellman recursions (1) and (2), with value $0$ outside $1\le h\le H$; theorems about general policies assume them measurable.
• Assumption A is stated with the total-variation normalization $\|(|\mu_h^{(i)}|(\mathcal S))_i\|\le\sqrt d$ instead of the printed $\|\boldsymbol\mu_h(\mathcal S)\|\le\sqrt d$; under the printed condition Lemma B.1 is false. The feature map is assumed measurable.
• Runs. A run is a process on a probability space with a filtration over the flattened time $(k-1)(H+1)+(h-1)$: states are adapted, actions are those of Algorithm 1, and the conditional law of $x^k_{h+1}$ given the past is $\mathbb P_h(\cdot\mid x^k_h,a^k_h)$. The initial states are otherwise unrestricted.
• Constants. $c$ and $C$ are quantified before the spaces, $d$, $H$, $K$, $p$, the MDP and the run; $d,H,K\ge1$ and $p\in(0,1)$. "With probability $1-p$" is an upper bound on the outer measure of the failure event.
• Ruling out trivializations. The goal does not assume the good event, optimism, or any milestone conclusion; $\beta$ is fixed by the existentially quantified $c$, not free; the regret uses the model value of the greedy policy, not a realized return. A sorry-free check exhibits a linear MDP and a run satisfying all hypotheses.
• Known gap. Algorithm 1 clips $Q^k_h$ only from above, so the bound $|V^k_{h+1}|\le H$ that Lemma B.3's proof needs (and the target bound in Lemma B.2's proof, here an explicit hypothesis) is not automatic off the good event. Lemma B.3 is stated as printed, for every $c_\beta>0$; a solver who finds it unprovable should report this in the discussion.
• Infrastructure needed: covering numbers of norm balls, the self-normalized martingale bound, Azuma–Hoeffding (in Mathlib), integration against signed measures, and measurability of the algorithm's outputs. The MDP and run definitions are reusable for other episodic RL results; contributions of general lemmas about them are welcome.

Selected references

• C. Jin, Z. Yang, Z. Wang, M. I. Jordan, Provably Efficient Reinforcement Learning with Linear Function Approximation, COLT 2020; arXiv:1907.05388v2, 2019. https://arxiv.org/abs/1907.05388
• Y. Abbasi-Yadkori, D. Pál, Cs. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, NeurIPS 2011. https://papers.nips.cc/paper/2011/hash/e1d5be1c7f2f456670de3d53c7b54f4a-Abstract.html
• M. G. Azar, I. Osband, R. Munos, Minimax Regret Bounds for Reinforcement Learning, ICML 2017. https://arxiv.org/abs/1703.05449
• C. Jin, Z. Allen-Zhu, S. Bubeck, M. I. Jordan, Is Q-learning Provably Efficient?, NeurIPS 2018. https://arxiv.org/abs/1807.03765
• L. F. Yang, M. Wang, Sample-Optimal Parametric Q-Learning Using Linearly Additive Features, ICML 2019. https://arxiv.org/abs/1902.04779
• A. Zanette, A. Lazaric, M. Kochenderfer, E. Brunskill, Learning Near Optimal Policies with Low Inherent Bellman Error, ICML 2020. https://arxiv.org/abs/2003.00153

Motivation

Many problems in machine learning and signal processing minimize a smooth loss plus a simple non-smooth regularizer: $\ell_1$-regularized least squares, group-sparse regression, and constrained problems written with an indicator function. The standard algorithm for this composite form is the proximal-gradient method, a gradient step on the smooth part followed by a proximal step on the regularizer. Its classical linear convergence guarantee needs the smooth part to be strongly convex, a hypothesis that fails for $\ell_1$-regularized least squares with fewer observations than variables and for most problems of interest without explicit $\ell_2$ regularization.

For smooth problems the Polyak–Łojasiewicz (PL) inequality $\tfrac12\|\nabla f(x)\|^2 \ge \mu(f(x) - f^*)$ gives a linear rate for gradient descent without convexity (Polyak 1963). Karimi, Nutini and Schmidt (arXiv:1608.04636, ECML PKDD 2016) propose a generalization to the composite setting, the proximal-PL inequality, under which the proximal-gradient method converges linearly with a one-paragraph proof. They show that it contains the PL case, the strongly convex case, and convex objectives with quadratic growth, and that it is equivalent to the Kurdyka–Łojasiewicz inequality (Bolte, Nguyen, Peypouquet, Suter 2017) and to the proximal error bound used earlier by Luo, Tseng and Drusvyatskiy–Lewis.

Timeline:

• 1963: Polyak proves linear convergence of gradient descent under the PL inequality.
• 1993: Luo and Tseng prove linear convergence of feasible descent methods under an error bound.
• 2015–2016: Bolte et al. and Li–Pong obtain linear rates of proximal gradient under the KL inequality; Drusvyatskiy and Lewis relate error bounds and quadratic growth (arXiv:1602.06661).
• 2016: Karimi, Nutini and Schmidt introduce the proximal-PL inequality and Theorem 5.

Setting

Let $f, g : \mathbb R^d \to \mathbb R$ and consider problem (11),

$$\min_{x \in \mathbb R^d} F(x) = f(x) + g(x).$$

The function $f$ is differentiable with an $L$-Lipschitz gradient, $\|\nabla f(x) - \nabla f(y)\| \le L\|x - y\|$ with $L > 0$. The function $g$ is convex. $F$ has a minimizer $x^*$, and $F^* = F(x^*)$.

For a base point $x$ and a parameter $\alpha > 0$, the proximal model is

$$m_{x,\alpha}(y) = \langle \nabla f(x), y - x\rangle + \frac{\alpha}{2}\|y - x\|^2 + g(y) - g(x),$$

and the paper's measure of non-stationarity is

$$\mathcal D_g(x, \alpha) = -2\alpha \min_{y} m_{x,\alpha}(y). \tag{13}$$

$F$ satisfies the proximal-PL inequality with modulus $\mu > 0$ if

$$\tfrac12\,\mathcal D_g(x, L) \ge \mu\bigl(F(x) - F^*\bigr) \quad \text{for all } x. \tag{12}$$

When $g$ is constant, $\mathcal D_g(x, \alpha) = \|\nabla f(x)\|^2$ and (12) is the PL inequality.

The proximal-gradient method with step size $1/L$ starts at an arbitrary $x_0$ and sets

$$x_{k+1} \in \operatorname*{argmin}_y m_{x_k, L}(y). \tag{14}$$

The proximal residual function of Appendix E is $\mathcal R_g(\lambda, x, a) = \min_y [\|\lambda(y - x) + a\|^2 + 2\lambda(g(y) - g(x))]$.

Formalization targets

Goal: Theorem 5 (p. 8)

Under the hypotheses above,

$$F(x_k) - F^* \le \Bigl(1 - \frac{\mu}{L}\Bigr)^k \bigl[F(x_0) - F^*\bigr] \qquad \text{for every } k \ge 0.$$

Milestones (proof of Theorem 5)

1. The quadratic upper bound (2), p. 2: an $L$-Lipschitz gradient gives $f(y) \le f(x) + \langle\nabla f(x), y - x\rangle + \frac L2\|y - x\|^2$.
2. Descent by $\mathcal D_g$, p. 9: if $x^+$ minimizes $m_{x,L}$, then $F(x^+) \le F(x) - \frac{1}{2L}\mathcal D_g(x, L)$.
3. The one-step contraction (15), p. 9: $F(x^+) - F^* \le (1 - \mu/L)[F(x) - F^*]$.

Companion results

• Lemma 2 (p. 17): for convex $g$, $\mathcal R_g(\cdot, x, a)$ is non-increasing on $(0, \infty)$.
• Lemma 1 = Corollary 1 (p. 17): $\mathcal D_g(x, \mu_2) \ge \mathcal D_g(x, \mu_1)$ for $\mu_2 \ge \mu_1 > 0$.
• Appendix F, item 1 (p. 18): for constant $g$, $\mathcal D_g(x, \alpha) = \|\nabla f(x)\|^2$, and proximal-PL is PL.
• Appendix F, item 2 (p. 18): for $\mu$-strongly convex $f$, $F^* \ge F(x) - \frac{1}{2\mu}\mathcal D_g(x, \mu)$.
• Appendix F, item 4 (p. 19): for convex $f$ and $F$ with quadratic growth of modulus $\mu$, $\mathcal D_g(x, \mu/2) \ge \frac{\mu}{2}(F(x) - F^*)$.
• Two well-definedness statements: for convex $g$ and a positive parameter, the minima in (13) and (27) are attained.

Significance

Theorem 5 gives a global linear rate for the proximal-gradient method under a hypothesis that does not require strong convexity, or convexity of $f$. Through the classes of Section 4.1 it covers $\ell_1$-regularized least squares, the composite strongly convex case, and convex composite problems with quadratic growth. The quantity $\mathcal D_g$ also drives the analysis of proximal coordinate descent (Theorem 6, mission VI of this series), and Lemma 1 is what lets the sufficient conditions of Appendix F, which hold with $\mathcal D_g(x, \lambda)$ for $\lambda \le L$, be used in (12).

The results are proved in the paper; none of them has a machine-checked proof that this mission knows of. The work here is to formalize the known proofs, including the properties of $\mathcal D_g$ and $\mathcal R_g$ that the paper uses without stating: the minimum in (13) exists, and the value is finite.

Difficulty

The proof of Theorem 5 is short; the difficulty sits in the objects. $\mathcal D_g$ is defined through a minimum over $\mathbb R^d$ of a function involving a non-smooth convex $g$, so every step that replaces the minimum by its value at a particular point needs the minimum to be finite and attained. The paper never states these facts, and they fail for an arbitrary $g$: for $g(y) = -\|y\|^2$ and $\alpha < 2$ the model is unbounded below and the minimum in (13) does not exist. The monotonicity of $\mathcal D_g$ in its second argument (Lemma 1) rests on the convexity inequality of $g$, and Appendix F item 4 relies on the projection onto the solution set, whose existence depends on that set being closed, convex and non-empty.

Formalization scope

• $\mathbb R^d$ is EuclideanSpace ℝ (Fin d), $\nabla f$ is Mathlib's gradient f, and the Lipschitz hypothesis is written literally, ‖gradient f x - gradient f y‖ ≤ L * ‖x - y‖, with 0 < L.
• The non-empty solution set is a point xstar with F xstar ≤ F y for all y; $F^*$ is f xstar + g xstar, never a free real.
• $g$ is real-valued and convex (ConvexOn ℝ Set.univ g). Indicator functions of convex sets, which the paper lists among its examples, take the value $+\infty$ and are outside this formalization; the formulas (13)–(15) subtract values of $g$, which is undefined at $+\infty$.
• The minimum in (13) and (27) is a real infimum. A real infimum of a set that is unbounded below has the junk value $0$ in Lean, so $\mathcal D_g(x, \alpha)$ is used only with $\alpha > 0$ and convex $g$, where the infimum is a minimum; this rules out the trivializing reading in which $\mathcal D_g$ vanishes and (12) becomes $F \le F^*$.
• A proximal-gradient run is any sequence whose every step is a minimizer of the model; the minimizer is unique for convex $g$, but uniqueness is not assumed.
• No relation between $\mu$ and $L$ is assumed, as in the paper.
• The PL predicate in Appendix F item 1 is the published ShiOptRates.PolyakLojasiewicz (the paper's (3) multiplied by 2), and (2) is the published ShiOptRates.QuadUpper.

Quadratic growth is stated with the distance to the solution set, $\operatorname{dist}(x, \mathcal X^*)$, which equals $\|x - x_p\|$ for the projection $x_p$ the paper uses. Appendix F item 3 (Hoffman's bound with an unspecified constant $\theta(A, B)$) and the equivalences of Appendix G are not included.

Contributions of every kind are welcome: proofs of the milestones, of the companion lemmas, and reusable facts about $\mathcal D_g$ (finiteness, attainment, continuity in $x$) that other proximal-method missions can import.

Selected references

• H. Karimi, J. Nutini, M. Schmidt, Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak-Łojasiewicz Condition, ECML PKDD 2016; arXiv:1608.04636v4, 2020. https://arxiv.org/abs/1608.04636
• B. T. Polyak, Gradient methods for minimizing functionals, USSR Computational Mathematics and Mathematical Physics 3(4), 1963. https://doi.org/10.1016/0041-5553(63)90382-3
• Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Annals of Operations Research 46, 1993. https://doi.org/10.1007/BF02096261
• J. Bolte, T. P. Nguyen, J. Peypouquet, B. W. Suter, From error bounds to the complexity of first-order descent methods for convex functions, Mathematical Programming 165, 2017. https://doi.org/10.1007/s10107-016-1091-6
• D. Drusvyatskiy, A. S. Lewis, Error bounds, quadratic growth, and linear convergence of proximal methods, Mathematics of Operations Research 43(3), 2018. https://arxiv.org/abs/1602.06661
• G. Li, T. K. Pong, Calculus of the exponent of Kurdyka–Łojasiewicz inequality and its applications to linear convergence of first-order methods, Foundations of Computational Mathematics 18, 2018. https://arxiv.org/abs/1602.02915