Regularity of a Centered Second Difference

Proved

FunctionalInequalities.Analysis.centeredDifference_contDiff_lipschitz_gradient_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readableletwin2026log-concave

This formalizes the regularity estimate for a centered second difference, cited in the literature register as part of Theorem 2.5 of Letwin (arXiv:2607.24164v1).

Let $u:\mathbb R^n\to\mathbb R$ be $C^1$ , let $G\in[0,\infty)$ , and suppose its gradient is $G$ -Lipschitz. For any $h\in\mathbb R^n$ , define

v_h(x)=u(x+h)+u(x-h)-2u(x).

Then $v_h$ is $C^1$ and its gradient is $4G$ -Lipschitz:

\operatorname{Lip}(\nabla v_h)\le 4G.

The Lean declaration is centeredDifference_contDiff_lipschitz_gradient_readable. The result is an adapter for centered-difference estimates and does not assume convexity.

Original Lean declaration header

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

theorem centeredDifference_contDiff_lipschitz_gradient {n : ℕ}
    {u : EuclideanSpace ℝ (Fin n) → ℝ} (hu : ContDiff ℝ 1 u)
    {G : NNReal} (hG : LipschitzWith G (gradient u))
    (h : EuclideanSpace ℝ (Fin n)) :
    ContDiff ℝ 1 (fun x => u (x + h) + u (x - h) - 2 * u x) ∧
      LipschitzWith (4 * G)
        (gradient (fun x => u (x + h) + u (x - h) - 2 * u x))

Module navigation

Module: Analysis/Convex/SecondDifference.

Previous: secondDifference_le_of_penalized_maxima · Next: centeredDifference_nonneg_le.

Source excerpt, lines 781–787 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Convex_SecondDifference

Formal statement


theorem FunctionalInequalities.Analysis.centeredDifference_contDiff_lipschitz_gradient_readable {n : ℕ}
    {u : EuclideanSpace ℝ (Fin n) → ℝ} (hu : ContDiff ℝ 1 u)
    {G : NNReal} (hG : LipschitzWith G (gradient u))
    (h : EuclideanSpace ℝ (Fin n)) :
    ContDiff ℝ 1 (fun x => u (x + h) + u (x - h) - 2 * u x) ∧
      LipschitzWith (4 * G)
        (gradient (fun x => u (x + h) + u (x - h) - 2 * u x)) := by sorry

Source

Source: Letwin, The KLS constant is O(log^(1/4) n) (arXiv:2607.24164v1), Theorem 2.5. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Convex/SecondDifference.lean#L779-L834 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Convex.SecondDifference`, declaration `FunctionalInequalities.Analysis.centeredDifference_contDiff_lipschitz_gradient`; the repository is private at upload time).

View graph