Lemma A.1 (co-coercivity), p. 21 — ‖∇f(x) − ∇f(y)‖² ≤ L⟨x − y, ∇f(x) − ∇f(y)⟩

Proved

SGDKaczmarz.SGD.lemma_A_1

by mikedeng1 · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

co-coercivityconvexityp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1smoothness

Let $\mathcal H$ be a real Hilbert space and $f : \mathcal H \to \mathbb R$ a differentiable convex function whose gradient is Lipschitz with constant $L \ge 0$ . Then for all $x, y \in \mathcal H$

\|\nabla f(x) - \nabla f(y)\|_2^2 \le L\,\langle x - y, \nabla f(x) - \nabla f(y)\rangle.

This is the co-coercivity of the gradient. In the proof of Theorem 2.1 it bounds the squared gradient difference of each component $f_i$ by an inner product that can then be averaged over $i$ .

Formalization Note The page states the lemma "for a smooth function $f$ whose gradient has Lipschitz constant $L$ " and calls the auxiliary functions of its proof convex; convexity of $f$ is stated as a hypothesis here, because without it the inequality fails ( $f(x) = -x^2$ on $\mathbb R$ , $L = 2$ ). Every use in the paper is for a convex $f_i$ .

Preamble

import Mathlib

open scoped NNReal InnerProductSpace

Formal statement

namespace SGDKaczmarz.SGD

/-- Lemma A.1 (Co-coercivity), p. 21: for a differentiable convex `f` whose gradient has Lipschitz
constant `L`, `‖∇f(x) − ∇f(y)‖² ≤ L ⟨x − y, ∇f(x) − ∇f(y)⟩`. -/
theorem lemma_A_1 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (f : H → ℝ) (hf : Differentiable ℝ f) (hconv : ConvexOn ℝ Set.univ f) (L : ℝ≥0)
    (hL : LipschitzWith L (gradient f)) (x y : H) :
    ‖gradient f x - gradient f y‖ ^ 2 ≤ (L : ℝ) * ⟪x - y, gradient f x - gradient f y⟫_ℝ := by sorry

end SGDKaczmarz.SGD

Source

Needell, Srebro & Ward, Stochastic gradient descent, weighted sampling, and the randomized Kaczmarz algorithm, arXiv:1310.5715v5, Lemma A.1, p. 21

Human review

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

View graph