Finite-Dimensional Poincaré Bound from Universal Cumulant Bounds

Proved

FunctionalInequalities.KLS.localSlope_le_of_cumulantBound_all_readable

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

bkl2026functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes the conditional form of Theorem 1.1 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), p. 2.

There exists a real constant $C>0$ such that, for every $K\in\mathbb R$ with $1\le K$ , if

\forall d\in\mathbb N,\quad 2\le d\ \Longrightarrow\ \operatorname{CumulantBound}\bigl(d,(d!)^2K^d\bigr),

then the following holds for every finite-dimensional complete real inner-product normed space $E$ with measurable Borel structure and second-countable topology, and every probability measure $\mu$ on $E$ that is log-concave and isotropic:

\operatorname{constant}_{\mathrm{Intrinsic}}(\mu) \le \operatorname{ENNReal.ofReal}(2CK).

This declaration extends the regular-potential estimate to arbitrary finite-dimensional isotropic log-concave probability measures and is the main conditional Poincaré assembly.

Formalization Note: The space carries an explicit FiniteDimensional ℝ E instance. The Poincaré constant is ENNReal-valued, while the displayed bound is formed with ENNReal.ofReal.

Original Lean declaration header

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

theorem localSlope_le_of_cumulantBound_all :
    ∃ C : ℝ, 0 < C ∧ ∀ K : ℝ, 1 ≤ K →
      (∀ d : ℕ, 2 ≤ d → CumulantBound d ((d.factorial : ℝ) ^ 2 * K ^ d)) →
      ∀ (E : Type u) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
        [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [FiniteDimensional ℝ E]
        (μ : ProbabilityMeasure E), KLS.LogConcave μ → KLS.Isotropic μ →
          Poincare.LocalSlope.Intrinsic.constant μ ≤ ENNReal.ofReal (2 * C * K)

Module navigation

Module: KLS/BKL/Reduction.

Definition modules: KLS/BKL/Suspension/Law, Probability/LogConcave, KLS/Isotropic, Poincare/LocalSlope/Basic.

Selected supporting theorems: convexOn_of_hessian_ge, exists_ambient_extension, Isotropic.map_linearIsometryEquiv, isBorellDensity_of_eq_tilted, localSlope_le_of_regular_isotropic_bound.

Previous: poincare_le_of_cumulantBound · Next: conjecture_of_cumulantBound.

Source excerpt, lines 307–313 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Reduction

open MeasureTheory FunctionalInequalities.Analysis.BakryEmery FunctionalInequalities.Analysis.Tensor
open FunctionalInequalities.KLS.LogConcave.Suspension
universe u

Formal statement


theorem FunctionalInequalities.KLS.localSlope_le_of_cumulantBound_all_readable :
    ∃ C : ℝ, 0 < C ∧ ∀ K : ℝ, 1 ≤ K →
      (∀ d : ℕ, 2 ≤ d → CumulantBound d ((d.factorial : ℝ) ^ 2 * K ^ d)) →
      ∀ (E : Type u) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
        [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [FiniteDimensional ℝ E]
        (μ : ProbabilityMeasure E), KLS.LogConcave μ → KLS.Isotropic μ →
          Poincare.LocalSlope.Intrinsic.constant μ ≤ ENNReal.ofReal (2 * C * K) := by sorry

Source

Source: Bizeul–Klartag–Lehec, Presenting a proof of the Kannan–Lovász–Simonovits conjecture (arXiv:2610.05474v1), Theorem 1.1, p. 2. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/Reduction.lean#L302-L330 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Reduction`, declaration `FunctionalInequalities.KLS.localSlope_le_of_cumulantBound_all`; the repository is private at upload time).

View graph