Lipschitz-Gradient Relaxation Bounded By Smooth Relaxation

Proved

FunctionalInequalities.Energy.SmoothGradient.lipschitzRelaxation_le_relaxation_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This theorem compares the sequential relaxation generated by globally Lipschitz gradient tests with the smooth-gradient relaxation.

Let $V$ be a finite-dimensional complete real inner-product normed space with its Borel measurable structure and second-countable topology. Let $\nu$ be a probability measure on $V$ , let $m$ be an additive Haar measure, and let $D$ be a local density for $(\nu,m)$ . For every $x\in L^2(\nu)$ ,

\operatorname{sequentialRelaxation}_{\operatorname{lipschitzOperator}(\nu,m,D)}(x) \le \operatorname{relaxation}_{\operatorname{smoothGradient}}(\nu)(x).

The Lean declaration is lipschitzRelaxation_le_relaxation_readable. Both sides are ENNReal-valued functionals and may equal $\top$ . This is an inequality of relaxed energies; it does not assert equality or finiteness.

Original Lean declaration header

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

theorem lipschitzRelaxation_le_relaxation (x : Lp ℝ 2 (ν : Measure V)) :
    (PreEnergy.ofLinearPMap (lipschitzOperator ν m D)).sequentialRelaxation x ≤ relaxation ν x

Module navigation

Module: Energy/SmoothGradient/Core.

Definition modules: Energy/Form/Functional, Energy/Relaxation/LinearPMap, Energy/SmoothGradient/Basic, Energy/Relaxation/Basic.

Supporting theorems: lowerSemicontinuous_sequentialRelaxation, Test.exists_domain_sequence_tendsto.

Previous: Test.exists_domain_sequence_tendsto.

Source excerpt, lines 265–266 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Energy_SmoothGradient_Core

open MeasureTheory Filter Topology
universe u
variable {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
variable (ν : MeasureTheory.ProbabilityMeasure V) (m : MeasureTheory.Measure V) [m.IsAddHaarMeasure] (D : FunctionalInequalities.Energy.SmoothGradient.LocalDensity ν m)

Formal statement


theorem FunctionalInequalities.Energy.SmoothGradient.lipschitzRelaxation_le_relaxation_readable (x : Lp ℝ 2 (ν : Measure V)) :
    (PreEnergy.ofLinearPMap (lipschitzOperator ν m D)).sequentialRelaxation x ≤ relaxation ν x := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Energy/SmoothGradient/Core.lean#L263-L282 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Energy.SmoothGradient.Core`, declaration `FunctionalInequalities.Energy.SmoothGradient.lipschitzRelaxation_le_relaxation`; the repository is private at upload time).

View graph