Closed Dimension-Free KLS Bound

The declaration proves the project-level proposition KLS.Conjecture: there is a universal finite constant controlling the literature Poincaré constant of every log-concave probability measure with finite second moment on every finite-dimensional Euclidean space, in the covariance-normalized form

This is the closed endpoint of the Bizeul–Klartag–Lehec formalization and is reused by the public KLS target theorem.

Formalization Note: The exact proposition is represented by the opaque definition KLS.Conjecture; the displayed expansion follows the module's documented meaning of that definition.

Original Lean source

Within namespace FunctionalInequalities.KLS.BKL.Localization. Shown in its original module context.

theorem conjecture : KLS.Conjecture :=
  conjecture_of_letwinCompact LogConcave.Suspension.letwinCompactBound

Module navigation

Module: KLS/BKL/Poincare.

Definition modules: KLS/Statement.

Selected supporting theorems: cumulantBoundCompact_of_cutoffEnergyClaim, cutoffEnergyClaim_all, cutoffEnergyClaim_succ, generator_cumulantEnergy_ge, cumulantBound_of_compact.

Previous: exists_isotropicBound.

Source excerpt, lines 40–41 · Frozen source 408915f.

Literature

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