Universal Isotropic Poincaré Bound

There exists a nonnegative real constant $C$ represented as an NNReal, with $0<C$, such that KLS.IsotropicBound C holds. In the formalization, this means that the same constant bounds the intrinsic local-slope Poincaré constant for every finite-dimensional real inner-product space satisfying the required measurable, Borel, complete, and second-countable hypotheses, and every isotropic log-concave probability measure on that space.

The resulting universal isotropic bound is the closed finite-dimensional Poincaré estimate used in the final KLS assembly.

Formalization Note: The witness has type NNReal, while the Poincaré constants being bounded take values in $[0,\infty]$ (ENNReal). The construction specializes the cumulant parameter to $153$.

Original Lean declaration header

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

theorem exists_isotropicBound : ∃ C : NNReal, 0 < C ∧ KLS.IsotropicBound.{u} C

Module navigation

Module: KLS/BKL/Poincare.

Definition modules: KLS/LogConcave/Isotropic.

Supporting theorems: cumulantBound_153, localSlope_le_of_cumulantBound_all.

Next: conjecture.

Source excerpt, lines 24–24 · Frozen source 408915f.

Literature

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