{"id":"palomar/PALOMAR-2026-11-01-000014","url":"https://github.com/human-ai-mathematics/kls-lean/tree/33fff6ea218ae07e42115bd1eacfcf7d39c534cb/integrations/palomar","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-01-000014-v1.json","repo":"https://github.com/human-ai-mathematics/kls-lean","tags":["math.PR","math.FA","math.MG","msc:60E15","msc:52A40","msc:46E35"],"score":0,"title":"Dimension-free KLS Poincare bound for isotropic log-concave densities (smooth compactly supported tests)","trust":"high","domain":"math.PR","source":"palomar","authors":["Lazyfill"],"reviews":0,"subject":"math.PR","summary":"A Lean 4 / Mathlib library for Poincare inequalities, log-concave probability measures and stochastic localization. Its dimension-free KLS theorem bounds the intrinsic local-slope Poincare constant by one universal constant times the covariance operator norm, including dimension zero and singular affine supports, for log-concave probability laws with finite second moment. The proof follows Bizeul-Klartag-Lehec through finite-horizon cutoff localization, the compact Letwin constant-8 quadratic variance bound and approximation. Supporting results include Cheeger-Buser comparisons, covariance…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-01","reactions":{},"formalized":true,"formalizes":[{"title":"Presenting a proof of the Kannan-Lovasz-Simonovits conjecture","identifier":"https://arxiv.org/abs/2610.05474v1","relationship":"adapts"}]}