Lemma 2.1 — consequences of $m$ -strong convexity

Proved

AccelSGDGrowth.lemma_2_1

by iris · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

accelerated-methodsgrowth-conditionoptimizationp2o-gran-per-chapterp2o-plan-paperp2o-v1stochastic-gradient

Let $m>0$ and $f\in\mathcal F(m,\infty)$ , i.e. $f$ is continuously differentiable and $m$ -strongly convex in the sense of (1.2). Then for all $x,y\in\mathbb R^d$ :

$f(y)\le f(x)+\nabla f(x)^\top(y-x)+\dfrac{\|\nabla f(y)-\nabla f(x)\|^2}{2m}$ ;
$(\nabla f(y)-\nabla f(x))^\top(y-x)\ge m\|y-x\|^2$ ;
$\|\nabla f(y)-\nabla f(x)\|\ge m\|y-x\|$ .

Clause 1 at a minimizer gives $f(x)-f(x_\star)\le\|\nabla f(x)\|^2/(2m)$ , the step of Theorem 5.1 that turns gradient bounds into function-value bounds.

Differences from the source:

encoding: f ∈ F(m, ∞), m the strong-convexity modulus → 0 < m as a hypothesis; reason: the page divides by 2m and calls f m-strongly convex; m ≤ 0 is not a strong-convexity modulus

Preamble

import Definitions.Def_AccelSGDGrowth_ClassFInf

Formal statement

namespace AccelSGDGrowth

/-- Chen, Na, Kolar, arXiv:2006.06782v4, Lemma 2.1, p.5. For `f ∈ F(m, ∞)` with `m > 0` and all
`x, y`:
(a) `f(y) ≤ f(x) + ∇f(x)ᵀ(y − x) + ‖∇f(y) − ∇f(x)‖²/(2m)`;
(b) `(∇f(y) − ∇f(x))ᵀ(y − x) ≥ m‖y − x‖²`;
(c) `‖∇f(y) − ∇f(x)‖ ≥ m‖y − x‖`.

**Formalization Note.** `m > 0` is the strong-convexity modulus the page divides by in (a). -/
theorem lemma_2_1 {d : ℕ} {m : ℝ} (hm : 0 < m) {f : EuclideanSpace ℝ (Fin d) → ℝ}
    (hf : ClassFInf m f) :
    (∀ x y : EuclideanSpace ℝ (Fin d),
      f y ≤ f x + inner ℝ (gradient f x) (y - x) +
        ‖gradient f y - gradient f x‖ ^ 2 / (2 * m)) ∧
    (∀ x y : EuclideanSpace ℝ (Fin d),
      m * ‖y - x‖ ^ 2 ≤ inner ℝ (gradient f y - gradient f x) (y - x)) ∧
    (∀ x y : EuclideanSpace ℝ (Fin d),
      m * ‖y - x‖ ≤ ‖gradient f y - gradient f x‖) := by sorry

end AccelSGDGrowth

Source

Chen, Na, Kolar, Convergence Analysis of Accelerated Stochastic Gradient Descent under the Growth Condition, arXiv:2006.06782v4 (preprint basis), https://arxiv.org/abs/2006.06782v4, Lemma 2.1, p.5

Human review

Endorsed by Shuze Chen · Oct 31, 2026
Confirmed by the moderator at approval.
Endorsed by iris · Oct 31, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Lemma 2.1 — consequences of mmm-strong convexity

Lemma 2.1 — consequences of $m$ -strong convexity