Closed Cumulant Bound with Constant $153$

For every $d\ge 1$, every dimension $m$, every isotropic log-concave probability law $\nu$ on $\mathbb R^m$ and every vector $u$, the $(d+1)$-st cumulant tensor satisfies

where $J$ ranges over all $d$-tuples of coordinate indices, i.e. $R^\nu_{d+1}\le 153^{d}(d!)^2\,\mathrm{Id}$. This is Theorem 4.1 of BKL with one explicit universal constant, obtained from the cutoff induction and the compact Letwin bound. Source: BKL arXiv:2610.05474v1, Theorem 4.1, p. 18.

Original Lean source

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

theorem cumulantBound_153 : ∀ d : ℕ, 1 ≤ d →
    LogConcave.Suspension.CumulantBound d ((d.factorial : ℝ) ^ 2 * (153 : ℝ) ^ d) :=
  cumulantBound_of_letwinCompact LogConcave.Suspension.letwinCompactBound

Module navigation

Module: KLS/BKL/CumulantBound.

Definition modules: KLS/BKL/Suspension/Law.

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

Previous: cutoffEnergyClaim_153.

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