Pointwise Limsup Bound for Mollified Gradients

Proved

FunctionalInequalities.Energy.limsup_enorm_gradient_mollify_le_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement bounds the limiting gradient size of mollifications by the asymptotic Lipschitz constant.

Let $V$ be a finite-dimensional real inner-product space with complete Borel measurable structure, and let $m$ be an additive Haar measure. Let $g:V\to\mathbb R$ be continuous, and fix $x\in V$ . For the prescribed sequence of positive mollification radii radius j, write mollify m (radius j) g for the corresponding mollifications. The gradient norm is regarded as an $[0,\infty]$ -valued ENNReal quantity.

The limsup along $j\to\infty$ satisfies

\limsup_{j\to\infty} \left\|\nabla\bigl(\operatorname{mollify}(m,\operatorname{radius}(j),g)\bigr)(x)\right\|_{\!e} \leq \operatorname{AsymptoticLipschitz.apply}(g,x).

This is a pointwise technical estimate used in smooth recovery of asymptotic-Lipschitz energies. It is stated in ENNReal, so infinite values are allowed.

Original Lean declaration header

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

theorem limsup_enorm_gradient_mollify_le (m : Measure V) [m.IsAddHaarMeasure]
    {g : V → ℝ} (hg : Continuous g) (x : V) :
    limsup (fun j ↦ ‖gradient (mollify m (radius j) g) x‖ₑ) atTop ≤
      AsymptoticLipschitz.apply g x

Module navigation

Module: Energy/Euclidean/Slope/Recovery.

Definition modules: Energy/Euclidean/LipschitzApproximation/Measurable, Energy/LocalSlope/Relaxation, Energy/Euclidean/LipschitzApproximation/Kernel.

Supporting theorems: lipschitzOnWith_mollify_ball.

Previous: lipschitzOnWith_mollify_ball · Next: relaxation_le_asymptoticLipschitz_of_lipschitzWith.

Source excerpt, lines 509–512 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Energy_Euclidean_Slope_Recovery

open MeasureTheory Filter Topology Set
open FunctionalInequalities.Energy.Euclidean.LipschitzApproximation
universe u
variable {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
omit [SecondCountableTopology V]

Formal statement


theorem FunctionalInequalities.Energy.limsup_enorm_gradient_mollify_le_readable (m : Measure V) [m.IsAddHaarMeasure]
    {g : V → ℝ} (hg : Continuous g) (x : V) :
    limsup (fun j ↦ ‖gradient (mollify m (radius j) g) x‖ₑ) atTop ≤
      AsymptoticLipschitz.apply g x := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Energy/Euclidean/Slope/Recovery.lean#L506-L544 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Energy.Euclidean.Slope.Recovery`, declaration `FunctionalInequalities.Energy.limsup_enorm_gradient_mollify_le`; the repository is private at upload time).

View graph