Lipschitz Gradient from a Second-Difference Bound

Proved

FunctionalInequalities.Analysis.lipschitzWith_gradient_of_second_difference_le_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

Let $E$ be a complete real inner-product normed space, let $u:E\to\mathbb R$ be convex and differentiable, and let $C\ge0$ . If for every $x,h\in E$ ,

u(x+h)+u(x-h)-2u(x)\le C\|h\|^2,

then the gradient is globally Lipschitz with constant $4C$ (represented in Lean by Real.toNNReal (4 * C)):

\|\nabla u(x)-\nabla u(y)\|\le4C\|x-y\|.

This is the standard $C^{1,1}$ consequence of the centered second-difference estimate.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem lipschitzWith_gradient_of_second_difference_le {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [CompleteSpace E] {u : E → ℝ} {C : ℝ}
    (hconv : ConvexOn ℝ Set.univ u) (hdiff : Differentiable ℝ u) (hC : 0 ≤ C)
    (hsd : ∀ x h : E, u (x + h) + u (x - h) - 2 * u x ≤ C * ‖h‖ ^ 2) :
    LipschitzWith (Real.toNNReal (4 * C)) (gradient u)

Module navigation

Module: Analysis/Convex/SecondDifference.

Next: sd_penalized_estimate.

Source excerpt, lines 217–221 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_SecondDifference

Formal statement


theorem FunctionalInequalities.Analysis.lipschitzWith_gradient_of_second_difference_le_readable {E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [CompleteSpace E] {u : E → ℝ} {C : ℝ}
    (hconv : ConvexOn ℝ Set.univ u) (hdiff : Differentiable ℝ u) (hC : 0 ≤ C)
    (hsd : ∀ x h : E, u (x + h) + u (x - h) - 2 * u x ≤ C * ‖h‖ ^ 2) :
    LipschitzWith (Real.toNNReal (4 * C)) (gradient u) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Convex/SecondDifference.lean#L215-L480 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Convex.SecondDifference`, declaration `FunctionalInequalities.Analysis.lipschitzWith_gradient_of_second_difference_le`; the repository is private at upload time).

View graph