Optimization

Motivation

Many optimization problems in machine learning minimize an average of losses, one loss for each observation. A full gradient step examines every observation, while a stochastic gradient step examines one. The latter is cheaper per step, but its sampled gradient can remain noisy even near the optimum. Section 6.3 of Bubeck's monograph studies stochastic variance reduced gradient descent (SVRG), which periodically computes a full gradient at an anchor point and uses it to correct subsequent sampled gradients. The question for this mission is whether that correction gives a geometric reduction of the expected objective gap at the constants printed in Theorem 6.5.

Bubeck places this method alongside full gradient descent and stochastic gradient descent for finite sums. The section records that earlier stochastic average gradient and dual coordinate ascent methods attain a gradient-computation cost of order $(m+\kappa)\log(1/\varepsilon)$ for the same regime, where $m$ is the number of components and $\kappa$ is a condition number. The target here is the precise SVRG convergence statement in the book, rather than a comparison of implementation costs. The source's discussion on pp. 334–336 gives the context and the algorithm.

Setting

Let $f_1,\ldots,f_m:\mathbb R^n\to\mathbb R$ be differentiable convex functions, with $m\ge1$, and define the finite-sum objective and its gradient by

$$f(x)=\frac1m\sum_{i=1}^m f_i(x),\qquad G(x)=\frac1m\sum_{i=1}^m \nabla f_i(x).$$

Each component is $\beta$-smooth when its gradient is $\beta$-Lipschitz in the Euclidean norm: $\|\nabla f_i(x)-\nabla f_i(z)\|_2\le\beta\|x-z\|_2$ for all $x,z$. The average $f$ is $\alpha$-strongly convex, meaning that for all $x,z$ it lies at least $\frac\alpha2\|z-x\|_2^2$ above its first-order affine approximation at $x$. The constants $\alpha$ and $\beta$ are positive, $x^*$ minimizes $f$ over $\mathbb R^n$, and $\kappa=\beta/\alpha$.

An epoch begins at an anchor $y$. Its first inner iterate is $x_1=y$. For $t=1,\ldots,k$, draw $i_t$ uniformly from $\{1,\ldots,m\}$, independently across steps and epochs, and update

$$x_{t+1}=x_t-\eta\bigl(\nabla f_{i_t}(x_t)-\nabla f_{i_t}(y)+G(y)\bigr).$$

The next anchor is the average $y^+=k^{-1}\sum_{t=1}^k x_t$. In particular, this average uses $x_1$ through $x_k$, while the last updated point $x_{k+1}$ is excluded. Starting from an arbitrary $y^{(1)}$ and repeating the epoch produces $y^{(s+1)}$. The expectation of $f(y^{(s+1)})$ is over all $sk$ sampled indices in the first $s$ epochs.

Formalization targets

Goal: geometric contraction across epochs

Theorem 6.5 sets $\eta=1/(10\beta)$ and $k=20\kappa$ and asserts, for every $s\ge1$,

$$\mathbb E f(y^{(s+1)})-f(x^*) \le 0.9^s\bigl(f(y^{(1)})-f(x^*)\bigr).$$

The epoch length is a count, so the statement takes $k\in\mathbb N$ and explicitly requires $k=20\beta/\alpha$. The goal uses exactly the book's step size, epoch length, and contraction factor.

Milestones: second moments and a single epoch

Lemma 6.4 bounds $\mathbb E_i\|\nabla f_i(x)-\nabla f_i(x^*)\|_2^2$ by $2\beta(f(x)-f(x^*))$. Equation (6.3) bounds the second moment of the corrected sampled direction by the objective gaps at the current point and the anchor. Equation (6.2), the unbiased-direction display, and the one-step display express how that direction changes squared distance to $x^*$. The later display on p. 338 bounds one epoch for any positive step size with $2\beta\eta<1$. Finally, equation (6.1) substitutes the stated constants to obtain the factor $0.9$ for one epoch. These seven source claims form the milestone list in reading order.

Significance

The theorem gives an explicit accuracy guarantee after a specified number of epochs: an initial gap $D$ falls below $0.9^sD$ in expectation. Because each epoch uses a full gradient at its anchor as well as sampled component gradients, the result makes clear which quantity contracts and which operations are counted. It is a concrete linear-rate statement for a method whose individual stochastic gradients need not approach zero at the optimum. Bubeck, §6.3 discusses this issue when introducing the correction term.

The mathematical result is already proved in the monograph. The remaining task is to produce machine-checked proofs of its precise finite-sum model, the single-index estimates, the epoch inequality, and the full repeated-epoch guarantee. The mission drafts those statements and definitions; no proof is claimed for the open theorem items. The finite uniform-average representation and the separation between a conditional one-step average and the full multi-epoch average can be reused in other finite-sum stochastic algorithms.

Difficulty

The sampled component gradient $\nabla f_{i_t}(x_t)$ need not be small when $x_t$ is near $x^*$, so a bound using only its norm does not yield the desired fixed-step contraction. The correction $-\nabla f_{i_t}(y)+G(y)$ has mean zero relative to the full gradient at the current iterate, but its second moment still depends on both $x_t$ and $y$. The proof must control those two gaps while respecting the fact that $x_t$ depends on earlier samples. A single-index estimate with $x_t$ held fixed and an expectation over complete sample histories are different statements; confusing them would make the goal weaker or false.

Formalization scope

The carrier is EuclideanSpace ℝ (Fin n) with its usual inner product and norm. The Fin m components and every sample array are finite. A real-valued uniform average is an ordinary finite sum divided by the number of arrays, and $m\ge1$ and $k\ge1$ prevent an empty average. Independent uniform sampling is represented by averaging over every function from step positions to component indices. The multi-epoch sample space has one such block for every epoch. There are no integrals or measurability side conditions.

The component assumptions include differentiability with an explicit gradient map, convexity on all of $\mathbb R^n$, and the book's gradient-Lipschitz version of smoothness. Strong convexity is imposed on the average objective alone, using the published OnlineConvexOpt.ConvexBasics.StronglyConvexOn definition on the whole space. The book's standing notation assumes a minimizing $x^*$ exists; this is explicit. Positivity of $\alpha$ and $\beta$, and integrality of $20\beta/\alpha$, make the displayed divisions and epoch length meaningful. The general epoch bound also requires $0<\eta$ and $2\beta\eta<1$. Dimension zero is allowed: the theorem remains a statement about the unique point of $\mathbb R^0$ and its zero objective gap.

The direction always contains the sampled difference $\nabla f_{i_t}(x_t)-\nabla f_{i_t}(y)$ and the full anchor gradient $G(y)$. Replacing that direction with $G(x_t)$ would define gradient descent and would not satisfy this mission's algorithm. Contributions are welcome for the finite averaging identities, the component-gradient estimate, the conditional one-step calculation, the epoch inequality, and the induction across epochs.

Selected references

• Sébastien Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4), 2015, pp. 231–358. arXiv:1405.4980v2
• Rie Johnson and Tong Zhang, Accelerating Stochastic Gradient Descent using Predictive Variance Reduction, Advances in Neural Information Processing Systems 26 (NIPS), 2013 (the origin of SVRG, cited by Bubeck on p. 335). https://proceedings.neurips.cc/paper/2013/hash/ac1dd209cbcc5e5d1c6e28598e8cbbe8-Abstract.html

Motivation

Many optimization problems in statistics and machine learning ask to minimize an expected loss $f(x)=\mathbb E_\xi\,\ell(x,\xi)$, or an average $f(x)=\frac1m\sum_{i=1}^m f_i(x)$ over a large data set. Exact gradients of such an $f$ are unavailable or too expensive, but unbiased random estimates are cheap: the gradient of the loss at one sample, or of one randomly chosen summand. The observation that first-order methods still make progress when the gradients are only correct on average goes back to Robbins and Monro (1951) and underlies stochastic gradient descent.

Chapter 6 of S. Bubeck, Convex Optimization: Algorithms and Complexity (2015), studies this setting through stochastic mirror descent (S-MD). Its Section 6.1 shows that in the non-smooth case a noisy oracle costs nothing in rate. Section 6.2 asks what smoothness buys: for a general stochastic oracle it cannot buy acceleration, but Theorem 6.3, whose proof the book takes from Dekel, Gilad-Bachrach, Shamir and Xiao (2012), shows that the rate splits into a noise term of order $1/\sqrt t$ and a smoothness term of order $1/t$. The book uses it to justify mini-batch SGD. This mission is the fourteenth of a series that formalizes the section capstones of the book.

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$. Gradients are linear forms $g$ on $E$, the value of $g$ at $v$ is written $g^\top v$, and the dual norm is $\|g\|_*=\sup_{\|v\|\le1}g^\top v$. Let $\mathcal X\subseteq E$ be compact and convex.

A mirror map is a function $\Phi$ on an open convex set $\mathcal D$ with $\mathcal X\subseteq\overline{\mathcal D}$ and $\mathcal X\cap\mathcal D\ne\emptyset$. It is strictly convex and differentiable on $\mathcal D$, its gradient $\nabla\Phi$ takes every value, and $\|\nabla\Phi(x)\|_*\to\infty$ as $x$ approaches the boundary of $\mathcal D$. Its Bregman divergence is $D_\Phi(x,y)=\Phi(x)-\Phi(y)-\nabla\Phi(y)^\top(x-y)$. The map is 1-strongly convex on $\mathcal X\cap\mathcal D$ if $D_\Phi(y,x)\ge\frac12\|x-y\|^2$ there. A function $f$ is $\beta$-smooth on $\mathcal X$ if $\|\nabla f(x)-\nabla f(y)\|_*\le\beta\|x-y\|$ for $x,y\in\mathcal X$.

A stochastic oracle returns, at a query point $x$, a random linear form $\tilde g(x)$. When the query point is itself random, the book requires the conditional expectation given the query point, $\mathbb E(\tilde g(x)\mid x)$, to be a subgradient of $f$ at $x$. In the smooth case it requires $\mathbb E(\tilde g(x)\mid x)=\nabla f(x)$ together with the variance bound $\mathbb E(\|\tilde g(x)-\nabla f(x)\|_*^2\mid x)\le\sigma^2$.

S-MD with step $\gamma$ starts at $x_1\in\operatorname{argmin}_{\mathcal X\cap\mathcal D}\Phi$ and, writing $\tilde g_s=\tilde g(x_s)$, iterates

$$x_{s+1}\in\operatorname*{argmin}_{x\in\mathcal X\cap\mathcal D}\ \gamma\,\tilde g_s^\top x+D_\Phi(x,x_s).$$

Let $R^2\ge\sup_{x\in\mathcal X\cap\mathcal D}\Phi(x)-\Phi(x_1)$, and let $x^*$ minimize $f$ on $\mathcal X$.

Formalization targets

Goal: Theorem 6.3

Let $f$ be convex and $\beta$-smooth, and let the oracle have variance at most $\sigma^2$. Then for every $t\ge1$, S-MD with step $1/(\beta+1/\eta)$ and $\eta=\frac R\sigma\sqrt{2/t}$ satisfies

$$\mathbb E\,f\Big(\frac1t\sum_{s=1}^t x_{s+1}\Big)-f(x^*)\le R\sigma\sqrt{\frac2t}+\frac{\beta R^2}{t}.$$

Milestones (the proof's four displays)

For points $x_s,x_{s+1}\in\mathcal X\cap\mathcal D$ and $\eta>0$, the smoothness step is

$$f(x_{s+1})-f(x_s)\le\tilde g_s^\top(x_{s+1}-x_s)+\tfrac\eta2\|\nabla f(x_s)-\tilde g_s\|_*^2+(\beta+1/\eta)D_\Phi(x_{s+1},x_s).$$

If $x_{s+1}$ is the S-MD step, the mirror step is

$$\tfrac{1}{\beta+1/\eta}\tilde g_s^\top(x_{s+1}-x^*)\le D_\Phi(x^*,x_s)-D_\Phi(x^*,x_{s+1})-D_\Phi(x_{s+1},x_s).$$

Combining the two gives a pathwise bound on $f(x_{s+1})$ with the cross term $(\tilde g_s-\nabla f(x_s))^\top(x^*-x_s)$. Taking expectations gives the expected one-step bound

$$\mathbb Ef(x_{s+1})-f(x^*)\le(\beta+1/\eta)\,\mathbb E\big(D_\Phi(x^*,x_s)-D_\Phi(x^*,x_{s+1})\big)+\frac{\eta\sigma^2}{2}.$$

Companion: Theorem 6.1 and (4.10)

For a convex $f$ with $\mathbb E(\|\tilde g(x)\|_*^2\mid x)\le B^2$, S-MD with $\eta=\frac RB\sqrt{2/t}$ satisfies

$$\mathbb E\,f\Big(\frac1t\sum_{s=1}^tx_s\Big)-\min_{\mathcal X}f\le RB\sqrt{2/t}.$$

This rests on the deterministic regret bound (4.10) of mirror descent along arbitrary vectors $g_s$:

$$\sum_{s\le t}g_s^\top(x_s-x)\le\frac{R^2}{\eta}+\frac{\eta}{2\rho}\sum_{s\le t}\|g_s\|_*^2.$$

Significance

Theorem 6.3 says exactly how much smoothness helps under noise. As $\sigma\to0$ it recovers the $\beta R^2/t$ rate of deterministic smooth optimization. For large $t$ the noise term $R\sigma\sqrt{2/t}$ dominates; the book notes, citing Tsybakov (2003), that smoothness brings no acceleration for a general stochastic oracle. Averaging $m$ independent oracle answers divides the variance by $m$, so the theorem quantifies the benefit of mini-batches: the noise term shrinks by $\sqrt m$ while the smoothness term is unchanged. Theorem 6.1 is the matching non-smooth statement and the template for stochastic subgradient methods in any norm.

These are classical, proved results. None of them is known to be formalized in Lean, and the platform has no stochastic mirror descent statement. Its stochastic gradient items cover the Euclidean strongly convex case and the non-convex gradient-norm case. This mission adds a reusable stochastic-oracle layer in an arbitrary norm, with conditional expectations given random query points, on top of the mirror-map layer of Chapter 4.

Difficulty

The deterministic steps are short manipulations of Bregman divergences. The difficulty is in the passage to expectations. The query point $x_s$ is random, so unbiasedness enters only through the conditional expectation given $x_s$. Making the cross term vanish requires pulling the $\sigma(x_s)$-measurable vector $x^*-x_s$ out of a conditional expectation of a dual-valued random variable. Every expectation also has to exist. When $\nabla\Phi$ blows up at the boundary of $\mathcal D$, the Bregman terms $D_\Phi(x^*,x_s)$ are not bounded a priori, and their integrability has to be derived from the recursion. A further obstacle is that the minimizer $x^*$ may lie on the boundary of $\mathcal D$, where $\Phi$ is not part of the book's data. Treating $\mathbb E$ informally, or assuming $x^*\in\mathcal D$, skips exactly these points.

Formalization scope

• Spaces and gradients. $E$ is a finite-dimensional real normed space. Gradients are explicit maps Φ' f' : E → (E →L[ℝ] ℝ), $g^\top v$ is g v, and $\|\cdot\|_*$ is the operator norm. $\beta$-smoothness is stated with derivatives relative to $\mathcal X$. $\Phi$ is a total function, constrained only by the mirror-map axioms on $\mathcal D$.
• Runs and oracle. S-MD is a run predicate. For every outcome, $x_1$ minimizes $\Phi$ on $\mathcal X\cap\mathcal D$, and $x_{s+1}$ is some minimizer of the step objective. The oracle is a predicate on the random sequences $(x_s,\tilde g_s)$: each $x_s$ is measurable, and the conditional expectations are taken given $\sigma(x_s)$. Every conditioned quantity is integrable.
• Conclusions. Every bound on an expectation also asserts integrability. Without it, the Lean integral of a non-integrable function is $0$ and the bound could hold trivially.
• Standing assumptions. The book's $R^2=\sup(\Phi-\Phi(x_1))$ is replaced by any upper bound $R^2$. The minimizer $x^*\in\mathcal X$ exists (p. 242). $\mathcal X$ is compact and convex (Chapter 4), and convex functions are closed (p. 236).
• Positivity side conditions. $R,\sigma,B>0$ and $t\ge1$ make the step sizes and bounds defined, and $\beta\ge0$.

A variance hypothesis stated only at deterministic points would not control the random iterates, and is not used. Run predicates that let $x_{s+1}$ be an arbitrary point of $\mathcal X\cap\mathcal D$ would make the theorems false, and are not used either.

A complete development needs: first-order optimality over a convex set, the three-point identity of Bregman divergences, the descent lemma in an arbitrary norm, and continuity of the gradient of a differentiable convex function. On the probability side it needs pull-out and conditional Jensen properties for dual-valued conditional expectations. The probability layer is reusable for every stochastic first-order method in the book, including SVRG and random coordinate descent. Proofs of the milestones are welcome, and so are general lemmas about conditional expectations of continuous-linear-map-valued random variables.

Selected references

• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2, https://arxiv.org/abs/1405.4980 (Chapter 6, pp. 329–333; Chapter 4, pp. 297–307).
• O. Dekel, R. Gilad-Bachrach, O. Shamir, L. Xiao, Optimal distributed online prediction using mini-batches, Journal of Machine Learning Research 13:165–202, 2012. https://jmlr.org/papers/v13/dekel12a.html
• H. Robbins, S. Monro, A stochastic approximation method, Annals of Mathematical Statistics 22(3):400–407, 1951. https://doi.org/10.1214/aoms/1177729586
• A. Beck, M. Teboulle, Mirror descent and nonlinear projected subgradient methods for convex optimization, Operations Research Letters 31(3):167–175, 2003. https://doi.org/10.1016/S0167-6377(02)00231-6
• A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM Journal on Optimization 19(4):1574–1609, 2009. https://doi.org/10.1137/070704277

Motivation

Newton's method is the basic second-order method of continuous optimization: at the current point it replaces the objective by its second-order Taylor model and jumps to the stationary point of that model. Its defining property is speed near a nondegenerate minimum, where the error is squared at every step, so that the number of correct digits roughly doubles per iteration. This local behaviour is what makes Newton's method the inner engine of interior point methods, the polynomial-time algorithms for linear, conic and general convex programming (Nesterov and Nemirovski, 1994). In S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015; arXiv:1405.4980v2), §5.3.2 recalls the traditional local analysis of Newton's method, Theorem 5.3, before turning to the affine-invariant self-concordance analysis used for interior point methods. This mission formalizes that theorem and the four steps of its proof.

Setting

Let $\mathbb R^n$ carry the Euclidean norm $\|\cdot\|$, and write $\|A\|$ for the operator norm of a linear map $A:\mathbb R^n\to\mathbb R^n$, so that $\|Ax\|\le\|A\|\,\|x\|$. Let $f:\mathbb R^n\to\mathbb R$ be a $C^2$ function, with gradient $\nabla f(x)\in\mathbb R^n$ and Hessian $\nabla^2 f(x)$, a linear map $\mathbb R^n\to\mathbb R^n$ (the derivative of the gradient map). For a real number $c$, $A\succeq cI_n$ means $\langle Av,v\rangle\ge c\|v\|^2$ for all $v\in\mathbb R^n$.

The Hessian is $M$-Lipschitz if $\|\nabla^2 f(x)-\nabla^2 f(y)\|\le M\|x-y\|$ for all $x,y\in\mathbb R^n$.

Newton's method starts at $x_0\in\mathbb R^n$ and iterates, for $k\ge0$,

$$x_{k+1}=x_k-[\nabla^2 f(x_k)]^{-1}\nabla f(x_k).$$

A point $x^*$ is a local minimum of $f$ if $f(x^*)\le f(x)$ for all $x$ in a neighbourhood of $x^*$; it has strictly positive Hessian if $\nabla^2 f(x^*)\succeq\mu I_n$ for some $\mu>0$.

Formalization targets

Goal: Theorem 5.3 (p. 320)

Assume the Hessian of $f$ is $M$-Lipschitz, $M>0$, and $x^*$ is a local minimum with $\nabla^2 f(x^*)\succeq\mu I_n$, $\mu>0$. If $\|x_0-x^*\|\le\mu/(2M)$, then Newton's method from $x_0$ is well defined (every Hessian along the iterates is invertible, so the sequence exists and is unique) and

$$\|x_{k+1}-x^*\|\le\frac M\mu\,\|x_k-x^*\|^2\quad(k\ge0),\qquad x_k\to x^*.$$

Milestones (p. 321, the steps of the proof)

1. The integral formula $\int_0^1\nabla^2 f(x+sh)\,h\,ds=\nabla f(x+h)-\nabla f(x)$.
2. The error representation of one Newton step, $x_{k+1}-x^*=[\nabla^2 f(x_k)]^{-1}\int_0^1[\nabla^2 f(x_k)-\nabla^2 f(x^*+s(x_k-x^*))](x_k-x^*)\,ds$.
3. The Lipschitz bound $\int_0^1\|\nabla^2 f(x_k)-\nabla^2 f(x^*+s(x_k-x^*))\|\,ds\le\frac M2\|x_k-x^*\|$.
4. The Hessian lower bound $\nabla^2 f(x_k)\succeq(\mu-M\|x_k-x^*\|)I_n\succeq\frac\mu2I_n$ when $\|x_k-x^*\|\le\mu/(2M)$.

Significance

The theorem gives a quantitative basin of quadratic convergence: an explicit radius $\mu/(2M)$, depending only on the curvature at the minimum and the Lipschitz constant of the Hessian, inside which Newton's method needs only $O(\log\log(1/\varepsilon))$ iterations to reach accuracy $\varepsilon$. It is the classical statement whose shortcomings (dependence on a choice of norm, constants that change under linear changes of variables) motivate the self-concordance theory of the following subsections, and it is the local convergence result invoked whenever a damped or globalized Newton scheme is shown to enter its quadratic phase.

On the formal side, Mathlib has the calculus this needs (Fréchet derivatives, interval integrals of vector-valued maps, operator norms) but no convergence theorem for multivariate Newton's method for minimization. A formal proof produces reusable pieces: the integral form of the mean value theorem for gradients, the stability of a positive-definite lower bound under Lipschitz perturbations, and an inverse-operator norm bound from a quadratic-form lower bound. The result itself is classical and fully proved in the literature; what is open here is its machine-checked proof in this form.

Difficulty

The individual inequalities are short, but the argument is an induction in which well-definedness and the rate are proved together: the Hessian at $x_k$ is invertible only because $x_k$ is still in the ball of radius $\mu/(2M)$, and $x_{k+1}$ stays in that ball only because of the rate. A proof that first assumes the sequence exists and then bounds it is circular. The proof also passes between two kinds of control on the Hessian, a lower bound on its quadratic form and an operator-norm bound on its inverse, and the second is only meaningful once invertibility is established. Finally, the integral manipulations need integrability of the maps $s\mapsto\nabla^2 f(x^*+s(x_k-x^*))(x_k-x^*)$, which comes from the continuity of the Hessian.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The gradient and Hessian are explicit maps $g:\mathbb R^n\to\mathbb R^n$ and $H:\mathbb R^n\to(\mathbb R^n\to_L\mathbb R^n)$ with ContDiff ℝ 2 f, HasGradientAt f (g x) x and HasFDerivAt g (H x) x at every point; the norm on $H(x)$ is Mathlib's operator norm, as on the page. $A\succeq cI_n$ is the quadratic-form inequality. A Newton run is a sequence $x:\mathbb N\to\mathbb R^n$ indexed from $0$ satisfying the linear system $\nabla^2 f(x_k)(x_k-x_{k+1})=\nabla f(x_k)$; no inverse of a possibly singular operator appears in any hypothesis, and "well defined" is a conclusion: a unique run exists from $x_0$ and every Hessian along it is bijective. The rate and $x_k\to x^*$ are asserted for every run. The error representation is stated with both sides multiplied by $\nabla^2 f(x_k)$, which is equivalent to the printed form once the Hessian is invertible. Milestones 3 and 4 use only the Lipschitz property and are stated for any Lipschitz map $H$.

Added hypothesis: $M>0$ (the radius $\mu/(2M)$ divides by $M$; with $M=0$, Lean's convention $\mu/0=0$ would collapse the hypothesis to $x_0=x^*$). Convexity of $f$ is not assumed, as on the page; $x^*$ is a local minimum and $\nabla f(x^*)=0$ is derived, not assumed. Encoding the Newton step with Lean's inverse (which returns $0$ on singular maps), or replacing $\nabla^2 f(x^*)\succeq\mu I_n$ by mere invertibility, would change the theorem and is ruled out.

A complete development needs the fundamental theorem of calculus for $C^1$ vector-valued maps along segments, Hessian-based quadratic-form estimates, and operator-norm bounds for inverses; all are reusable for the analysis of damped Newton, cubic regularization and interior point methods. Proofs of the milestones independently of the goal are welcome.

Selected references

• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2, §5.3.2, Theorem 5.3, pp. 320–321.
• Yu. Nesterov and A. Nemirovski, Interior-Point Polynomial Algorithms in Convex Programming, SIAM Studies in Applied Mathematics 13, 1994. doi:10.1137/1.9781611970791
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004, Theorem 1.2.5. doi:10.1007/978-1-4419-8853-9

Why accelerated rates matter

First-order methods, which query only function values and gradients, are the workhorse of large-scale optimization in machine learning, signal processing and operations research, because each step costs little more than one gradient evaluation. For a function that is both strongly convex and smooth, plain gradient descent converges geometrically, but the number of steps needed to reach accuracy $\varepsilon$ scales with the condition number $\kappa$ of the problem. In 1983 Nesterov showed that a gradient method with a carefully chosen momentum term needs a number of steps proportional to $\sqrt\kappa$ instead, and that this is optimal for black-box first-order methods. On ill-conditioned problems, where $\kappa$ is in the thousands or millions, the difference between $\kappa$ and $\sqrt\kappa$ is the difference between practical and impractical.

This mission is the tenth of a series formalizing S. Bubeck's monograph Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015; arXiv:1405.4980v2). It covers §3.7.1, the smooth and strongly convex case of Nesterov's accelerated gradient descent, and its main result, Theorem 3.18.

Setting

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

• $f$ is $\beta$-smooth if its gradient is $\beta$-Lipschitz: $\|\nabla f(x)-\nabla f(y)\|\le\beta\|x-y\|$ for all $x,y$.
• $f$ is $\alpha$-strongly convex ($\alpha>0$) if for all $x,y$

$$f(y)\ge f(x)+\nabla f(x)^\top(y-x)+\frac\alpha2\|y-x\|^2 .$$

• The condition number is $\kappa=\beta/\alpha$; for $n\ge1$ one always has $\kappa\ge1$.
• $x^*$ denotes a minimizer of $f$ on $\mathbb R^n$.

Nesterov's accelerated gradient descent starts at an arbitrary point $x_1=y_1$ and iterates, for $t\ge1$,

$$y_{t+1}=x_t-\frac1\beta\nabla f(x_t),\qquad x_{t+1}=\Big(1+\frac{\sqrt\kappa-1}{\sqrt\kappa+1}\Big)y_{t+1}-\frac{\sqrt\kappa-1}{\sqrt\kappa+1}\,y_t .$$

The point $y_{t+1}$ is a gradient step from $x_t$, and $x_{t+1}$ moves beyond $y_{t+1}$ in the direction $y_{t+1}-y_t$ by the fixed momentum factor $(\sqrt\kappa-1)/(\sqrt\kappa+1)$.

The analysis in the book uses auxiliary quadratic functions $\Phi_s$ (an estimate sequence), defined from the points $x_s$ by

$$\Phi_1(x)=f(x_1)+\frac\alpha2\|x-x_1\|^2,\qquad \Phi_{s+1}(x)=\Big(1-\frac1{\sqrt\kappa}\Big)\Phi_s(x)+\frac1{\sqrt\kappa}\Big(f(x_s)+\nabla f(x_s)^\top(x-x_s)+\frac\alpha2\|x-x_s\|^2\Big),$$

together with their centres $v_s$ (with $v_1=x_1$ and the recursion (3.21) of the book) and their minimum values $\Phi^*_s$.

Formalization targets

Goal: Theorem 3.18

For every run of the method and every $t\ge1$,

$$f(y_t)-f(x^*)\le\frac{\alpha+\beta}2\,\|x_1-x^*\|^2\exp\Big(-\frac{t-1}{\sqrt\kappa}\Big).$$

Milestones, from the book's proof

1. (3.18): $\Phi_{s+1}(x)\le f(x)+(1-1/\sqrt\kappa)^s(\Phi_1(x)-f(x))$ for all $x$.
2. (3.19): $f(y_s)\le\min_{x\in\mathbb R^n}\Phi_s(x)$.
3. The geometric rate: $f(y_t)-f(x^*)\le\frac{\alpha+\beta}2\|x_1-x^*\|^2(1-1/\sqrt\kappa)^{t-1}$.
4. The form $\Phi_s(x)=\Phi^*_s+\frac\alpha2\|x-v_s\|^2$ with $v_s$ given by (3.21).
5. The identity (3.22) for $\Phi^*_{s+1}$.
6. The inequality (3.20), the inductive step of (3.19).
7. The coupling $v_s-x_s=\sqrt\kappa\,(x_s-y_s)$.

The geometric form in milestone 3 is slightly stronger than the goal, which follows from $1-u\le e^{-u}$.

Significance

Theorem 3.18 gives $\varepsilon$-accuracy after $O(\sqrt\kappa\log(1/\varepsilon))$ gradient evaluations. Projected gradient descent with step $1/\beta$ on the same class contracts only at the rate $\exp(-t/\kappa)$ (Theorem 3.10 of the book). The lower bound of Theorem 3.15 shows that no black-box first-order method can do better than $((\sqrt\kappa-1)/(\sqrt\kappa+1))^{2(t-1)}$, so the accelerated rate is optimal up to constants. The estimate-sequence argument is the template for many later accelerated methods: proximal, stochastic and variance-reduced variants such as Katyusha, and accelerated coordinate descent.

The result is classical and fully proved on paper. No machine-checked proof of the accelerated rate for strongly convex smooth functions is known to exist in Lean's Mathlib. This mission produces one, with the estimate sequence $\Phi_s$, its centres and its minimum values as reusable objects, and with every algebraic identity of the book's proof stated separately.

Difficulty

The algorithm is two lines, but its analysis is not a one-step contraction: neither $\|x_t-x^*\|$ nor $f(y_t)-f(x^*)$ decreases by the factor $1-1/\sqrt\kappa$ at every step. A Lyapunov argument for gradient descent, applied directly to $y_t$, gives only the rate $1-1/\kappa$. The book obtains the rate through the auxiliary functions $\Phi_s$. The inequality (3.18) is easy, but (3.19), that the minimum of $\Phi_s$ never drops below $f(y_s)$, depends on the exact choice of the momentum factor. It holds only through the identity $v_s-x_s=\sqrt\kappa(x_s-y_s)$, which ties the centre of $\Phi_s$ to the iterates. Formally, the obstacles are the bookkeeping of the recursive quadratics on $\mathbb R^n$ and the algebra in $\sqrt\kappa$, $1/\sqrt\kappa$ and $1/(\alpha\sqrt\kappa)=\sqrt\kappa/\beta$.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The gradient is an explicit map g with HasGradientAt f (g x) x at every point, which is part of the smoothness predicate IsBetaSmooth f g β. Strong convexity is the published definition OnlineConvexOpt.ConvexBasics.StronglyConvexOn Set.univ f g α, which is the book's (3.13).
• A run of the method is a predicate IsNesterovSCRun g α β x y on two sequences indexed from $1$, with $x_1=y_1$ arbitrary. Every theorem holds for every run, that is, every starting point.
• $\kappa$ is kappa α β = β / α. All theorems assume $\alpha>0$ and $\beta>0$. The second is implied by the other hypotheses for $n\ge1$; no hypothesis $\alpha\le\beta$ is added.
• The existence of a minimizer $x^*$ is the book's standing assumption, written as a hypothesis.
• $\Phi_s$, $v_s$ and $\Phi^*_s=\Phi_s(v_s)$ are explicit recursive definitions. The book's $\Phi^*_s=\min\Phi_s$ is recovered by milestone 4, and no real infimum is used. The minimum in (3.19) is stated as $f(y_s)\le\Phi_s(x)$ for every $x$.
• The identities of milestones 4, 5 and 7 are algebraic and are stated without convexity or smoothness, for arbitrary sequences or runs.
• Ruled out as trivializing: a run predicate that drops $x_1=y_1$ breaks (3.19) at $s=1$ and is not used. A minimum value $\Phi^*_s$ defined through (3.22) would make that identity a tautology, so $\Phi^*_s$ is defined as a value of $\Phi_s$.
• The definitions are local to the namespace ConvexOptAlg.NesterovStrong. β-smoothness duplicates the predicate of other missions of the series and will be merged afterwards. Contributions welcome: proofs of the milestones, and general lemmas on quadratics $z\mapsto c+\frac\alpha2\|z-v\|^2$ that the algebraic milestones need.

Selected references

• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2, §3.7.1, Theorem 3.18, pp. 290–293.
• Y. Nesterov, A method of solving a convex programming problem with convergence rate O(1/k²), Soviet Mathematics Doklady 27:372–376, 1983.
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. doi:10.1007/978-1-4419-8853-9

Motivation

Minimizing a convex function $f:\mathbb R^n\to\mathbb R$ whose gradient is Lipschitz is the basic problem of first-order optimization, and it is the regime in which most large-scale methods of machine learning, signal processing and operations research are analysed. The natural method, gradient descent, reaches accuracy $\varepsilon$ after $O(1/\varepsilon)$ gradient evaluations. In 1983 Nesterov showed that a method using the same oracle, but combining the current and the previous iterate, reaches accuracy $\varepsilon$ after only $O(1/\sqrt\varepsilon)$ evaluations, and that no method using only gradient information can do better by more than a constant factor. This accelerated gradient descent and its proximal variants (FISTA) are now the default fast first-order methods for smooth and composite convex problems.

This mission formalizes the accelerated rate as presented in S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015; arXiv:1405.4980v2), §3.7.2, Theorem 3.19, whose proof follows Beck and Teboulle (2009).

Timeline.

• 1983: Nesterov introduces the accelerated method with rate $O(1/t^2)$ for convex functions with Lipschitz gradient (Soviet Math. Dokl. 27).
• 1983: Nemirovski and Yudin's black-box lower bounds show that $\Omega(1/t^2)$ is the best possible rate for this class (Theorem 3.14 of the book gives $3\beta\|x_1-x^*\|^2/(32(t+1)^2)$).
• 2009: Beck and Teboulle's FISTA extends the method, with the same step sequence $\lambda_t$, to composite problems with a simple nonsmooth term (SIAM J. Imaging Sci. 2(1)).
• 2008: Tseng gives a unified treatment with simpler step sizes (manuscript).

Setting

Let $\mathbb R^n$ carry the Euclidean inner product $x^\top y$ and norm $\|\cdot\|$. A differentiable function $f:\mathbb R^n\to\mathbb R$ is β-smooth if its gradient is $\beta$-Lipschitz:

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

Assume $f$ is convex and $\beta$-smooth with $\beta>0$, and let $x^*$ be a minimizer of $f$.

Define the step sequences $\lambda_0=0$,

$$\lambda_t=\frac{1+\sqrt{1+4\lambda_{t-1}^2}}{2}\quad(t\ge1),\qquad\gamma_t=\frac{1-\lambda_t}{\lambda_{t+1}}.$$

Then $\lambda_1=1$, $\lambda_t\ge1$ for $t\ge1$, and $\gamma_t\le0$. Nesterov's accelerated gradient descent for the smooth case starts from an arbitrary point $x_1=y_1$ and sets, for $t\ge1$,

$$y_{t+1}=x_t-\frac1\beta\nabla f(x_t),\qquad x_{t+1}=(1-\gamma_t)\,y_{t+1}+\gamma_t\,y_t.$$

The primary sequence $(y_t)$ consists of gradient steps of length $1/\beta$; the sequence $(x_t)$, at which the gradient is queried, moves past $y_{t+1}$ away from $y_t$ (since $\gamma_t\le0$). Write $\delta_t=f(y_t)-f(x^*)$ for the optimality gap.

Formalization targets

Goal: Theorem 3.19

For every run of the method and every $t\ge1$,

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

The constant $2$ and the exponent $2$ are those printed in the book.

Milestones

In the order of the book's proof (pp. 294–295):

1. Lemma 3.6, unconstrained (p. 270): $f(x-\tfrac1\beta\nabla f(x))-f(y)\le\nabla f(x)^\top(x-y)-\tfrac1{2\beta}\|\nabla f(x)\|^2$ for all $x,y$.
2. (3.23): $f(y_{s+1})-f(y_s)\le\beta(x_s-y_{s+1})^\top(x_s-y_s)-\tfrac\beta2\|x_s-y_{s+1}\|^2$.
3. (3.24): $f(y_{s+1})-f(x^*)\le\beta(x_s-y_{s+1})^\top(x_s-x^*)-\tfrac\beta2\|x_s-y_{s+1}\|^2$.
4. The λ identity: $\lambda_{s-1}^2=\lambda_s^2-\lambda_s$ for $s\ge1$.
5. (3.25): $\lambda_s^2\delta_{s+1}-\lambda_{s-1}^2\delta_s\le\tfrac\beta2\bigl(\|\lambda_sx_s-(\lambda_s-1)y_s-x^*\|^2-\|\lambda_sy_{s+1}-(\lambda_s-1)y_s-x^*\|^2\bigr)$.
6. (3.26): $\lambda_{s+1}x_{s+1}-(\lambda_{s+1}-1)y_{s+1}=\lambda_sy_{s+1}-(\lambda_s-1)y_s$.
7. Telescoped bound: $\delta_t\le\frac{\beta}{2\lambda_{t-1}^2}\|u_1\|^2$ for $t\ge2$, with $u_1=\lambda_1x_1-(\lambda_1-1)y_1-x^*$.
8. Growth of λ: $\lambda_{t-1}\ge t/2$ for $t\ge2$.

Significance

The result. Theorem 3.19 is the upper half of the statement that first-order methods on smooth convex functions have complexity $\Theta(\sqrt{\beta\|x_1-x^*\|^2/\varepsilon})$: together with the black-box lower bound of Theorem 3.14 it shows that the accelerated method is optimal up to a constant factor, while plain gradient descent (Theorem 3.3, rate $2\beta\|x_1-x^*\|^2/(t-1)$) is not. The same potential-function argument, with the gradient step replaced by a proximal step, yields the rate of FISTA for composite objectives, and the identity $\lambda_{s-1}^2=\lambda_s^2-\lambda_s$ is the algebraic core of most later analyses of accelerated and momentum methods.

Formalizing it. The theorem is classical and fully proved on paper. What this mission adds is a machine-checked proof of the $O(1/t^2)$ rate for the exact step sequence of the book, with every intermediate inequality of the proof stated separately so that each can be closed and reused. A Lean development of accelerated gradient descent with this rate is not, to our knowledge, in Mathlib.

Difficulty

The rate does not follow from monotone decrease of $f(y_t)$, which is the engine of the analysis of plain gradient descent: the accelerated iterates are not monotone, and no single-step inequality on $\delta_t$ alone gives $1/t^2$. The proof instead tracks a weighted potential $\lambda_{s-1}^2\delta_s+\frac\beta2\|u_s\|^2$ and needs three exact algebraic coincidences: the identity $\lambda_{s-1}^2=\lambda_s^2-\lambda_s$, the completion of a square $2a^\top b-\|a\|^2=\|b\|^2-\|b-a\|^2$, and the rewriting (3.26) of the update rule, which makes consecutive potentials match exactly. In Lean the work is in this bookkeeping (vector identities in an inner-product space, a real recursion with square roots, and a telescoping sum indexed from $1$), not in any deep analytic fact.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n); $x^\top y$ is ⟪x, y⟫_ℝ.
• The gradient is an explicit map $g$ with HasGradientAt f (g x) x for every $x$; β-smoothness is the Lipschitz bound on $g$ (not the quadratic upper bound (3.4), which is a consequence). Convexity is ConvexOn ℝ Set.univ f.
• $\lambda$ is a real sequence defined by recursion on $\mathbb N$ with $\lambda_0=0$; $\gamma_t=(1-\lambda_t)/\lambda_{t+1}$ never divides by zero because $\lambda_{t+1}\ge1$.
• A run is a predicate on two sequences $x,y:\mathbb N\to\mathbb R^n$, indexed from $1$ as in the book; index $0$ is unconstrained. Every theorem quantifies over all runs.
• Standing assumptions: $x^*$ is a minimizer of $f$ (book, p. 242); $\beta>0$ (implicit in the step $1/\beta$) is a stated hypothesis.
• The page prints the update as $x_{t+1}=(1-\gamma_s)y_{t+1}+\gamma_ty_t$; the formalization uses $\gamma_t$ in both places, as the proof's (3.26) requires. A run predicate with a fixed coefficient $\gamma_s$ would describe a different (non-accelerated) method and is ruled out.
• The goal is stated for all $t\ge1$, including $t=1$, which the printed proof does not cover but which follows from (3.4). The growth bound $\lambda_{t-1}\ge t/2$ is stated for $t\ge2$, since $\lambda_0=0$. The telescoping display prints $\delta_s^2$ for $\delta_s$; the formalization uses $\delta_s$.

Contributions of every kind are welcome: proofs of the λ facts and of (3.26) are pure algebra; (3.23)–(3.25) need the descent lemma for β-smooth functions and first-order convexity, both of which are reusable well beyond this mission.

Selected references

• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980
• Y. Nesterov, A method of solving a convex programming problem with convergence rate O(1/k²), Soviet Mathematics Doklady 27:372–376, 1983. mathnet
• A. Beck, M. Teboulle, A fast iterative shrinkage-thresholding algorithm for linear inverse problems, SIAM J. Imaging Sciences 2(1):183–202, 2009. doi:10.1137/080716542
• P. Tseng, On accelerated proximal gradient methods for convex-concave optimization, manuscript, 2008. pdf
• A. Nemirovski, D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.

Why lower bounds for first-order methods

Upper bounds for an optimization method say how fast it converges; oracle complexity lower bounds say how fast any method of a given kind can possibly converge. Chapter 3 of S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning 8(3–4), 2015, arXiv:1405.4980) proves upper bounds for subgradient descent on Lipschitz functions and for gradient methods on smooth functions. Section 3.5 (Lower bounds, pp. 279–283) shows that these rates cannot be improved by more than a numerical constant, as long as the number of queries is smaller than the dimension. For smooth convex functions the matching lower bound is what identifies Nesterov's accelerated gradient descent, with its $1/t^2$ rate, as an optimal method.

Timeline. The lower bounds first appeared in A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization (Wiley, 1983). The presentation followed by the book, with an explicit tridiagonal quadratic as the hard instance and the "span of past gradients" restriction on the method, is that of Y. Nesterov, Introductory Lectures on Convex Optimization (Kluwer, 2004), §2.1.2. Nesterov's accelerated method (1983) attains the matching upper bound.

Setting

Work in $\mathbb R^n$ with the Euclidean inner product $x^\top y$, coordinates $x(1),\dots,x(n)$, canonical basis $e_1,\dots,e_n$ and balls $\mathrm B_2(R)=\{x:\|x\|\le R\}$. A first-order oracle for $f$ answers a query $x$ with a subgradient $g\in\partial f(x)$ (the gradient when $f$ is differentiable). A black-box procedure maps the history $(x_1,g_1,\dots,x_t,g_t)$ to the next query $x_{t+1}$. Section 3.5 restricts attention to procedures with

$$x_1=0,\qquad x_{t+1}\in\mathrm{Span}(g_1,\dots,g_t)\quad(t\ge0), \tag{3.15}$$

which covers gradient descent, its accelerated variants and conjugate gradient. A function is $\beta$-smooth if its gradient is $\beta$-Lipschitz; $L$-Lipschitz on $\mathcal X$ if every subgradient at every point of $\mathcal X$ has norm at most $L$; $\alpha$-strongly convex if $x\mapsto f(x)-\frac\alpha2\|x\|^2$ is convex.

The hard smooth instance uses, for $k\le n$, the symmetric tridiagonal matrix $A_k$ with entries $2$ on the first $k$ diagonal positions and $-1$ on the neighbouring off-diagonal positions of the leading $k\times k$ block, zero elsewhere, and the quadratics

$$f_k(x)=\frac\beta8x^\top A_kx-\frac\beta4x^\top e_1 ,\qquad f_k^*=\inf_{x\in\mathbb R^n}f_k(x).$$

Formalization targets

Goal: Theorem 3.14 (p. 282)

For $1\le t\le\frac{n-1}2$ and $\beta>0$ there are a $\beta$-smooth convex $f$ and a minimizer $x^*$ such that every procedure satisfying (3.15) has

$$\min_{1\le s\le t}f(x_s)-f(x^*)\ \ge\ \frac{3\beta}{32}\,\frac{\|x_1-x^*\|^2}{(t+1)^2}.$$

The constant $3/32$ is the book's.

Milestones (proof of Theorem 3.14, pp. 282–283)

1. $0\preceq A_k\preceq4I_n$, through $x^\top A_kx=x(1)^2+x(k)^2+\sum_{i=1}^{k-1}(x(i)-x(i+1))^2$.
2. For $f=f_{2t+1}$ and any procedure satisfying (3.15), $x_s\in\mathrm{Span}(e_1,\dots,e_{s-1})$; hence $f(x_s)=f_s(x_s)$ for $s\le t$.
3. $x_k^*(i)=1-\frac i{k+1}$ solves $A_kx=e_1$, minimizes $f_k$, and $f_k^*=-\frac\beta8\bigl(1-\frac1{k+1}\bigr)$.
4. $\|x_k^*\|^2\le\frac{k+1}3$.
5. $f_t^*-f_{2t+1}^*=\frac\beta8\bigl(\frac1{t+1}-\frac1{2t+2}\bigr)\ge\frac{3\beta}{32}\frac{\|x^*_{2t+1}\|^2}{(t+1)^2}$.

Companion: Theorem 3.13 (p. 280)

For $1\le t\le n$ and $L,R>0$ there are a convex $f$, $L$-Lipschitz on $\mathrm B_2(R)$, and a first-order oracle for it such that every procedure satisfying (3.15) has $\min_{s\le t}f(x_s)-\min_{\mathrm B_2(R)}f\ge\frac{RL}{2(1+\sqrt t)}$; and for $\alpha>0$ there are an $\alpha$-strongly convex $f$, $L$-Lipschitz on $\mathrm B_2(\frac L{2\alpha})$, and an oracle with gap at least $\frac{L^2}{8\alpha t}$ over that ball.

Significance

The upper bounds of Chapter 3 (projected subgradient descent at rate $RL/\sqrt t$, accelerated gradient descent at rate $\beta\|x_1-x^*\|^2/t^2$) become optimal statements only through these lower bounds: no method in the class (3.15) can be faster by more than a constant factor while $t$ is below the dimension. The restriction to $t\lesssim n$ is necessary, since Chapter 2's cutting-plane methods converge exponentially once the number of queries exceeds the dimension.

The results are classical and proved. Formalizing them yields machine-checked versions of the quadratic-form computation for the tridiagonal matrix, of the Krylov-type support argument under (3.15), and of the explicit minimizer of $f_k$, each reusable in other lower-bound arguments (Theorem 3.15 in $\ell_2$, lower bounds for strongly convex smooth functions, conjugate gradient analyses). The platform held no formal statement of these oracle lower bounds when this mission was drafted.

Difficulty

Each analytic step is elementary; the difficulty is in the bookkeeping. The span argument is an induction that must track, at each step, that the gradient of a tridiagonal quadratic at a vector supported on the first $s-1$ coordinates is supported on the first $s$, and that the span hypothesis transfers this to the next query. The minimizer computation requires solving $A_kx=e_1$ on the leading block and showing that the coordinates beyond $k$ do not affect $f_k$. A natural first attempt, choosing the hard function after seeing the procedure, proves a much weaker statement and is excluded by the quantifier order: the function is fixed first and must defeat every procedure.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). Coordinates in Lean are 0-based; the definitions provide the book's 1-based coordinate coord x i and basis vector basisVec n i, and the matrix tridiag n k translates book index $i$ to Fin n index $i-1$. The query sequence starts at index $1$. The oracle is a fixed map $g$, so (3.15) reads $x_{t+1}\in\mathrm{Span}(g(x_1),\dots,g(x_t))$ with $x_1=0$. In Theorem 3.14 the oracle is the gradient, given as a map with HasGradientAt everywhere; $\beta$-smoothness is the Lipschitz bound on that map. In Theorem 3.13 the oracle is part of what is constructed, because the book's proof uses a specific "resisting" subgradient selection and the claim fails for an arbitrary one.

Committed conventions, each stated in the item's Formalization Note: the minimum over $1\le s\le t$ is the bound for every such $s$, and $t\ge1$ is required; $t\le(n-1)/2$ is $2t+1\le n$; the minimizer $x^*$ is existentially chosen together with $f$ (the hard function has many minimizers when $2t+1<n$, and the bound is false for some of them); the minimum over a ball is the bound against every point of the ball; $f_k^*$ is the real infimum, asserted to be attained.

A formalization that let the function depend on the procedure, dropped $x_1=0$, or took the span over gradients at points other than the queries would state a different and weaker theorem; the statements here keep $f$ (and the oracle) before the universally quantified procedure.

Infrastructure needed: quadratic forms of explicit matrices on EuclideanSpace, gradients of quadratics, and span/support lemmas for EuclideanSpace.single-type vectors. Contributions of proofs for any milestone, and of the strongly convex $\ell_2$ lower bound (Theorem 3.15, not included here), are welcome.

Selected references

• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. https://arxiv.org/abs/1405.4980
• A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9