Smooth-Test Constant Equals Lipschitz-Gradient Constant

Proved

FunctionalInequalities.Poincare.SmoothTest.constant_eq_lipschitz_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This identifies two optimal Poincaré constants.

Let $V$ be a finite-dimensional real inner-product normed space with Borel and second-countable structure. Let $\nu$ be a probability measure, $m$ an additive Haar measure, and assume $\nu\ll m$ and

\nu\bigl(\partial\operatorname{supp}\nu\bigr)=0.

Then the smooth-test constant equals the optimal constant of the Lipschitz-gradient relaxation:

\mathrm{SmoothTest.constant}(\nu) =\mathrm{L2Energy.constant}\bigl(\nu,\mathrm{LipschitzGradient.relaxation}(\nu,m,\nu\ll m)\bigr).

This is an equality of optimal values, which may be $\infty$ ; it does not assert that either constant is finite.

Original Lean declaration header

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

theorem constant_eq_lipschitz
    (hac : (ν : Measure V) ≪ m) (hfr : (ν : Measure V) (frontier (ν : Measure V).support) = 0) :
    constant (ν : Measure V) =
      Poincare.L2Energy.constant ν (Energy.LipschitzGradient.relaxation ν m hac)

Module navigation

Module: Poincare/LipschitzGradient/Comparison.

Definition modules: Poincare/SmoothTest/Basic, Poincare/L2/Energy.

Supporting theorems: holds_ofPreEnergy_of_localSlope, localSlope_holds_of_relaxation, holds_iff_localSlope, holds_ofPreEnergy_iff.

Previous: localSlope_holds_of_relaxation · Next: relaxation_le_mul_lipschitz.

Source excerpt, lines 174–177 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Poincare_LipschitzGradient_Comparison

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]

Formal statement


theorem FunctionalInequalities.Poincare.SmoothTest.constant_eq_lipschitz_readable
    (hac : (ν : Measure V) ≪ m) (hfr : (ν : Measure V) (frontier (ν : Measure V).support) = 0) :
    constant (ν : Measure V) =
      Poincare.L2Energy.constant ν (Energy.LipschitzGradient.relaxation ν m hac) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Poincare/LipschitzGradient/Comparison.lean#L172-L194 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Poincare.LipschitzGradient.Comparison`, declaration `FunctionalInequalities.Poincare.SmoothTest.constant_eq_lipschitz`; the repository is private at upload time).

View graph