Convex Optimization

Log-concave functions are the meeting point of convex analysis and probability: densities of Gaussian, exponential, uniform and Wishart distributions are all log-concave, and countless facts of applied probability flow from one structural theorem — integrating out variables preserves log-concavity. This mission builds the convex-analysis spine of Boyd & Vandenberghe's Convex Optimization (Chapters 2–3) — separation and supporting hyperplanes, dual cones, the first- and second-order differential characterizations of convexity, Fenchel conjugacy — and climbs to Prékopa's theorem via the Prékopa–Leindler inequality, a landmark of Brunn–Minkowski theory absent from Mathlib.

The Karush–Kuhn–Tucker conditions are the central result of convex optimization: for a convex differentiable problem satisfying Slater's condition, a point is optimal exactly when primal feasibility, dual feasibility, complementary slackness and Lagrangian stationarity hold. This mission formalizes Chapters 4–5 of Boyd & Vandenberghe end to end — the first-order optimality criterion, concavity of the Lagrange dual, weak duality, Slater's strong-duality theorem with dual attainment (via the separating-hyperplane argument of §5.3.2), the saddle-point characterization, sensitivity bounds and Pareto scalarization — culminating in the full KKT characterization.

Every full-dimensional convex body is sandwiched between an ellipsoid and its $n$-fold dilation: shrinking the minimum-volume covering (Löwner–John) ellipsoid $\mathcal{E}$ about its centre $x_0$ by the factor $1/n$ lands inside the body,

and the factor $n$ is tight on simplices. This rounding theorem underlies the ellipsoid method, John's theorem on the Banach–Mazur distance to the Euclidean ball, and much of modern convex geometry. The mission formalizes §8.4 of Boyd & Vandenberghe for polytopes $C = \operatorname{conv}\{x_1,\dots,x_m\}$, exactly as the book proves it: existence and uniqueness of the extremal ellipsoid, the KKT identities at the normalized optimum ($\sum_i \lambda_i x_i x_i^{T} = I$, $\sum_i \lambda_i x_i = 0$, $\sum_i \lambda_i = n$), the convex-combination step that produces the $1/n$ ball, and affine invariance.

The classical convergence theory of smooth convex minimization. For a function that is $m$-strongly convex and $M$-smooth ($mI \preceq \nabla^2 f(x) \preceq MI$), gradient descent converges linearly, while Newton's method exhibits its famous two phases: a damped phase in which every backtracking step decreases the objective by a fixed amount $\gamma$, and a quadratically convergent phase in which the scaled gradient norm squares at each step, $\tfrac{L}{2m^2}\lVert \nabla f(x^{+})\rVert_2 \le \bigl(\tfrac{L}{2m^2}\lVert \nabla f(x)\rVert_2\bigr)^2$. Together they give the iteration count of B&V (9.36),

with $L$ the Lipschitz constant of the Hessian and $\alpha,\beta$ the backtracking parameters. This mission formalizes Chapters 9–10 of Boyd & Vandenberghe with every constant exactly as printed — a quantitative theory entirely absent from Mathlib.

Two quadratic functions can be compared losslessly. The S-procedure says that, when the constraint is strictly feasible, the implication

holds if and only if a single nonnegative multiplier certifies it as a matrix inequality, $\lambda \begin{bmatrix} F_1 & g_1 \\ g_1^{T} & h_1\end{bmatrix} \succeq \begin{bmatrix} F_2 & g_2 \\ g_2^{T} & h_2\end{bmatrix}$ for some $\lambda \ge 0$. It is a cornerstone of control theory, trust-region methods and robust optimization, and a rare case in which a nonconvex problem has zero duality gap. The route runs through the theory this mission builds from Boyd & Vandenberghe §5.8–5.9 and Appendix B: strong alternatives for convex inequality systems, cone-program strong duality under a generalized Slater condition, semidefinite programming duality, the LMI theorems of alternatives, and the hidden convexity of the joint range of two quadratic forms.

Why do interior-point methods solve convex programs in $O(\sqrt{m}\log(1/\varepsilon))$ Newton steps? Nesterov and Nemirovskii's answer is self-concordance: a convex function whose third derivative is controlled by its second, $|\varphi'''(t)| \le 2\,\varphi''(t)^{3/2}$ along every line, admits a Newton analysis with absolute constants and no condition number — and the logarithmic barrier is self-concordant. This mission formalizes §9.6 and Chapter 11 of Boyd & Vandenberghe: the self-concordance calculus, the Newton-decrement analysis, the duality gap $m/t$ along the central path, the per-centering work bound $m(\mu - 1 - \log\mu)/\gamma + c$, and the crown result — with the aggressive schedule $\mu = 1 + 1/\sqrt{m}$ the barrier method reaches duality gap $\varepsilon$ after

centering steps, each of uniformly bounded Newton cost.

Motivation

Many convex optimization problems in machine learning and statistics have objectives that are convex but not differentiable: hinge losses, $\ell_1$ penalties, maxima of finitely many affine functions, and the dual functions of Lagrangian relaxations. Methods that rely on gradients do not apply to them directly, while cutting-plane methods such as the ellipsoid method pay a price that grows with the dimension. The projected subgradient method replaces the gradient by an arbitrary subgradient and restores feasibility by a Euclidean projection. Its guarantee depends on the dimension only through two constants, a radius $R$ and a Lipschitz constant $L$. This is the reason it, and its descendants (mirror descent, stochastic gradient descent, online gradient descent), are the standard tools for large-scale nonsmooth problems.

The rate analysed here goes back to the subgradient methods of Shor and Polyak in the 1960s and 1970s and to the lower bounds of Nemirovski and Yudin (1983). The book follows the presentation of Nesterov, Introductory Lectures on Convex Optimization (2004). The strongly convex variant with weights proportional to $s$ is from Lacoste-Julien, Schmidt and Bach (2012).

This mission is the third of a series formalizing S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning, 2015), and covers the preamble of Chapter 3, Section 3.1 and Section 3.4.1.

Setting

Let $\mathbb R^n$ carry the Euclidean inner product $x^\top y$ and norm $\|\cdot\|$. Let $\mathcal X\subseteq\mathbb R^n$ be compact and convex, and let $f$ be a convex function on $\mathcal X$ with a minimizer $x^*\in\mathcal X$.

A vector $g$ is a subgradient of $f$ at $x\in\mathcal X$ if $f(x)-f(y)\le g^\top(x-y)$ for every $y\in\mathcal X$. The set of subgradients at $x$ is written $\partial f(x)$. The projection $\Pi_{\mathcal X}(y)$ of a point $y\in\mathbb R^n$ is the point of $\mathcal X$ nearest to $y$.

Fix step sizes $\eta_s>0$. Projected subgradient descent starts at some $x_1\in\mathcal X$ and iterates, for $s\ge1$,

Any subgradient may be chosen at each step. In Section 3.1 the step is constant, $\eta_s=\eta$. The set $\mathcal X$ lies in the Euclidean ball of radius $R$ centred at $x_1$, and the subgradients have norm at most $L$.

A function $f$ is $\alpha$-strongly convex on $\mathcal X$ if $f(x)-f(y)\le g^\top(x-y)-\frac{\alpha}{2}\|x-y\|^2$ for all $x,y\in\mathcal X$ and $g\in\partial f(x)$.

Formalization targets

Goal: Theorem 3.2

For every horizon $t\ge1$, projected subgradient descent with the constant step $\eta=R/(L\sqrt t)$ satisfies

Milestones

1. Lemma 3.1. For $x\in\mathcal X$ and $y\in\mathbb R^n$: $(\Pi_{\mathcal X}(y)-x)^\top(\Pi_{\mathcal X}(y)-y)\le0$, already on the platform as a published theorem. The mission also states its consequence

2. The per-step inequality in the proof of Theorem 3.2:

3. The summed inequality for any constant step $\eta>0$:

Companion: Theorem 3.9

If $f$ is $\alpha$-strongly convex and its subgradients are bounded by $L$, then with $\eta_s=2/(\alpha(s+1))$,

Significance

Theorem 3.2 gives an oracle complexity of $O(R^2L^2/\varepsilon^2)$ for reaching an $\varepsilon$-optimal point, independent of the ambient dimension. Section 3.5 of the book shows this rate is unimprovable for black-box first-order methods once the dimension is large. Theorem 3.9 shows how strong convexity improves the rate to $O(1/t)$, with the averaging weights changed from uniform to linear. These two bounds are the reference points against which the rest of Chapter 3 and Chapters 4 to 6 (smooth, accelerated, mirror, stochastic methods) are measured.

The results are classical and their proofs are short. Formalizing them produces a reusable, machine-checked account of the basic projected first-order step: the projection inequality, the one-step distance recursion, and the telescoping argument with Jensen's inequality for averaged iterates. To our knowledge, no machine-checked proof of the averaged-iterate bound for the projected subgradient method exists in Mathlib. Related platform items cover other algorithms or other averaging schemes.

Difficulty

The arithmetic is elementary, and the obvious argument works. The care is in the bookkeeping. The projection must be shown not to increase the distance to $x^*$, which needs convexity of $\mathcal X$ and the variational characterization of the nearest point. The sum must telescope with a horizon-dependent constant step. Jensen's inequality must be applied to a finite convex combination of points of $\mathcal X$, which requires showing that the average lies in $\mathcal X$. In Theorem 3.9 the step sizes and the averaging weights are coupled, so neither can be changed independently. In Lean, the iterates are indexed from $1$ with natural-number horizons, and the bounds involve $\sqrt t$, so these casts need care.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The iterates are sequences ℕ → EuclideanSpace ℝ (Fin n) with the first iterate at index $1$. The projection is the published relation OnlineConvexOpt.FirstOrder.IsMetricProjection ($x_{s+1}\in\mathcal X$ is a nearest point to $y_{s+1}$). Subgradients are taken relative to $\mathcal X$ (Definition 1.2). A run is a predicate on the steps $s=1,\dots,t$, and every theorem holds for all runs, that is, for every choice of subgradients. Compactness and convexity of $\mathcal X$, convexity of $f$ on $\mathcal X$ and the existence of the minimizer $x^*$ are the book's standing assumptions and appear as hypotheses. $R>0$, $L>0$ and $\alpha>0$ are explicit, because Lean's division by zero would otherwise turn the step size into a junk value.

The book assumes $\|g\|\le L$ for every subgradient at every point of $\mathcal X$. With subgradients relative to a compact $\mathcal X$, that assumption can never hold at a boundary point, since every outward normal can be added to a subgradient. Stated that way the theorems would be vacuous. The mission therefore assumes the bound only for the subgradients $g_1,\dots,g_t$ that the run uses. This is a weaker hypothesis and gives a stronger, non-vacuous statement. Bounding only these subgradients is a deliberate choice, not a trivialization: the bound still constrains every quantity the conclusion depends on.

Contributions welcome: proofs of the four inequalities and of the two rates, and a reusable lemma that the convex combination of finitely many points of a convex set lies in the set, together with Jensen's inequality in the form used here.

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
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• A. Nemirovski and D. Yudin, Problem Complexity and Method Efficiency in Optimization, Wiley, 1983.
• S. Lacoste-Julien, M. Schmidt and F. Bach, A simpler approach to obtaining an O(1/t) convergence rate for the projected stochastic subgradient method, 2012. https://arxiv.org/abs/1212.2002
• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer, 1985. https://doi.org/10.1007/978-3-642-82118-9

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:

• 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

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$

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

Many optimization problems in statistics, machine learning and operations research ask to minimize a smooth convex function over a simple convex set: a box, a ball, a simplex, a cone of positive semidefinite matrices. Projected gradient descent is the most basic first-order method for such problems. It takes a gradient step and then returns to the feasible set by Euclidean projection. Its cost per iteration is one gradient evaluation and one projection, independent of the dimension apart from the cost of manipulating vectors, which is why it remains a workhorse in very high dimension.

This mission is the fifth in a series formalizing S. Bubeck, Convex Optimization: Algorithms and Complexity (Foundations and Trends in Machine Learning 8(3–4), 2015; arXiv:1405.4980). Chapter 3 of the monograph treats "dimension-free" convex optimization. Its §3.2 first proves that gradient descent on a convex $\beta$-smooth function on $\mathbb R^n$ has rate $O(\beta\|x_1-x^*\|^2/t)$ (Theorem 3.3, the subject of mission IV), and then turns to the constrained case, which is the subject of this mission. The analysis follows Nesterov's Introductory Lectures on Convex Optimization (2004).

Setting

Write $x^\top y$ for the Euclidean inner product on $\mathbb R^n$ and $\|\cdot\|$ for the Euclidean norm. The constraint set $\mathcal X\subseteq\mathbb R^n$ is compact and convex; this is the standing assumption of Chapter 3. The Euclidean projection of $y\in\mathbb R^n$ onto $\mathcal X$ is

which exists and is unique for a nonempty closed convex set.

A differentiable function $f:\mathbb R^n\to\mathbb R$ is $\beta$-smooth on $\mathcal X$ if its gradient is $\beta$-Lipschitz there:

It is $\alpha$-strongly convex on $\mathcal X$ if $f(x)-f(y)\le\nabla f(x)^\top(x-y)-\frac\alpha2\|x-y\|^2$ for $x,y\in\mathcal X$. A minimizer $x^*\in\mathcal X$ of $f$ over $\mathcal X$ is assumed to exist, as everywhere in the monograph.

Projected gradient descent with step size $\eta=1/\beta$ starts at $x_1\in\mathcal X$ and iterates

For a point $x$ with projected step $x^+=\Pi_{\mathcal X}\bigl(x-\frac1\beta\nabla f(x)\bigr)$, the gradient mapping is $g_{\mathcal X}(x)=\beta(x-x^+)$. Without constraints it equals $\nabla f(x)$.

Formalization targets

Goal: Theorem 3.7 (p. 270)

For $f$ convex and $\beta$-smooth on $\mathcal X$, projected gradient descent with $\eta=1/\beta$ satisfies, for every $t\ge1$,

Milestones

1. Lemma 3.1 (p. 263): for $x\in\mathcal X$ and $y\in\mathbb R^n$, $(\Pi_{\mathcal X}(y)-x)^\top(\Pi_{\mathcal X}(y)-y)\le0$, and hence $\|\Pi_{\mathcal X}(y)-x\|^2+\|y-\Pi_{\mathcal X}(y)\|^2\le\|y-x\|^2$. The first claim is an already proved platform theorem.
2. (3.7) (p. 270): $\nabla f(x)^\top(x^+-y)\le g_{\mathcal X}(x)^\top(x^+-y)$ for $y\in\mathcal X$.
3. Lemma 3.6 (p. 270): for $x,y\in\mathcal X$,

4. Descent and gap (pp. 270–271): $f(x_{s+1})-f(x_s)\le-\frac1{2\beta}\|g_{\mathcal X}(x_s)\|^2$ and $f(x_{s+1})-f(x^*)\le\|g_{\mathcal X}(x_s)\|\,\|x_s-x^*\|$.
5. Distances decrease (p. 271): $\|x_{s+1}-x^*\|\le\|x_s-x^*\|$.
6. Recursion and induction (p. 271): with $\delta_s=f(x_s)-f(x^*)$, $\delta_{s+1}\le\delta_s-\frac{1}{2\beta\|x_1-x^*\|^2}\delta_{s+1}^2$, and an induction on this recursion gives the bound of Theorem 3.7.

Companion: Theorem 3.10 (p. 278)

If $f$ is in addition $\alpha$-strongly convex on $\mathcal X$, with condition number $\kappa=\beta/\alpha$, then the strengthened Lemma 3.6, display (3.14), gives for every $t\ge0$

Significance

Theorem 3.7 shows that a constraint set with a cheap projection costs nothing in the order of convergence: the $O(\beta\|x_1-x^*\|^2/t)$ rate of unconstrained gradient descent survives, with a constant that depends on $f(x_1)-f(x^*)$. Lemma 3.6 is the reusable part. It isolates the gradient mapping as the quantity that measures progress under constraints, and the same inequality, with a strong-convexity term added, gives the linear rate of Theorem 3.10. It is also the starting point of the analysis of proximal gradient methods for composite objectives.

All of these results are classical and proved in the textbook. As far as a search of the platform shows, none of them is formalized there. A related platform theorem on constrained gradient descent for well-conditioned functions (from Hazan's Introduction to Online Convex Optimization) bounds function values with a different exponent. It is not Theorem 3.10, which bounds distances with rate $\exp(-t/\kappa)$. This mission adds machine-checked statements of the constrained analysis in Bubeck's formulation, with the book's constants. The definitions of $\beta$-smoothness on a set, the gradient mapping and the run predicate can be reused by later missions on accelerated and proximal methods.

Difficulty

The obvious attempt is to copy the unconstrained proof, which rests on the descent inequality $f(x-\frac1\beta\nabla f(x))\le f(x)-\frac1{2\beta}\|\nabla f(x)\|^2$. That inequality fails under constraints: the projection can cut the step short, so the decrease in $f$ is not controlled by $\|\nabla f(x)\|$. At a boundary minimizer, for instance, $\nabla f(x^*)\neq0$ while no step makes progress. The proof has to replace the gradient by the gradient mapping throughout. It also has to show separately that the iterates do not move away from $x^*$, a fact that came for free without constraints from co-coercivity of the gradient (display (3.6)).

The closing induction is not routine either. The step from $s$ to $s+1$ works only from $s=2$ on, and the step from $1$ to $2$ needs a direct computation that uses the term $f(x_1)-f(x^*)$ in the numerator.

Formalization scope

• Space. $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), and $x^\top y$ is ⟪x, y⟫_ℝ.
• Constraint set and minimizer. Every statement assumes $\mathcal X$ compact (IsCompact X) and convex (Convex ℝ X), the standing assumption of Chapter 3. Every statement about a run assumes a minimizer $x^*\in\mathcal X$ with $f(x^*)\le f(y)$ for all $y\in\mathcal X$, the monograph's standing assumption.
• Gradient. The gradient is an explicit map g with HasGradientAt f (g x) x at every point of $\mathbb R^n$, so $\nabla f(x)$ is defined at boundary points of $\mathcal X$. $\beta$-smoothness on $\mathcal X$ (IsBetaSmoothOn X f g β) asks this together with $\beta\ge0$ and the Lipschitz bound on $\mathcal X$ only. It is not the quadratic upper bound (3.4), which is a consequence.
• Strong convexity. It is the published predicate OnlineConvexOpt.ConvexBasics.StronglyConvexOn X f g α, which is display (3.13) with the same gradient map. Display (3.14) and Theorem 3.10 use $\alpha>0$.
• Projection. The projection is the published relation IsMetricProjection X y p: $p\in\mathcal X$ and $\|y-p\|\le\|y-z\|$ for every $z\in\mathcal X$. No choice function is used.
• Run. A run is IsProjGDRun X g β x: $\beta>0$, $x_1\in\mathcal X$, and for every $t\ge1$ the iterate $x_{t+1}$ is a projection of $x_t-\beta^{-1}g(x_t)$. Indices start at $1$ as in the book, and x 0 is unused.
• Gradient mapping. gradMap β x xplus $=\beta(x-x^+)$ takes the projected point of the run as an argument.
• Positivity. $\beta>0$ is assumed, as the step size $1/\beta$ requires, and $\alpha>0$ for Theorem 3.10, as $\kappa=\beta/\alpha$ requires.
• The recursion. The recursion of milestone 6 is stated multiplied by $2\beta\|x_1-x^*\|^2$, so the case $x_1=x^*$ needs no division.
• No trivial readings. A run predicate with a free step size, or $\beta$-smoothness replaced by the quadratic bound (3.4), would change the content. Both are excluded: the step is fixed to $1/\beta$, and smoothness is the Lipschitz condition on the gradient.

Contributions are welcome on any milestone. Lemma 3.1 and (3.7) need only the variational characterization of the projection. Lemma 3.6 needs the quadratic upper bound for a function whose gradient is Lipschitz on a convex set, together with the first-order characterization of convexity relative to a set. Both are of independent use. The induction milestone is a self-contained statement about real sequences.

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, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer Academic Publishers, 2004. doi:10.1007/978-1-4419-8853-9
• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., MIT Press, 2022. arXiv:1909.05207

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$,

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

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

Many constrained optimization problems in machine learning and statistics have a feasible set $\mathcal X$ over which a linear function is cheap to minimize but a Euclidean projection is expensive: the $\ell_1$-ball, the simplex, the nuclear-norm ball, the convex hull of a combinatorial family. Projected gradient descent needs a projection at every step. Conditional gradient descent, introduced by Frank and Wolfe in 1956 for quadratic programming, replaces the projection by a call to a linear minimization oracle over $\mathcal X$, and its iterates are convex combinations of oracle outputs, which makes them sparse when $\mathcal X$ is a polytope.

This mission is the seventh 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 Section 3.3, whose main result, Theorem 3.8, is the $O(1/t)$ rate of the method in the form given by Jaggi (2013), going back to Dunn and Harshbarger (1978).

Setting

Let $E$ be a finite-dimensional real vector space with an arbitrary norm $\|\cdot\|$. For a linear form $g$ on $E$, written $v\mapsto g^\top v$, the dual norm is $\|g\|_*=\sup_{\|v\|\le1}g^\top v$. Let $\mathcal X\subseteq E$ be nonempty, compact and convex, with diameter $R=\sup_{x,y\in\mathcal X}\|x-y\|$.