Smooth Relaxation Bound by Local-Slope Energy

Proved

FunctionalInequalities.Energy.SmoothGradient.relaxation_le_localSlope_of_lipschitzWith_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement bounds the smooth-gradient relaxation of a globally Lipschitz test by its local-slope energy.

Let $V$ be a finite-dimensional real inner-product space with complete Borel measurable and second-countable structure. Let $\nu$ be a probability measure on $V$ , let $g:V\to\mathbb R$ , and let $L\in[0,\infty)$ . Assume:

$g$ is globally $L$ -Lipschitz, expressed by LipschitzWith L g.
$g\in L^2(\nu)$ , expressed by MemLp g 2 (\nu : Measure V).

Then

\operatorname{relaxation}(\nu)([g]_{L^2(\nu)}) \leq \operatorname{LocalSlope.energy}(\nu,g).

The energies take values in $[0,\infty]$ . This is a density and recovery estimate for globally Lipschitz tests, relating the relaxed smooth energy to the raw local-slope energy.

Original Lean declaration header

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

theorem relaxation_le_localSlope_of_lipschitzWith (ν : ProbabilityMeasure V) {g : V → ℝ}
    {L : ℝ≥0} (hg : LipschitzWith L g) (hmem : MemLp g 2 (ν : Measure V)) :
    relaxation ν (hmem.toLp g) ≤ LocalSlope.energy ν g

Module navigation

Module: Energy/Euclidean/Slope/Density.

Definition modules: Energy/LocalSlope/Basic, Energy/Form/Functional, Energy/SmoothGradient/Basic.

Supporting theorems: exists_patch, lowerSemicontinuous_secant, lowerSemicontinuous_sequentialRelaxation, relaxation_le_asymptoticLipschitz_of_lipschitzWith.

Previous: exists_patch · Next: sq_add_le_mul_sq_add.

Source excerpt, lines 800–802 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Energy_Euclidean_Slope_Density

open MeasureTheory Filter Topology Set
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]

Formal statement


theorem FunctionalInequalities.Energy.SmoothGradient.relaxation_le_localSlope_of_lipschitzWith_readable (ν : ProbabilityMeasure V) {g : V → ℝ}
    {L : ℝ≥0} (hg : LipschitzWith L g) (hmem : MemLp g 2 (ν : Measure V)) :
    relaxation ν (hmem.toLp g) ≤ LocalSlope.energy ν g := by sorry

Source

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

View graph