Smooth-Test and Local-Slope Poincaré Equivalence
ProvedFunctionalInequalities.Poincare.SmoothTest.holds_iff_localSlope_readableThis is an equivalence between two Poincaré test classes.
Let be a finite-dimensional real inner-product normed space with Borel and second-countable structure. Let be a probability measure and an additive Haar measure, and assume . For every finite nonnegative constant ,
The two predicates use their respective Lean-defined finite-energy test domains. The result is an exact equivalence, not merely a comparison of optimal constants; it imposes no log-concavity or moment hypothesis.
Original Lean declaration header
Within namespace FunctionalInequalities.Poincare.SmoothTest. Shown in its original module context. Proof omitted.
theorem holds_iff_localSlope (ν : ProbabilityMeasure E) (m : Measure E)
[Measure.IsAddHaarMeasure m] (hν : (ν : Measure E) ≪ m) (C : NNReal) :
Holds (ν : Measure E) (C : ℝ) ↔ Poincare.LocalSlope.Holds ν C
Module navigation
Module: Poincare/LocalSlope/SmoothTestComparison.
Definition modules: Poincare/LocalSlope/Basic, Poincare/SmoothTest/Basic.
Supporting theorems: admissible_iff_memLp_gradient, apply_eq_norm_gradient.
Source excerpt, lines 71–73 · Frozen source 408915f.
import Definitions.Def_KLSModular_FunctionalInequalities_Poincare_LocalSlope_SmoothTestComparison
open MeasureTheory Filter Topology
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
[MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [FiniteDimensional ℝ E]
theorem FunctionalInequalities.Poincare.SmoothTest.holds_iff_localSlope_readable (ν : ProbabilityMeasure E) (m : Measure E)
[Measure.IsAddHaarMeasure m] (hν : (ν : Measure E) ≪ m) (C : NNReal) :
Holds (ν : Measure E) (C : ℝ) ↔ Poincare.LocalSlope.Holds ν C := by sorry