Local Lipschitz Bound for Mollification on Balls

Proved

FunctionalInequalities.Energy.lipschitzOnWith_mollify_ball_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement gives the local Lipschitz stability of mollification under an additive Haar measure.

Let $V$ be a finite-dimensional real inner-product space with its Borel measurable structure, and let $m$ be an additive Haar measure on $V$ . Let $R,\delta\in\mathbb R$ satisfy $0<R$ . Let $c\in[0,\infty)$ , let $g:V\to\mathbb R$ be continuous, and fix $x\in V$ . Assume that $g$ is $c$ -Lipschitz on the ball of radius $\delta+2R$ centered at $x$ .

Then the mollification mollify m R g is $c$ -Lipschitz on the ball of radius $\delta$ centered at $x$ :

\operatorname{LipschitzOnWith}(c,g,B(x,\delta+2R)) \;\Longrightarrow\; \operatorname{LipschitzOnWith}(c,\operatorname{mollify}(m,R,g),B(x,\delta)).

The result is a local recovery tool: the radius- $R$ mollifier requires control only on the enlarged ball of radius $\delta+2R$ .

Original Lean declaration header

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

theorem lipschitzOnWith_mollify_ball (m : Measure V) [m.IsAddHaarMeasure]
    {R δ : ℝ} (hR : 0 < R) {c : ℝ≥0} {g : V → ℝ} (hg : Continuous g) (x : V)
    (h : LipschitzOnWith c g (Metric.ball x (δ + 2 * R))) :
    LipschitzOnWith c (mollify m R g) (Metric.ball x δ)

Module navigation

Module: Energy/Euclidean/Slope/Recovery.

Definition modules: Energy/Euclidean/LipschitzApproximation/Kernel.

Previous: apply_mul_le · Next: limsup_enorm_gradient_mollify_le.

Source excerpt, lines 462–465 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Energy_Euclidean_Slope_Recovery

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

Formal statement


theorem FunctionalInequalities.Energy.lipschitzOnWith_mollify_ball_readable (m : Measure V) [m.IsAddHaarMeasure]
    {R δ : ℝ} (hR : 0 < R) {c : ℝ≥0} {g : V → ℝ} (hg : Continuous g) (x : V)
    (h : LipschitzOnWith c g (Metric.ball x (δ + 2 * R))) :
    LipschitzOnWith c (mollify m R g) (Metric.ball x δ) := by sorry

Source

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

View graph