Prove2Me

Corollary 2.2 — ∥∇f(x)∥2≤2L (f(x)−min⁡f)\|\nabla f(x)\|^2\le 2L\,(f(x)-\min f) for f∈CL1,1f\in C^{1,1}_L with a minimizer

Proved
SDEConvexOpt.corollary_2_2

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

convex-optimizationgradient-flowmartingalesp2o-gran-per-chapterp2o-plan-paperp2o-v1stochastic-differential-equations

Let L≥0L\ge0 and let f∈CL1,1(Rd)f\in C^{1,1}_L(\mathbb R^d), i.e. ff is continuously differentiable and ∇f\nabla f is LL-Lipschitz continuous, and assume argmin⁡f≠∅\operatorname{argmin} f\neq\emptyset. Then

∥∇f(x)∥2≤2L (f(x)−min⁡f)for all x∈Rd.\|\nabla f(x)\|^2\le 2L\,\big(f(x)-\min f\big)\qquad\text{for all } x\in\mathbb R^d .

No convexity is assumed. In the proof of Theorem 3.1(iii) this bound turns the integrability of f(X(t))−min⁡ff(X(t))-\min f into that of ∥∇f(X(t))∥2\|\nabla f(X(t))\|^2.

Differences from the source:

  • encoding: min⁡f\min f; CL1,1(Rd)C^{1,1}_L(\mathbb R^d) with L≥0L\ge0 → ⨅ y, f y; ContDiff ℝ 1 f, LipschitzWith L (gradient f) with L : ℝ≥0, on SDEState d; reason: the infimum is the minimum since argmin⁡f≠∅\operatorname{argmin} f\neq\emptyset; the class of p.6
Preamble
import Definitions.Def_EthierKurtz_SDEState
import Definitions.Def_SDEConvexOpt_argminSet

open MeasureTheory ProbabilityTheory Filter
open scoped NNReal ENNReal Topology InnerProductSpace
Formal statement
namespace SDEConvexOpt

open EthierKurtz

/-- Corollary 2.2 of Maulen S., Fadili, Attouch, arXiv:2207.02750v1, p.6: let
`f ∈ C^{1,1}_L(ℝ^d)` such that `argmin f ≠ ∅`; then `‖∇f(x)‖² ≤ 2L(f(x) − min f)` for all
`x ∈ ℝ^d`.

**Formalization Note** `C^{1,1}_L(ℝ^d)` (p.6, `L ≥ 0`) is `ContDiff ℝ 1 f` with
`LipschitzWith L (gradient f)`, `L : ℝ≥0`; no convexity is assumed, as on the page. `min f` is
`⨅ y, f y`, the minimum value since `argmin f ≠ ∅`. -/
theorem corollary_2_2 {d : ℕ} (f : SDEState d → ℝ) (L : ℝ≥0) (hf : ContDiff ℝ 1 f)
    (hL : LipschitzWith L (gradient f)) (hS : (argminSet f).Nonempty) (x : SDEState d) :
    ‖gradient f x‖ ^ 2 ≤ 2 * (L : ℝ) * (f x - ⨅ y, f y) := by sorry

end SDEConvexOpt
Source
Maulen S., Fadili, Attouch, An SDE perspective on stochastic convex optimization, arXiv:2207.02750v1, Corollary 2.2, p.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