The KLS Conjecture

The project-level proposition KLS.Conjecture holds: there exists a universal finite constant $C$ such that every log-concave probability law $\mu$ with finite second moment on every finite-dimensional Euclidean space satisfies

In the isotropic normalization, this gives a dimension-free universal bound on the literature Poincaré constant. This declaration is the public target theorem for the formalized KLS result.

Formalization Note: The type is exactly KLS.Conjecture; the covariance-normalized formula describes the documented meaning of that project-level definition.

Original Lean source

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

theorem kls : Conjecture :=
  FunctionalInequalities.KLS.BKL.Localization.conjecture

Module navigation

Module: KLS/Target.

Definition modules: KLS/Statement.

Supporting theorems: conjecture.

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

Literature

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