Lemma 2.2 — consequences of convexity and $\mathcal L$ -smoothness

Proved

AccelSGDGrowth.lemma_2_2

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

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

Let $\mathcal L>0$ and $f\in\mathcal F(0,\mathcal L)$ , i.e. $f$ is continuously differentiable, convex and satisfies the upper quadratic bound of (1.2). Then for all $x,y\in\mathbb R^d$ :

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

Clause 1 (Lipschitz gradient) is what makes $\mathbb E\|\nabla f(x_k)\|^2$ finite along the algorithm.

Differences from the source:

encoding: f ∈ F(0, L), L the smoothness constant → 0 < L as a hypothesis; reason: the page divides by 2L and by L

Preamble

import Definitions.Def_AccelSGDGrowth_ClassF

Formal statement

namespace AccelSGDGrowth

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

**Formalization Note.** `F(0, L)` is `ClassF 0 L f`: (1.2) with `m = 0`, i.e. convexity plus the
quadratic upper bound. `L > 0` is the smoothness constant the page divides by. -/
theorem lemma_2_2 {d : ℕ} {L : ℝ} (hL : 0 < L) {f : EuclideanSpace ℝ (Fin d) → ℝ}
    (hf : ClassF 0 L f) :
    (∀ x y : EuclideanSpace ℝ (Fin d),
      ‖gradient f y - gradient f x‖ ≤ L * ‖y - x‖) ∧
    (∀ x y : EuclideanSpace ℝ (Fin d),
      f x + inner ℝ (gradient f x) (y - x) + ‖gradient f y - gradient f x‖ ^ 2 / (2 * L) ≤ f y) ∧
    (∀ x y : EuclideanSpace ℝ (Fin d),
      ‖gradient f y - gradient f x‖ ^ 2 / L ≤ inner ℝ (gradient f y - gradient f x) (y - x)) ∧
    (∀ x y : EuclideanSpace ℝ (Fin d),
      inner ℝ (gradient f y - gradient f x) (y - x) ≤ L * ‖y - x‖ ^ 2) := 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.2, pp.5–6

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.2 — consequences of convexity and L\mathcal LL-smoothness

Lemma 2.2 — consequences of convexity and $\mathcal L$ -smoothness