Identity-weighted Lipschitz-gradient relaxation

Definition

KLSModular_FunctionalInequalities_Poincare_LipschitzGradient_Comparison

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a probability measure ν on a finite-dimensional, second-countable normed inner-product space $V$ , and a Haar measure m with $(ν : \text{Measure }V) \ll m$ , Energy.LipschitzGradient.relaxation is the sequential relaxation on $L^2(ν)$ of the squared gradient energy for globally Lipschitz tests. It is defined using the weighted-gradient operator with the identity map as weight; this bundle only defines the functional and does not assert any Poincaré inequality or finiteness property.

Original module imports

import FunctionalInequalities.Energy.WeightedGradient.Core
import FunctionalInequalities.Poincare.LocalSlope.SmoothTestComparison
import FunctionalInequalities.Poincare.Relaxation
import FunctionalInequalities.Probability.Covariance.Factorization

Original declaration excerpt

Shown in the original module context.

def relaxation (hac : (ν : Measure V) ≪ m) :
    Functional (Lp ℝ 2 (ν : Measure V)) :=
  (PreEnergy.ofLinearPMap (Energy.WeightedGradient.operator ν (ContinuousLinearMap.id ℝ V) hac)).sequentialRelaxation

Module navigation

Direct project imports: Energy/WeightedGradient/Core, Poincare/LocalSlope/SmoothTestComparison, Poincare/Relaxation, Probability/Covariance/Factorization.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Poincare.LipschitzGradient.Comparison · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Energy_WeightedGradient_Core
import Definitions.Def_KLSModular_FunctionalInequalities_Poincare_LocalSlope_SmoothTestComparison
import Definitions.Def_KLSModular_FunctionalInequalities_Poincare_Relaxation
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Covariance_Factorization

noncomputable section
open MeasureTheory Filter Topology
open scoped ContDiff
namespace FunctionalInequalities
open Energy.Euclidean
universe u
variable {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
variable (ν : ProbabilityMeasure V) (m : Measure V) [m.IsAddHaarMeasure]
namespace Energy
namespace LipschitzGradient
/-- The sequential relaxation of `f ↦ ‖∇f‖²` on the classes of globally Lipschitz `L²(ν)` functions
with square-integrable gradient: the weighted gradient operator with `B = 1`. -/
def relaxation (hac : (ν : Measure V) ≪ m) :
    Functional (Lp ℝ 2 (ν : Measure V)) :=
  (PreEnergy.ofLinearPMap (Energy.WeightedGradient.operator ν (ContinuousLinearMap.id ℝ V) hac)).sequentialRelaxation
end LipschitzGradient
end Energy
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Poincare/LipschitzGradient/Comparison.lean#L52-L56 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Poincare.LipschitzGradient.Comparison`, definition bundle `KLSModular_FunctionalInequalities_Poincare_LipschitzGradient_Comparison`; the repository is private at upload time).

View graph