Prove2Me

KLS Bound from Universal Cumulant Bounds

Proved
FunctionalInequalities.KLS.conjecture_of_cumulantBound_readable

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

bkl2026functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

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

Assume that there exists K∈RK\in\mathbb R such that 1≤K1\le K and

∀d∈N,2≤d ⟹ CumulantBound⁡(d,(d!)2Kd).\forall d\in\mathbb N,\quad 2\le d\ \Longrightarrow\ \operatorname{CumulantBound}\bigl(d,(d!)^2K^d\bigr).

Then the proposition KLS.Conjecture holds.

The declaration is the conditional assembly from the universal cumulant estimate to the formalized dimension-free KLS statement. It does not itself assert the cumulant hypothesis; that hypothesis is supplied separately by a closed producer in the development.

Formalization Note: KLS.Conjecture is an opaque project-level proposition in this type. The implication is an existence hypothesis followed by a proposition, not an unconditional statement of the cumulant bounds.

Original Lean declaration header

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

theorem conjecture_of_cumulantBound
    (hSource : ∃ K : ℝ, 1 ≤ K ∧
      ∀ d : ℕ, 2 ≤ d → CumulantBound d ((d.factorial : ℝ) ^ 2 * K ^ d)) :
    KLS.Conjecture

Module navigation

Module: KLS/BKL/Reduction.

Definition modules: KLS/BKL/Suspension/Law, KLS/Statement.

Supporting theorems: exists_isotropic_localSlope_constant_eq, localSlope_le_mul_intrinsicCovariance, localSlope_le_of_cumulantBound_all.

Previous: localSlope_le_of_cumulantBound_all.

Source excerpt, lines 335–338 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Reduction

open FunctionalInequalities.KLS.LogConcave.Suspension
Formal statement

theorem FunctionalInequalities.KLS.conjecture_of_cumulantBound_readable
    (hSource : ∃ K : ℝ, 1 ≤ K ∧
      ∀ d : ℕ, 2 ≤ d → CumulantBound d ((d.factorial : ℝ) ^ 2 * K ^ d)) :
    KLS.Conjecture := 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#L332-L349 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Reduction`, declaration `FunctionalInequalities.KLS.conjecture_of_cumulantBound`; the repository is private at upload time).

View graph