Convex Optimization

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

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

$$\Pi_{\mathcal X}(y)=\operatorname*{argmin}_{z\in\mathcal X}\|y-z\| ,$$

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:

$$\|\nabla f(x)-\nabla f(y)\|\le\beta\|x-y\|\qquad(x,y\in\mathcal X).$$

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

$$x_{t+1}=\Pi_{\mathcal X}\Bigl(x_t-\tfrac1\beta\nabla f(x_t)\Bigr)\qquad(t\ge1).$$

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

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

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

$$f(x^+)-f(y)\le g_{\mathcal X}(x)^\top(x-y)-\frac1{2\beta}\|g_{\mathcal X}(x)\|^2 .$$

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$

$$\|x_{t+1}-x^*\|^2\le\exp\Bigl(-\frac t\kappa\Bigr)\|x_1-x^*\|^2 .$$

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