Extension of Compact Cumulant Bounds

This formalizes the compact-support approximation step cited on p. 19 and at the end of Section 6 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), with the literature register associating it with Theorem 4.1.

Let $d\in\mathbb N$ satisfy $1\le d$, let $b\in\mathbb R$, and assume CumulantBoundCompact d b: the cumulant bound holds for compactly supported isotropic log-concave laws. Then the corresponding unrestricted bound holds:

In particular, the bound applies at every order $d+1\ge2$ to every isotropic log-concave probability law. The declaration transfers a hypothesis about compactly supported laws; it does not produce a numerical value of $b$ or prove the compact bound itself.

Original Lean declaration header

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

theorem cumulantBound_of_compact {d : ℕ} (hd : 1 ≤ d) {b : ℝ} (h : CumulantBoundCompact d b) :
    CumulantBound d b

Module navigation

Module: KLS/BKL/CompactReduction.

Definition modules: KLS/BKL/Suspension/Law.

Selected supporting theorems: cumulant_map_affine, cumulant_two_eq_centered_moment_of_integrable_exp, memLp_of_polynomial_bound_of_integrable_exp, tendsto_cumulant_cond_closedBall, exists_integrable_exp_norm.

Previous: exists_standardized.

Source excerpt, lines 316–317 · Frozen source 408915f.