Local-Slope Constants Extend To The Pre-Energy Test Family

Proved

FunctionalInequalities.Energy.LipschitzGradient.holds_ofPreEnergy_of_localSlope_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This theorem transfers a local-slope Poincaré constant to the associated identity-weighted pre-energy test family.

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 assume

$\nu\ll m$ ;
$\nu(\partial\operatorname{supp}\nu)=0$ ;
for a constant $C\in[0,\infty)$ represented by NNReal, the predicate Poincare.LocalSlope.Holds ν C holds.

Then the same constant satisfies the test-family inequality for the pre-energy generated by the identity-weighted gradient operator:

\operatorname{TestFamily.Holds}\!\left( \operatorname{TestFamily.ofPreEnergy}(\nu, \operatorname{PreEnergy.ofLinearPMap}(\operatorname{WeightedGradient.operator}(\nu,\operatorname{id},\nu\ll m))),C \right).

The declaration is holds_ofPreEnergy_of_localSlope_readable. It is a comparison result between two formally defined Poincaré predicates; it does not assert that such a constant exists or is finite.

Original Lean declaration header

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

theorem holds_ofPreEnergy_of_localSlope (hac : (ν : Measure V) ≪ m)
    (hfr : (ν : Measure V) (frontier (ν : Measure V).support) = 0) {C : NNReal}
    (h : Poincare.LocalSlope.Holds ν C) :
    (Poincare.TestFamily.ofPreEnergy ν
      (PreEnergy.ofLinearPMap (Energy.WeightedGradient.operator ν (ContinuousLinearMap.id ℝ V) hac))).Holds C

Module navigation

Module: Poincare/LipschitzGradient/Comparison.

Definition modules: Energy/WeightedGradient/Basic, Poincare/SmoothTest/Optimal, Poincare/LocalSlope/Basic, Poincare/Relaxation, Energy/Relaxation/LinearPMap.

Supporting theorems: admissible_iff_memLp_gradient, apply_eq_norm_gradient.

Next: localSlope_holds_of_relaxation.

Source excerpt, lines 65–69 · 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.Energy.LipschitzGradient.holds_ofPreEnergy_of_localSlope_readable (hac : (ν : Measure V) ≪ m)
    (hfr : (ν : Measure V) (frontier (ν : Measure V).support) = 0) {C : NNReal}
    (h : Poincare.LocalSlope.Holds ν C) :
    (Poincare.TestFamily.ofPreEnergy ν
      (PreEnergy.ofLinearPMap (Energy.WeightedGradient.operator ν (ContinuousLinearMap.id ℝ V) hac))).Holds C := by sorry

Source

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

View graph