Machine Learning

Motivation

Gradient descent is a basic method for minimizing a differentiable function when evaluating its gradient is practical but solving the optimization problem directly is not. The rate at which its iterates approach an optimizer depends on the assumptions about the function. For a convex function with a Lipschitz gradient, the value error decreases at a sublinear rate. Adding strong convexity changes the behavior: the distance from the optimizer contracts at each step, giving an exponential bound on the value error. This section of Bubeck's monograph identifies a fixed step size that uses both the smoothness and curvature constants and gives the corresponding rate.

The result matters when a high-accuracy answer is needed. A sublinear bound makes each extra digit progressively more expensive; an exponential bound says that a fixed number of additional gradient evaluations reduces the error by a fixed factor. The theorem is a textbook result, already proved mathematically. This mission asks for its precise machine-checked statement and the source's supporting inequalities, rather than for a new optimization method.

Setting

Work in Euclidean space $\mathbb R^n$ with $n\ge1$, equipped with its usual inner product and norm. A differentiable function $f:\mathbb R^n\to\mathbb R$ has gradient $g(x)=\nabla f(x)$. It is $\beta$-smooth when its gradient is $\beta$-Lipschitz: $\|g(x)-g(y)\|\le\beta\|x-y\|$ for every $x,y$. It is $\alpha$-strongly convex when, for every $x,y$,

$$f(y)\ge f(x)+\langle g(x),y-x\rangle+\frac\alpha2\|y-x\|^2.$$

The first condition limits how rapidly the gradient changes. The second gives a quadratic lower bound on the function around any point. Here $\alpha>0$ and $\beta\ge0$. In positive dimension, the two conditions together entail $\beta\ge\alpha$, so the condition number $\kappa=\beta/\alpha$ is at least one. The case $\alpha=\beta$ remains part of the target.

A point $x^*$ is a global minimizer when $f(x^*)\le f(y)$ for every $y$. The book assumes such a point exists as a standing convention. A gradient descent run is a sequence $(x_t)_{t\ge1}$ satisfying $x_{t+1}=x_t-\eta g(x_t)$ at each positive index. Its first iterate $x_1$ is arbitrary. The step size in this mission is fixed at $\eta=2/(\alpha+\beta)$, rather than chosen by line search or adapted along the run.

Formalization targets

The central target is Theorem 3.12 of Bubeck, p. 279. For every integer $t\ge0$, the gradient descent run satisfies

$$f(x_{t+1})-f(x^*)\le \frac\beta2\exp\!\left(-\frac{4t}{\kappa+1}\right)\|x_1-x^*\|^2.$$

At $t=0$ this is a smoothness bound on the initial value gap. For subsequent iterations it gives a linear convergence rate with the explicit exponential factor stated in the book. No initial-radius bound or bounded domain is imposed: the actual squared distance $\|x_1-x^*\|^2$ appears in the conclusion.

The milestones trace the mathematical claims stated in the source. Equation (3.6) is the co-coercivity inequality for gradients of convex smooth functions. The proof of Lemma 3.11 introduces $\phi(z)=f(z)-(\alpha/2)\|z\|^2$, and identifies it as convex and $(\beta-\alpha)$-smooth. Lemma 3.11 combines curvature and smoothness into a sharper inequality for two gradients. The proof of Theorem 3.12 then gives a value-gap bound, a one-step distance contraction, and its iterated exponential form. These statements are separately useful: the co-coercivity and contraction bounds can be reused in analyses of related first-order methods.

Significance

The theorem states a complete guarantee for the algorithm: an explicit rule, the hypotheses on the objective, and a bound valid for every iteration count. It makes the role of $\kappa$ visible. When $\kappa$ is close to one, the contraction is strong; when the smoothness constant is much larger than the curvature constant, more iterations are needed for the same error reduction. The stated dependence supports comparisons with projected and accelerated gradient methods elsewhere in the same monograph.

Formalizing the result requires a common interface for actual gradients, smoothness, strong convexity, and algorithm runs. The strong-convexity predicate is an existing published definition, while the local smoothness and run definitions use Bubeck's conventions. Once these interfaces and the inequalities are proved, later missions can use the resulting declarations to compare rates without translating between informal meanings of “smooth” or changing the iterate index. The source provides a mathematical proof; these draft Lean theorems carry sorry and do not yet constitute machine-checked proofs.

Difficulty

The main issue is getting the sharp contraction factor from two assumptions that control different parts of the gradient step. A direct Lipschitz estimate on the update map does not by itself express the mixed inner-product term with the constants needed for the stated factor. Lemma 3.11 is the source's precise bridge between the gradient difference, the point displacement, and their inner product. The case $\alpha=\beta$ also needs to remain valid: a proof route that divides by $\beta-\alpha$ cannot cover that boundary by the same calculation.

The last display in the proof of Theorem 3.12 joins a one-step inequality involving $x_t$ to an exponential inequality involving $x_1$. The latter is the cumulative statement after $t$ steps. Keeping these as separate milestones makes each quantified claim explicit while preserving the theorem's bound.

Formalization scope

Lean represents $\mathbb R^n$ as EuclideanSpace ℝ (Fin n), with $n>0$. The gradient is an explicit map $g$ required to be the actual gradient of $f$ at every point. Smoothness is the gradient Lipschitz condition, not a quadratic upper bound used as a definition. Strong convexity uses the published OnlineConvexOpt.ConvexBasics.StronglyConvexOn predicate on the whole space; its formula is the book's (3.13). Iterates are indexed from one, and index zero imposes no condition. The norm, inner product, constants, and real exponential follow the printed formulas.

The added explicit conditions are $n>0$, $\alpha>0$, and $\beta>0$ where Equation (3.6) divides by $\beta$. Positive dimension excludes a degenerate space where curvature imposes no restriction on smoothness. The positivity of $\alpha$ makes $\kappa$ meaningful; the source treats it as a positive strong-convexity parameter. The minimizer hypothesis is the book's standing convention. There is no assumption that $g(x^*)=0$: that property follows from global minimality and differentiability. A gradient map unrelated to $f$ would trivialize the model, so the smoothness definition includes the gradient identity.

The local development needs Euclidean inner-product identities, convexity, differentiability, Lipschitz gradient bounds, and real exponential estimates. The auxiliary function and the two co-coercivity inequalities are reusable outside this chapter. Contributions should prove the exact milestone statements and the final theorem, including $t=0$ and $\alpha=\beta$, without weakening constants or substituting another gradient descent step.

Selected references

• Sébastien Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2; DOI:10.1561/2200000050.

Motivation

Gradient descent goes back to Cauchy (1847). It is the simplest method for minimizing a differentiable function, and most of the first-order methods in large-scale optimization and machine learning are variants of it. Its appeal in high dimension is that its oracle complexity, the number of gradient evaluations needed to reach a given accuracy, can be bounded independently of the dimension. For a merely Lipschitz convex function the projected subgradient method needs on the order of $1/\varepsilon^2$ steps to reach accuracy $\varepsilon$ (Theorem 3.2 of the book). Under a smoothness assumption gradient descent does much better, because the gradients shrink near the optimum and the steps adapt automatically.

This mission formalizes the basic result of that kind: Theorem 3.3 of S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning 8(3–4), 2015; arXiv:1405.4980v2). It states that gradient descent with step size $1/\beta$ on a convex $\beta$-smooth function on $\mathbb R^n$ has optimality gap $O(1/t)$ after $t$ steps. The result and its proof are standard; versions appear in Nesterov's Introductory Lectures on Convex Optimization (2004, §2.1.5). It is the fourth mission in a series that formalizes the capstone results of Bubeck's monograph.

Setting

Write $\mathbb R^n$ for Euclidean space with inner product $x^\top y$ and norm $\|\cdot\|$. Let $f:\mathbb R^n\to\mathbb R$ be differentiable with gradient $\nabla f$.

• $f$ is convex if $f((1-\lambda)x+\lambda y)\le(1-\lambda)f(x)+\lambda f(y)$ for all $x,y$ and $\lambda\in[0,1]$.
• For $\beta\ge0$, $f$ is $\beta$-smooth if its gradient is $\beta$-Lipschitz:

$$\|\nabla f(x)-\nabla f(y)\|\le\beta\|x-y\|\qquad\text{for all }x,y\in\mathbb R^n.$$

• A minimizer is a point $x^*$ with $f(x^*)\le f(y)$ for every $y$. Throughout the book a minimizer is assumed to exist.
• Gradient descent with step size $\eta>0$, started at $x_1\in\mathbb R^n$, is the sequence

$$x_{t+1}=x_t-\eta\nabla f(x_t),\qquad t\ge1. \tag{3.1}$$

The optimality gaps are $\delta_s=f(x_s)-f(x^*)\ge0$.

Formalization targets

Goal: Theorem 3.3 (p. 267)

If $f$ is convex and $\beta$-smooth with $\beta>0$, $x^*$ is a minimizer, and $(x_t)$ is gradient descent with $\eta=1/\beta$, then for every $t\ge2$

$$f(x_t)-f(x^*)\le\frac{2\beta\|x_1-x^*\|^2}{t-1}.$$

Milestones

These are the statements the book's proof uses, in the book's order:

1. Lemma 3.4 (p. 267). For any $\beta$-smooth $f$, with no convexity: $|f(x)-f(y)-\nabla f(y)^\top(x-y)|\le\frac\beta2\|x-y\|^2$.
2. (3.4) (p. 267). For convex $\beta$-smooth $f$: $0\le f(x)-f(y)-\nabla f(y)^\top(x-y)\le\frac\beta2\|x-y\|^2$.
3. (3.5) (p. 267). For convex $f$, one step of length $1/\beta$ decreases $f$ by at least $\frac1{2\beta}\|\nabla f(x)\|^2$.
4. Lemma 3.5 (p. 268). If (3.4) holds, then $f(x)-f(y)\le\nabla f(x)^\top(x-y)-\frac1{2\beta}\|\nabla f(x)-\nabla f(y)\|^2$.
5. (3.6) (p. 269). Co-coercivity: $(\nabla f(x)-\nabla f(y))^\top(x-y)\ge\frac1\beta\|\nabla f(x)-\nabla f(y)\|^2$.
6. Distances decrease (proof of Theorem 3.3, p. 269). $\|x_{s+1}-x^*\|\le\|x_s-x^*\|$ for every $s\ge1$.
7. The recursion (p. 268). $\delta_{s+1}\le\delta_s-\frac{1}{2\beta\|x_1-x^*\|^2}\delta_s^2$.
8. From the recursion to the rate (p. 269). For $\omega>0$ and non-negative reals, $\omega\delta_s^2+\delta_{s+1}\le\delta_s$ for all $s\ge 1$ implies $1/\delta_t\ge\omega(t-1)$.

Stronger companion: footnote 4 (p. 269)

Under the same hypotheses, $f(x_t)-f(x^*)\le 2\beta\|x_1-x^*\|^2/(t+3)$ for every $t\ge1$.

Significance

Theorem 3.3 is the reference rate for first-order methods on smooth convex problems. Several later results in the book are measured against it. Nesterov's accelerated gradient descent (§3.7) improves $1/t$ to $1/t^2$, the lower bounds of §3.5 show that $1/t^2$ cannot be beaten by any black-box first-order method, and adding strong convexity (§3.4) upgrades $1/t$ to a linear rate. Its ingredients are reused throughout the book and the optimization literature: the descent lemma (Lemma 3.4), the one-step improvement (3.5) and co-coercivity (3.6). Co-coercivity is the finite-dimensional case of the Baillon–Haddad theorem.

The result is classical and fully proved on paper. To our knowledge Mathlib does not contain this rate for gradient descent on convex smooth functions, and no published Prove2Me theorem states it. The mission provides it, together with Lemma 3.4 and co-coercivity as reusable statements on EuclideanSpace ℝ (Fin n). These are the facts that later missions of the series on projected gradient descent, strong convexity and acceleration need. Formalizing the improved constant of footnote 4 is a welcome addition.

Difficulty

Two steps are not routine. The first is Lemma 3.4, where the book integrates the gradient along a segment. In Lean this needs a mean-value or fundamental-theorem-of-calculus argument for a function on a Euclidean space, together with a Cauchy–Schwarz estimate, and Mathlib's HasGradientAt interface has to be connected to one-variable derivatives along lines.

The second is the monotonicity of $\|x_s-x^*\|$. The natural first attempt is to telescope the one-step improvement (3.5) together with the convexity bound $\delta_s\le\|x_s-x^*\|\|\nabla f(x_s)\|$. That gives a recursion involving $\|x_s-x^*\|$, which is not controlled by $\|x_1-x^*\|$ without further work. Making the recursion uniform requires co-coercivity (3.6), which comes from Lemma 3.5. That lemma's hypothesis is the two-sided inequality (3.4), not smoothness directly. The final numerical step divides by the gaps $\delta_s$, so zero gaps need separate handling.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), and $x^\top y$ is ⟪x, y⟫_ℝ.
• The gradient is an explicit map $g:\mathbb R^n\to\mathbb R^n$ with the hypothesis ∀ x, HasGradientAt f (g x) x.
• $\beta$-smoothness (IsBetaSmooth f g β) is the book's definition: $\beta\ge0$, the gradient-existence hypothesis, and the Lipschitz bound $\|g(x)-g(y)\|\le\beta\|x-y\|$. The book's "continuously differentiable" follows from it.
• Convexity is Mathlib's ConvexOn ℝ Set.univ f. A minimizer is a point xstar with ∀ y, f xstar ≤ f y; its existence is the book's standing assumption, and $\nabla f(x^*)=0$ is derived, not assumed.
• A gradient-descent run (IsGDRun g η x) is a sequence x : ℕ → ℝⁿ with $\eta>0$ and $x_{t+1}=x_t-\eta g(x_t)$ for every $t\ge1$. The book's $x_1$ is x 1, and index $0$ is unused. Every theorem quantifies over all runs with $\eta=1/\beta$.

Disclosed side conditions:

• $\beta>0$ wherever the page divides by $\beta$. Convexity is retained for (3.5), as in its source context.
• $t\ge2$ in the goal, where the page's bound has denominator $t-1$.
• Statements in which the page divides by $\delta_s$ or by $\|x_1-x^*\|^2$ are multiplied through, so that they stay true and meaningful when those quantities vanish.

A trivializing formalization is ruled out. Smoothness is the Lipschitz condition on the gradient, so Lemma 3.4 and (3.4) are not restatements of the definition, as they would be if the quadratic upper bound (3.4) were taken as the definition of smoothness. The run predicate also fixes the step size $1/\beta$.

A complete development needs:

• the segment integral or mean-value estimate for HasGradientAt functions;
• first-order characterizations of convexity for differentiable functions;
• elementary inner-product algebra.

Lemma 3.4, Lemma 3.5 and (3.6) are reusable well beyond this mission. Proofs of any milestone are welcome independently.

Selected references

• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–357, 2015. arXiv:1405.4980v2; §3.2, pp. 266–269.
• A. Cauchy, Méthode générale pour la résolution des systèmes d'équations simultanées, C. R. Acad. Sci. Paris 25:536–538, 1847.
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. doi:10.1007/978-1-4419-8853-9
• J.-B. Baillon and G. Haddad, Quelques propriétés des opérateurs angle-bornés et n-cycliquement monotones, Israel J. Math. 26:137–150, 1977. doi:10.1007/BF03007664

Motivation

In multiclass classification a learner sees examples $(x, y)$ with $x$ in a domain $\mathcal X$ and a label $y$ in a set $\mathcal Y$, and must predict labels of new points. When $\mathcal Y$ is finite, the Natarajan dimension characterizes PAC learnability, extending the role of the VC dimension in binary classification (Natarajan 1989; Ben-David, Cesa-Bianchi, Haussler, Long 1995). Label sets in practice are often unbounded: structured prediction, ranking, and language modelling all predict from very large or infinite label spaces. For infinite $\mathcal Y$ the Natarajan dimension fails to characterize learnability, and the question of which combinatorial parameter does was left open by Daniely and Shalev-Shwartz.

Timeline:

• 1989–1995. Natarajan, then Ben-David et al. and Haussler–Long: for finite $\mathcal Y$, learnability is equivalent to finite Natarajan dimension, with sample complexity depending on $\log|\mathcal Y|$.
• 2011–2015. Daniely, Sabato, Ben-David and Shalev-Shwartz show that ERM can fail for multiclass problems with many labels. Daniely and Shalev-Shwartz (COLT 2014) introduce the DS dimension, prove that finite DS dimension is necessary for learnability, and ask whether it is sufficient.
• 2022. Brukhim, Carmon, Dinur, Moran, Yehudayoff prove sufficiency, so the DS dimension characterizes multiclass PAC learnability, and show that the Natarajan dimension does not.

Setting

A concept class is a set $\mathcal H\subseteq\mathcal Y^{\mathcal X}$ of functions. For a sequence $S=(x_1,\dots,x_n)$ the projection $\mathcal H|_S\subseteq\mathcal Y^n$ is the set of label words $(h(x_1),\dots,h(x_n))$, $h\in\mathcal H$. A finite non-empty set $B\subseteq\mathcal Y^d$ is a pseudo-cube if every $h\in B$ has, in every coordinate $i$, a neighbour $g\in B$ that differs from $h$ exactly in coordinate $i$. The sequence $S$ is DS-shattered if $\mathcal H|_S$ contains an $n$-dimensional pseudo-cube, and the DS dimension $d_{DS}(\mathcal H)$ is the maximum length of a DS-shattered sequence. The Natarajan dimension $d_N(\mathcal H)\le d_{DS}(\mathcal H)$ is the same with Boolean cubes $\prod_i\{f(i),g(i)\}$, $f(i)\ne g(i)$, in place of pseudo-cubes.

A sample $S\in(\mathcal X\times\mathcal Y)^n$ is $\mathcal H$-realizable if some $h\in\mathcal H$ is consistent with it. An $n\to r$ sample compression scheme for $\mathcal H$ (Littlestone and Warmuth 1986) is a single reconstruction function $\rho:(\mathcal X\times\mathcal Y)^r\to\mathcal Y^{\mathcal X}$ such that every realizable sample of size $n$ contains $r$ of its examples $S'$ with $\rho(S')$ consistent with the whole sample. Logarithms are base $2$ throughout.

Formalization targets

Goal: Theorem 36 (p. 22)

For $\mathcal H$ with $d_{DS}(\mathcal H)=d_{DS}<\infty$ and $d_N(\mathcal H)=d_N$, and all integers $n,t>0$, there is an $n\to r$ sample compression scheme, $r\le n$, with

$$r\le\left(\frac{d_{DS}+t+1}{t+1}(d_{DS}+t)+10^3d_N\log\left(\binom{d_{DS}+t+1}{t+1}\log(2n)\right)\right)\log(2n).$$

Milestones

The scheme combines two components, each with its own chain of results:

• List learning from the DS dimension. Lemma 13 (orientations of out-degree $\le d$ on $\mathcal Y^{d+1}$), Claim 16 (the one-inclusion algorithm is right on some leave-one-out example), Fact 14 (leave-one-out symmetrization), Proposition 32 (a list PAC learner with list size $\binom{d+t}{t}$ and success probability $\frac{t+1}{d+t+1}$), Lemma 39 (an $n\to r_1$ list compression scheme with $r_1\le\frac{d_{DS}+t+1}{t+1}(d_{DS}+t)\log(2n)$ and menu size $\le\binom{d_{DS}+t+1}{t+1}\log(2n)$).
• Learning from a menu via shifting. Claim 22, Corollary 23, Claim 26, Proposition 27 ($\operatorname{avd}\le4d_E$), Corollary 28, Lemma 29 ($d_E\le5d_N\log p$), Lemma 17 (orientations of out-degree $\le20d_N\log p$ on $[p]^n$), Proposition 34 (error $\le20d_N\log(p)/n$ given a $p$-menu), Lemma 40 (an $n\to r_2$ compression scheme given a $p$-menu with $r_2\le10^3d_N\log(p)\log(2n)$).

Significance

Theorem 36 is the algorithmic heart of the characterization: by the standard "compression implies generalization" argument it gives PAC learnability of every class of finite DS dimension, with sample complexity $\tilde O(d_{DS}^{3/2}/\epsilon)$ in the realizable case ($t=\lceil d_{DS}^{1/2}\rceil$), and with the agnostic case following by known reductions. It also exhibits sample compression schemes of size polylogarithmic in $n$ for multiclass classes with infinitely many labels, in contrast to the constant-size schemes known for finite VC classes.

The result is proved in the paper; none of it is formalized. The formalization would produce a machine-checked theory of one-inclusion graphs and their orientations, multiclass shifting, the exponential dimension, list learning, and sample compression schemes for arbitrary label sets. These objects recur throughout learning theory (one-inclusion graphs in optimal PAC learning, shifting in VC theory), so the infrastructure is reusable beyond this mission.

Difficulty

The natural first idea, running empirical risk minimization or bounding the Natarajan dimension, fails: classes with Natarajan dimension $1$ and infinitely many labels can be unlearnable, and ERM can fail even for learnable classes. The DS dimension gives only a weak guarantee: by Claim 16, among $d+1$ leave-one-out runs, one is correct. Turning this into a learner requires a list learner whose menus are still of unbounded total size, and then learning with a menu of size $p$, where the obstacle is controlling one-inclusion graph orientations over $[p]^n$ by the Natarajan dimension. Multiclass shifting does not preserve the average degree (Example 20), so the binary argument breaks down, and a new potential ($\operatorname{avd}'$) and a new dimension ($d_E$) are needed. Lemma 13 for infinite classes needs a compactness argument.

Formalization scope

Lean conventions:

• A class is H : Set (X → Y) with arbitrary types X, Y; sequences and samples are functions on Fin n ($[n]$ is 0-based).
• The DS, Natarajan and exponential dimensions are suprema in ℕ∞, so unbounded families give ⊤; hypotheses are written dsDim H = dDS with dDS : ℕ. A pseudo-cube is required to be finite.
• Logarithms are Real.logb 2. Menu sizes use Set.encard.
• A compression scheme is a reconstruction function fixed before the sample (∃ ρ, ∀ S, ∃ S'); a subsample may repeat and reorder examples. Theorem 36 states $r\le n$ explicitly.
• Orientations of the one-inclusion graph of $V\subseteq\mathcal Y^m$ are maps sending a direction $i$ and a vertex $v$ to the head of the edge of direction $i$ through $v$; the out-degree of $v$ counts directions whose head is not $v$.
• Classes over $[p]$ use labels Fin p; the shifting condition $1\le g(i)\le|e_f|$ becomes $g(i)<|e_f|$.
• The one-inclusion algorithm (Algorithms 1 and 3) is parametrized by a permutation-equivariant choice of minimal orientations, the reading under which the paper's leave-one-out proofs are valid; statements about the algorithm hold for every such choice. Its default output on non-realizable input requires a non-empty label set, assumed in Claim 16 and Propositions 32 and 34. Lemma 40 assumes a non-empty label set because it is false for $\mathcal X\ne\emptyset=\mathcal Y$.
• Distributions are discrete (PMF), and i.i.d. probabilities are sums over $\mathcal Z^m$. The measure-theoretic generality of the paper is not attempted.

A trivial formalization is ruled out by these choices. Placing the reconstruction function after the sample would let it output the consistent hypothesis. A dimension in ℕ defined by sSup would be $0$ for infinite dimension. Pseudo-cubes without finiteness would change the dimension (Example 8).

Contributions welcome: proofs of any milestone, in particular the shifting results of §3 (self-contained combinatorics on finite classes), Fact 14 (pure discrete probability), and Lemma 13; general-purpose lemmas about one-inclusion graphs, orientations and sample compression schemes are reusable by other learning-theory missions.

Selected references

• N. Brukhim, D. Carmon, I. Dinur, S. Moran, A. Yehudayoff, A Characterization of Multiclass Learnability, FOCS 2022; arXiv:2203.01550v1 (2022). https://arxiv.org/abs/2203.01550
• A. Daniely, S. Shalev-Shwartz, Optimal Learners for Multiclass Problems, COLT 2014. https://arxiv.org/abs/1405.2690
• N. Littlestone, M. Warmuth, Relating Data Compression and Learnability, unpublished technical report, University of California, Santa Cruz, 1986 (no stable link).
• D. Haussler, N. Littlestone, M. Warmuth, Predicting {0,1}-Functions on Randomly Drawn Points, Information and Computation 115(2), 1994. https://doi.org/10.1006/inco.1994.1097
• D. Haussler, P. M. Long, A Generalization of Sauer's Lemma, Journal of Combinatorial Theory, Series A 71(2), 1995. https://doi.org/10.1016/0097-3165(95)90006-3
• S. Ben-David, N. Cesa-Bianchi, D. Haussler, P. M. Long, Characterizations of Learnability for Classes of {0,…,n}-Valued Functions, JCSS 50(1), 1995. https://doi.org/10.1006/jcss.1995.1008
• B. K. Natarajan, On Learning Sets and Functions, Machine Learning 4, 1989. https://doi.org/10.1007/BF00114804

Motivation

Least-squares regression fitted by stochastic gradient descent — the least-mean-square (LMS) algorithm — is the basic large-scale learning procedure: each observation is touched once, at a cost linear in the dimension. Classical analyses of stochastic approximation give the rate $O(1/\sqrt n)$ for non-strongly-convex objectives, and $O(1/(\mu n))$ when the objective is $\mu$-strongly convex. For least squares, $\mu$ is the smallest eigenvalue of the input covariance, which in high-dimensional problems is close to zero, so the strongly convex rate is often worse than the non-strongly-convex one.

F. Bach and E. Moulines (arXiv:1306.2119, NeurIPS 2013) showed that for the square loss this dichotomy disappears: averaged LMS with a constant step size reaches the rate $O(1/n)$ with no strong-convexity assumption, and with a constant that does not involve the smallest eigenvalue. Averaging of stochastic approximation iterates goes back to Polyak and Juditsky (SIAM J. Control Optim. 1992), whose guarantees are asymptotic and use decreasing step sizes. The proof technique for the expansion of the noise process is adapted from Aguech, Moulines and Priouret (SIAM J. Control Optim. 2000). This mission formalizes the non-asymptotic bound in expectation (Theorem 1 of the paper) and the chain of lemmas of its Appendix A.

Setting

Let $\mathcal H=\mathbb R^d$ with $d\ge1$, inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. For $a\in\mathcal H$, $a\otimes a$ is the operator $b\mapsto\langle a,b\rangle a$. For self-adjoint operators, $A\preccurlyeq B$ means that $B-A$ is positive semi-definite.

The data are independent and identically distributed pairs $(x_n,z_n)\in\mathcal H\times\mathcal H$, $n\ge1$, with finite second moments. The covariance operator is $H=\mathbb E[x_n\otimes x_n]$, assumed invertible (its eigenvalues may be arbitrarily small). The least-squares objective

$$f(\theta)=\tfrac12\,\mathbb E\big[\langle\theta,x_n\rangle^2-2\langle\theta,z_n\rangle\big]$$

attains its global minimum at $\theta^*$, and $\xi_n=z_n-\langle\theta^*,x_n\rangle x_n$ is the residual. The model need not be well specified: $\mathbb E[\xi_n\mid x_n]$ need not vanish. Two constants $R,\sigma>0$ satisfy

$$\mathbb E[\xi_n\otimes\xi_n]\preccurlyeq\sigma^2H,\qquad \mathbb E\big[\|x_n\|^2x_n\otimes x_n\big]\preccurlyeq R^2H .$$

These are assumptions (A1)–(A6) of §2.1. The LMS recursion with constant step size $\gamma$, started at $\theta_0\in\mathcal H$, is

$$\theta_n=\theta_{n-1}-\gamma\big(\langle\theta_{n-1},x_n\rangle x_n-z_n\big)=(I-\gamma x_n\otimes x_n)\theta_{n-1}+\gamma z_n ,$$

and its average is $\bar\theta_{n-1}=n^{-1}\sum_{k=0}^{n-1}\theta_k$.

Formalization targets

Goal: Theorem 1, Eq. (2)

For every step size $0<\gamma<1/R^2$ and every $n\ge1$,

$$\mathbb E\big[f(\bar\theta_{n-1})-f(\theta^*)\big]\le\frac{1}{2n}\left[\frac{\sigma\sqrt d}{1-\sqrt{\gamma R^2}}+R\|\theta_0-\theta^*\|\frac{1}{\sqrt{\gamma R^2}}\right]^2 .$$

The constants are the paper's. A companion item states the case $\gamma=1/(4R^2)$, where the bound reads $\frac2n\big[\sigma\sqrt d+R\|\theta_0-\theta^*\|\big]^2$.

Milestones (Appendix A)

1. The excess risk is a quadratic form: $f(\theta)-f(\theta^*)=\tfrac12\langle\theta-\theta^*,H(\theta-\theta^*)\rangle$.
2. Consequences of (A6): $\mathbb E\|x_n\|^2\le R^2$, $\operatorname{tr}H\le R^2$, $H\preccurlyeq R^2I$, and $\gamma H\preccurlyeq I$ for $\gamma\le1/R^2$.
3. Lemma 1: for a recursion $\alpha_n=(I-\gamma x_n\otimes x_n)\alpha_{n-1}+\gamma\xi_n$ with martingale-difference noise and $\gamma R^2\le1$,

$$(1-\gamma R^2)\,\mathbb E\langle\bar\alpha_{n-1},H\bar\alpha_{n-1}\rangle+\tfrac{1}{2n\gamma}\mathbb E\|\alpha_n\|^2\le\tfrac{1}{2n\gamma}\|\alpha_0\|^2+\tfrac{\gamma}{n}\textstyle\sum_{k=1}^{n}\mathbb E\|\xi_k\|^2 .$$

4. Lemma 3: $(1-(1-u)^n)^2\le nu$ for $u\in[0,1]$ and $n>0$.
5. Lemma 2: for $\alpha_n=(I-\gamma H)\alpha_{n-1}+\gamma\xi_n$ with $\mathbb E[\xi_n\otimes\xi_n]\preccurlyeq C$, the second-moment bound (13) and

$$\mathbb E\langle\bar\alpha_{n-1},H\bar\alpha_{n-1}\rangle\le\tfrac{1}{n\gamma}\|\alpha_0\|^2+\tfrac1n\operatorname{tr}(CH^{-1}).$$

6. The pathwise decomposition $\theta_n-\theta^*=M^n_1(\theta_0-\theta^*)+\gamma\sum_{k=1}^nM^n_{k+1}\xi_k$ (A.2).
7. The initial-condition bound $\mathbb E\langle\bar\eta_{n-1},H\bar\eta_{n-1}\rangle\le\|\eta_0\|^2/(n\gamma)$ for the noise-free process (A.3).
8. The expansion of the noise process (A.4): the remainder recursion (16), the covariance bound (17) $\mathbb E[\eta^r_{n-1}\otimes\eta^r_{n-1}]\preccurlyeq\gamma^{r+1}R^{2r}\sigma^2I$, the order-$r$ bound $\frac1n\gamma^rR^{2r}d\sigma^2$, the remainder bound $\frac{\gamma^{r+2}\sigma^2R^{2r+4}}{1-\gamma R^2}$, and the noise bound

$$\big(\mathbb E\langle\bar\eta_{n-1},H\bar\eta_{n-1}\rangle\big)^{1/2}\le\frac{\sigma\sqrt d}{\sqrt n}\cdot\frac{1}{1-\sqrt{\gamma R^2}}\quad(\eta_0=0,\ \gamma R^2<1).$$

Significance

The result. Theorem 1 gives a finite-sample, dimension-explicit bound with two terms: a variance term $\sigma^2d/n$, which matches the minimax rate for least-squares regression, and a bias term $R^2\|\theta_0-\theta^*\|^2/(\gamma n)$. Neither involves the smallest eigenvalue of $H$, so the guarantee survives ill-conditioning, which is the regime of high-dimensional learning. The bound is the basis for the paper's later results: the high-probability bound (Theorem 2) and the constant-step algorithm for logistic regression (Theorem 3), whose analysis invokes Theorem 1 for the quadratic approximations.

Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge no part of it has been machine-checked. A formalization yields a reusable layer for linear stochastic approximation in finite dimension: martingale-difference noise in $\mathbb R^d$, second-moment bounds for linear recursions driven by random operators, Loewner-order arguments, and averaging. The lemmas are stated for an abstract filtration and an abstract operator $H$, so they apply beyond this model. The mission also records the corrections the appendix needs (an "$=$" that should be "$\preccurlyeq$" in (13), an index in (16), and the exponent of $\|\eta_0\|$ in A.5).

Difficulty

Two steps resist the naive approach. First, the obvious one-step analysis — expand $\|\theta_n-\theta^*\|^2$ and take expectations — yields the bias part and Lemma 1, but on the noise it gives only $\gamma\sum_k\mathbb E\|\xi_k\|^2/n$, which does not decrease with $n$. The $\sigma^2d/n$ rate requires averaging to cancel the noise, and this cancellation is visible only for the recursion with $x_n\otimes x_n$ replaced by its mean $H$. The random recursion is therefore expanded in powers of $\gamma$ around the mean recursion, and each term $\eta^r$ needs its own covariance bound, by induction on $r$, using the independence of $x_n$ from $\eta^{r}_{n-1}$. Second, the induction relies on Loewner-order bookkeeping: sums of $(I-\gamma H)^{2k}H$ must be bounded uniformly in $n$ without dividing by small eigenvalues.

Formalization scope

The space $\mathcal H$ is EuclideanSpace ℝ (Fin d). Operators are continuous linear maps, and $H^{-1}$ is an explicit two-sided inverse. Observations are indexed from $1$. Averages are $\bar p_{n-1}=n^{-1}\sum_{k=0}^{n-1}p_k$, with $n\ge1$ in every statement that uses them. The covariance operator is defined by its bilinear form, $\langle v,Hw\rangle=\mathbb E[\langle x_1,v\rangle\langle x_1,w\rangle]$. Every Loewner inequality whose sides are expectations is an inequality of quadratic forms (for example $\mathbb E\langle\xi_1,v\rangle^2\le\sigma^2\langle v,Hv\rangle$ for all $v$), which is the same order for self-adjoint operators.

Lean's Bochner integral is $0$ on non-integrable functions, so every moment assumption carries the integrability of its integrand, and every bounded expectation in a conclusion is paired with an integrability conjunct. Without these, a heavy-tailed $x_n$ would satisfy (A6) vacuously and a conclusion could hold through the value $0$; neither formalization is acceptable. Independence is of the pairs $(x_n,z_n)$, not of $x_n$ and $z_n$ separately. (A4) is attainment of the minimum, not a gradient condition.

The following hypotheses are added to the page and disclosed in each item:

• $\gamma>0$ (a step size, and $\sqrt{\gamma R^2}$ is a denominator);
• $n\ge1$;
• the positivity and self-adjointness of $H$ in Lemma 2;
• $\gamma R^2<1$ instead of $\le1$ in the remainder bound, which divides by $1-\gamma R^2$.

A complete development needs:

• conditional expectations of $\mathbb R^d$-valued martingale differences, and the orthogonality of their sums;
• independence of a fresh observation from the past iterates;
• spectral calculus for $(I-\gamma H)^k$;
• Minkowski's inequality in $L^2$.

All of these are reusable for other stochastic-approximation missions. Proofs of any milestone are welcome, as are alternative arguments for the noise bound that avoid the expansion.

Selected references

• F. Bach and E. Moulines, Non-strongly-convex smooth stochastic approximation with convergence rate O(1/n), Advances in Neural Information Processing Systems 26, 2013. https://arxiv.org/abs/1306.2119
• B. T. Polyak and A. B. Juditsky, Acceleration of stochastic approximation by averaging, SIAM Journal on Control and Optimization 30(4), 1992. https://doi.org/10.1137/0330046
• R. Aguech, E. Moulines and P. Priouret, On a perturbation approach for the analysis of stochastic tracking algorithms, SIAM Journal on Control and Optimization 39(3), 2000. https://doi.org/10.1137/S0363012997331639
• F. Bach and E. Moulines, Non-asymptotic analysis of stochastic approximation algorithms for machine learning, Advances in Neural Information Processing Systems 24, 2011. https://hal.science/hal-00608041

Motivation

Many decision problems are solved repeatedly against data that arrive over time: routing traffic, allocating budgets, choosing portfolios or combinatorial structures. Online linear optimization models this. At each round $t = 1, \ldots, T$ a learner picks a decision $x_t$ from a fixed domain $\mathcal K\subseteq\mathbb R^n$, then a reward vector $f_t$ is revealed and the learner earns $f_t\cdot x_t$. Performance is measured by regret, the gap to the best fixed decision in hindsight. When $\mathcal K$ is combinatorial (paths, spanning trees, assignments), the only computationally reasonable access to $\mathcal K$ is a procedure that optimizes a linear function over it, and in practice such procedures are often only approximate.

Follow the Perturbed Leader (FPL), introduced by Hannan (1957) and analysed for linear optimization by Kalai and Vempala (JCSS 2005), uses exactly one call to an exact linear optimizer per round and achieves regret $O(\sqrt T)$ over arbitrary, not necessarily convex, domains. Ben-Tal, Hazan, Koren and Mannor (arXiv:1402.6361, Operations Research 2015) needed a version of FPL that works with an additively approximate linear optimizer, as a building block for oracle-based robust optimization with linearly parametrized uncertainty sets. Their §3.3 analyses this variant and proves Theorem 6, the goal of this mission.

Setting

Fix a dimension $n$, a domain $\mathcal K\subseteq\mathbb R^n$ (arbitrary: not necessarily convex, closed or bounded) and $\epsilon > 0$. An $\epsilon$-approximate linear optimization procedure over $\mathcal K$ is a map $M_\epsilon:\mathbb R^n\to\mathbb R^n$ such that, for every $g\in\mathbb R^n$,

$$M_\epsilon(g)\in\mathcal K \qquad\text{and}\qquad g\cdot M_\epsilon(g)\;\ge\; g\cdot x-\epsilon\quad\text{for all }x\in\mathcal K .$$

Reward vectors $f_1,\ldots,f_T\in\mathbb R^n$ are fixed in advance (an oblivious adversary). Write $f_{1:t}=\sum_{\tau=1}^t f_\tau$, with $f_{1:0}=0$, and $\|v\|_1=\sum_i|v_i|$.

Follow the Approximate Perturbed Leader with parameter $\eta>0$ plays at round $t$

$$x_t = M_\epsilon\big(f_{1:t-1}+p_t\big),\qquad p_t \text{ uniform on the cube } [0,1/\eta]^n .$$

Three scale parameters enter the bound: $D$ bounds the $\ell_1$ diameter of $\mathcal K$, $\|x-y\|_1\le D$ for $x,y\in\mathcal K$; $A$ bounds $\|f_t\|_1$; and $R$ bounds how much each reward varies over the domain, $|f_t\cdot x-f_t\cdot y|\le R$ for $x,y\in\mathcal K$.

Formalization targets

Goal: Theorem 6 (p. 11)

With $\eta=\sqrt{D/(RAT)}$, for every $x^*\in\mathcal K$,

$$\sum_{t=1}^T f_t\cdot x^* - \mathbf E\Big[\sum_{t=1}^T f_t\cdot x_t\Big]\;\le\;2\sqrt{DRAT}+2\epsilon T .$$

The bound for every $\eta$ (proof of Theorem 6, p. 13)

For every $\eta>0$ and $x\in\mathcal K$,

$$\mathbf E\Big[\sum_{t=1}^T f_t\cdot x_t\Big]\;\ge\; f_{1:T}\cdot x-\frac D\eta-\eta RAT-2\epsilon T .$$

Supporting lemmas (pp. 12–13)

• Lemma 7 (approximate be-the-leader): $\sum_{t=1}^T M_\epsilon(f_{1:t})\cdot f_t\ge M_\epsilon(f_{1:T})\cdot f_{1:T}-\epsilon T$.
• Lemma 8 (be the approximate perturbed leader): for $T\ge2$, $p\in[0,1/\eta]^n$ and $x\in\mathcal K$, $\sum_{t=1}^T M_\epsilon(f_{1:t}+p)\cdot f_t\ge f_{1:T}\cdot x-D/\eta-2\epsilon T$.
• Lemma 9 (stability): for $p$ uniform on $[0,1/\eta]^n$, $\mathbf E[M_\epsilon(f_{1:t-1}+p)\cdot f_t]-\mathbf E[M_\epsilon(f_{1:t}+p)\cdot f_t]\ge-\eta RA$.

Significance

Theorem 6 shows that perturbed-leader online linear optimization is robust to additive error in its optimization subroutine: an $\epsilon$-approximate oracle costs only $2\epsilon T$ extra regret, so the average regret is $2\sqrt{DRA/T}+2\epsilon$. This allows the algorithm to be run over domains where exact linear optimization is intractable but a good additive approximation is available, and the paper invokes it as the online-learning primitive of its oracle-based scheme for linearly parametrized uncertainty in §3.2 (that application is not part of this mission). Unlike online gradient methods, it requires no convexity of $\mathcal K$ and no projection.

On the formal side, no regret bound for Follow the Perturbed Leader, exact or approximate, is currently formalized on the platform, and the Kalai–Vempala stability argument (comparing a uniform distribution on a cube with its translate) is a reusable piece of measure theory. The mission's statements are proved on paper; the work here is to formalize those proofs, with one correction to a hypothesis, explained under Formalization scope.

Difficulty

Lemmas 7 and 8 are deterministic and combinatorial. The substance is Lemma 9. It compares the expectations of one bounded function of $M_\epsilon(\cdot)$ under the uniform law on a cube and under its translate by $f_t$. The natural first attempt, a pointwise comparison of $M_\epsilon(f_{1:t-1}+p)$ and $M_\epsilon(f_{1:t}+p)$, fails: an approximate (even an exact) maximizer can jump arbitrarily under an arbitrarily small change of its input, and $M_\epsilon$ is not assumed continuous or even consistent between nearby inputs. Any valid argument must therefore control the two distributions as a whole rather than the decisions point by point, which in the formal development involves Lebesgue measure on $\mathbb R^n$, conditioning on a box and translation invariance.

A second subtlety is that the stability bound depends on how $R$ is read, which is the reason for the correction below.

Formalization scope

Vectors are Fin n → ℝ with dotProduct. All $\ell_1$ quantities are written as $\sum_i|v_i|$, never with the default norm (the sup norm). Rewards are a function f : ℕ → Fin n → ℝ read at $t=1,\ldots,T$, and $f_{1:t}$ is prefixSum f t. The perturbation law is Lebesgue measure conditioned on the cube $[0,1/\eta]^n$ (ProbabilityTheory.cond volume), a probability measure for $\eta>0$. Maxima over $\mathcal K$ are expressed as "for every $x\in\mathcal K$", so neither attainment nor boundedness of $\mathcal K$ is presupposed.

Conventions and deviations, each also stated in the affected item:

1. $R$ is an oscillation bound. The paper takes $R\ge\max_{t,x}|f_t\cdot x|$. With that reading Lemma 9 is false (for $\mathcal K=\{-1,1\}$, the exact maximizer, $f_{1:t-1}=-A$, $f_t=A=R$, $\eta A\le1$, the left side is $-2\eta RA$), and the printed constant in Theorem 6 does not follow. The proof's step "they can differ by at most $R$" is correct when $R\ge|f_t\cdot x-f_t\cdot y|$ for $x,y\in\mathcal K$; Lemma 9, the display and Theorem 6 are stated with that hypothesis. The printed hypothesis implies it with $2R$; for non-negative rewards the two coincide.
2. Expected reward. $\mathbf E[\sum_t f_t\cdot x_t]$ is written as $\sum_t\int f_t\cdot M_\epsilon(f_{1:t-1}+p)\,d\mu_\eta(p)$, which by linearity of expectation is the same for independent or shared perturbations (the paper makes the same observation).
3. Printed typos. In (13) the summand $f_t$ is $f_\tau$ and round $t$ uses $f_{1:t-1}$; in Lemma 8 and the display, $\max_{x}f_{1:t}\cdot x$ means $f_{1:T}$.
4. Added hypotheses. $M_\epsilon$ is measurable (otherwise every expectation would be a Bochner integral of a non-measurable function and equal $0$); an approximate maximizer can always be chosen measurable. $D,R,A>0$ and $T\ge1$ make $\eta=\sqrt{D/(RAT)}$ a positive real. The display is stated for $T\ge1$ (Lemma 8 needs $T\ge2$ as printed; the case $T=1$ also holds).
5. No $O(\cdot)$ appears: all constants are the paper's explicit ones.

A trivializing formalization is ruled out: $M_\epsilon$ must return points of $\mathcal K$ (otherwise $D$ would not bound $\|M_\epsilon(\cdot)-M_\epsilon(\cdot)\|_1$), it must be measurable, and the perturbation law is the normalized uniform distribution, not Lebesgue measure restricted to the cube (which is not a probability measure for $\eta\neq1$).

Needed infrastructure: the overlap estimate for a cube and its translate, $\mathrm{vol}([0,1/\eta]^n\cap(v+[0,1/\eta]^n))\ge(1-\eta\|v\|_1)\,\eta^{-n}$, and the integrability of bounded measurable functions of $M_\epsilon$. Both are reusable for any perturbation-based online-learning analysis; contributions of these as standalone lemmas are welcome.

Selected references

• A. Ben-Tal, E. Hazan, T. Koren, S. Mannor, Oracle-Based Robust Optimization via Online Learning, Operations Research 63(3), 2015; preprint arXiv:1402.6361v1, 2014. https://arxiv.org/abs/1402.6361
• A. Kalai, S. Vempala, Efficient algorithms for online decision problems, Journal of Computer and System Sciences 71(3), 291–307, 2005. https://doi.org/10.1016/j.jcss.2004.10.016
• J. Hannan, Approximation to Bayes risk in repeated play, Contributions to the Theory of Games III, Annals of Mathematics Studies 39, 97–139, 1957.

Motivation

In online convex optimization a decision maker picks points $x_1,x_2,\dots,x_n$ in a convex set $S\subseteq\mathbb R^d$, and after each choice pays $c_t(x_t)$ for a convex cost function $c_t$ chosen in advance by an adversary. Performance is measured by regret: the total cost paid minus the cost of the best fixed point in hindsight. Zinkevich (ICML 2003) showed that projected gradient descent has regret $O(\sqrt n)$ when the whole function $c_t$, or at least its gradient at $x_t$, is revealed after each round.

In many applications only the number $c_t(x_t)$ is observed: a seller sets a price and sees revenue, a router picks a path and sees its delay, an advertiser places a bid and sees the cost. This is the bandit setting. Flaxman, Kalai and McMahan (arXiv:cs/0408007, SODA 2005) gave the first simple algorithm for bandit convex optimization against an oblivious adversary with general bounded convex costs: a randomized gradient descent that estimates the gradient from a single function value, with expected regret $O(n^{5/6})$. The same one-point gradient estimate is the starting point of later work on bandit convex optimization and on zeroth-order (derivative-free) stochastic optimization; see, e.g., Bubeck and Cesa-Bianchi's survey (arXiv:1204.5721, Ch. 6) and Hazan's textbook (arXiv:1909.05207, Ch. 6).

Timeline. Zinkevich (2003): $O(\sqrt n)$ regret with full gradient feedback. Kleinberg (NIPS 2004), independently: $O(n^{3/4})$ bandit regret for Lipschitz costs by a different reduction. Flaxman, Kalai, McMahan (2004/2005): $O(n^{5/6})$ for bounded convex costs and $O(n^{3/4})$ for Lipschitz costs, with one function value per round. Later work (Bubeck, Lee, Eldan 2017 and others) reached $\tilde O(\sqrt n)$ with more complex algorithms.

Setting

Let $\mathbb B=\{x\in\mathbb R^d : |x|\le1\}$ and $\mathbb S=\{x : |x|=1\}$ be the closed unit ball and the unit sphere, $d\ge1$. The feasible set $S$ is closed and convex with

$$r\mathbb B\subseteq S\subseteq R\mathbb B,\qquad r>0 .$$

The costs $c_1,c_2,\dots$ are fixed before play (an oblivious adversary); each is convex on $S$ with $|c_t(x)|\le C$ for $x\in S$, where $C>0$. For $K\subseteq\mathbb R^d$, $P_K(z)$ is the nearest point of $K$ to $z$.

The bandit gradient descent algorithm $\mathrm{BGD}(\alpha,\delta,\nu)$ (Figure 1 of the paper) keeps an iterate $y_t$ with $y_1=0$. At period $t$ it draws a unit vector $u_t$ uniformly from $\mathbb S$, independently of the past, plays

$$x_t=y_t+\delta u_t ,$$

observes only $c_t(x_t)$, and updates

$$y_{t+1}=P_{(1-\alpha)S}\big(y_t-\nu\,c_t(x_t)\,u_t\big).$$

The smoothed cost is $\hat c_t(x)=\mathbb E_{v\in\mathbb B}[c_t(x+\delta v)]$ with $v$ uniform on $\mathbb B$. The expected regret after $n$ rounds is

$$\mathbb E\Big[\sum_{t=1}^n c_t(x_t)\Big]-\min_{x\in S}\sum_{t=1}^n c_t(x).$$

Formalization targets

Goal: Theorem 1 (p. 8)

For every $n\ge(3Rd/2r)^2$, with $\nu=R/(C\sqrt n)$, $\delta=\sqrt[3]{rR^2d^2/(12n)}$ and $\alpha=\sqrt[3]{3Rd/(2r\sqrt n)}$,

$$\mathbb E\Big[\sum_{t=1}^n c_t(x_t)\Big]-\min_{x\in S}\sum_{t=1}^n c_t(x)\le 3Cn^{5/6}\sqrt[3]{\frac{12\,dR}{r}} .$$

The paper prints the constant $3Cn^{5/6}\sqrt[3]{dR/r}$. Its own last step bounds the regret by $a/\delta+b\delta/\alpha+c\alpha$ with $a=RdC\sqrt n$, $b=6Cn/r$, $c=2Cn$, and with the stated $\delta$ and $\alpha$ this equals $3\sqrt[3]{abc}=3Cn^{5/6}\sqrt[3]{12dR/r}$. The goal states the bound the proof establishes.

Milestones

1. Lemma 1 (p. 5): $\mathbb E_{u\in\mathbb S}[f(x+\delta u)u]=\frac\delta d\nabla\hat f(x)$, the one-point gradient estimate.
2. Lemma 2 (p. 6): gradient descent with conditionally unbiased gradient estimates of norm at most $G$ has expected regret at most $RG\sqrt n$ for $\eta=R/(G\sqrt n)$.
3. Observations 1–3 (pp. 7–8): the comparator over $(1-\alpha)S$ is within $2\alpha Cn$ of that over $S$; balls of radius $\alpha r$ around $(1-\alpha)S$ lie in $S$; on $(1-\alpha)S$ the costs satisfy $|c_t(x)-c_t(y)|\le\frac{2C}{\alpha r}|x-y|$.
4. The played points are feasible (p. 8).
5. Regret against the smoothed costs (p. 9): at most $RdC\sqrt n/\delta$.
6. Display (10) (p. 9): regret at most $RdC\sqrt n/\delta+3\delta Ln+2\alpha Cn$ with $L=2C/(\alpha r)$.

Companion items

The tuning identity (p. 9): $a/\delta+b\delta/\alpha+c\alpha=3\sqrt[3]{abc}$ at $\delta=\sqrt[3]{a^2/bc}$, $\alpha=\sqrt[3]{ab/c^2}$, for $a,b,c>0$.

Theorem 2 (p. 9). If each $c_t$ is $L$-Lipschitz on $S$, then with $\nu=R/(C\sqrt n)$, $\delta=n^{-1/4}\sqrt{RdCr/(3(Lr+C))}$, $\alpha=\delta/r$, and $n$ large enough that $\delta<r$,

$$\mathbb E\Big[\sum_{t=1}^n c_t(x_t)\Big]-\min_{x\in S}\sum_{t=1}^n c_t(x)\le 2n^{3/4}\sqrt{3RdC\big(L+C/r\big)} .$$

Significance

The theorem shows that bandit feedback costs only a polynomial factor in regret for arbitrary bounded convex costs, with an algorithm that is gradient descent plus one random perturbation per round. Lemma 1 is the general tool behind it: an unbiased estimate of the gradient of a smoothed function from one function value. It is reused across zeroth-order optimization, bandit learning and stochastic approximation. Lemma 2 is a self-contained regret bound for projected gradient descent with noisy gradients, the shape in which Zinkevich's analysis is most often applied.

The results are proved in the paper and are standard. To the platform's knowledge none of them has a machine-checked proof. Related statements from Bubeck and Cesa-Bianchi's survey, for differentiable Lipschitz losses, are open on the platform, and two earlier formalizations of the textbook versions were disproved because of missing regularity or independence hypotheses. Formalizing this mission produces a checked one-point gradient identity for continuous (not differentiable) functions on the sphere, a measure-theoretic regret bound for stochastic projected gradient descent, and the corrected constant of Theorem 1.

Difficulty

The bandit algorithm itself is simple; the difficulty sits in Lemma 1 and in the measure theory around it. The paper derives Lemma 1 from Stokes' theorem, $\nabla\int_{\delta\mathbb B}f(x+v)\,dv=\int_{\delta\mathbb S}f(x+u)\frac{u}{|u|}\,du$, and the ratio $\delta/d$ of the volume to the surface area of a ball. Mathlib has neither this divergence identity on balls in $\mathbb R^d$ nor the explicit link between its spherical measure and the surface integral needed here. The identity must hold for functions that are merely continuous near the ball, since convex costs need not be differentiable.

The obvious first idea, differentiating under the integral sign in $\hat f(x)=\mathbb E_v[f(x+\delta v)]$, fails because $f$ is not differentiable. The second obvious idea, applying Lemma 1 to $c_t$ as given, fails at the boundary of $S$, where $c_t$ is unconstrained. Lemma 2's conditional expectation $\mathbb E[g_t\mid x_t]$ requires that the direction $u_t$ be independent of the iterate $y_t$, and the integrability and measurability of the played points come from continuity of convex functions in the interior of $S$.

Formalization scope

Points are EuclideanSpace ℝ (Fin d) with $d\ge1$, and rounds are numbered $1,\dots,n$. The costs are functions on $\mathbb R^d$, and no statement assumes anything about them outside $S$: no global convexity, continuity, differentiability or Lipschitz bound. The standing model is part of the goal's hypotheses: $S$ is convex with $r\mathbb B\subseteq S\subseteq R\mathbb B$, the costs are convex on $S$ with values in $[-C,C]$ there, and $C>0$. Additions and conventions:

• $S$ is assumed closed. The paper's projection oracle $P_S(x)=\arg\min_{z\in S}|x-z|$ presupposes that the minimum is attained.
• The directions $u_t$ are measurable, independent, and each uniform on $\mathbb S$ (the published uniformSphere d). Uniform marginals alone are not enough.
• The BGD run is a relation (IsBGDRun) required for every outcome. Projection uses the published predicate IsNearestPoint, and regret the published pseudoRegret, whose minimum is an infimum over the subtype; it is attained in every use here.
• Lemma 1 adds continuity of $f$ on an open set containing $x+\delta\mathbb B$. As printed ("for any function $f$") it is false. The application in Theorem 1 supplies this hypothesis.
• The smoothed-regret and (10) milestones use the strict $\delta<\alpha r$ (the page has $\delta/r\le\alpha$), which keeps every smoothing ball in the interior of $S$. They use $\alpha\le1$ in place of $\alpha<1$; Theorem 1's $\alpha$ equals $1$ at $n=(3Rd/2r)^2$.
• Theorem 2's "for $n$ sufficiently large" is the hypothesis $\delta<r$, the only place the proof uses it.

A formalization that assumed integrability of the costs along the run, assumed differentiable or globally Lipschitz costs, dropped the independence of the directions, or stated $\nabla\hat f$ through Mathlib's gradient (which is $0$ off differentiability) would trivialize or change the result. All of these are ruled out.

Needed infrastructure: the divergence identity for the ball average (Lemma 1), conditional expectation given $\sigma(x_t)$ for vector-valued variables, continuity of convex functions on the interior of a convex set, and nearest-point projection onto closed convex sets. The first two are reusable well beyond this mission. Contributions toward Lemma 1 in particular are welcome.

Selected references

• A. D. Flaxman, A. T. Kalai, H. B. McMahan, Online convex optimization in the bandit setting: gradient descent without a gradient, SODA 2005; arXiv:cs/0408007v1, 2004. https://arxiv.org/abs/cs/0408007
• M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://www.cs.cmu.edu/~maz/publications/ICML03.pdf
• R. Kleinberg, Nearly tight bounds for the continuum-armed bandit problem, NIPS 2004. https://papers.nips.cc/paper/2634-nearly-tight-bounds-for-the-continuum-armed-bandit-problem
• S. Bubeck, N. Cesa-Bianchi, Regret analysis of stochastic and nonstochastic multi-armed bandit problems, Foundations and Trends in ML, 2012. https://arxiv.org/abs/1204.5721
• E. Hazan, Introduction to online convex optimization, 2nd ed., 2019. https://arxiv.org/abs/1909.05207
• S. Bubeck, Y. T. Lee, R. Eldan, Kernel-based methods for bandit convex optimization, STOC 2017. https://arxiv.org/abs/1607.03084