Third Cumulant Bound From the Compact Letwin Bound

This formalizes the compactly supported part of Bizeul–Klartag–Lehec Lemma 4.2, p. 18.

Assume LetwinCompactBound. Then the compact cumulant bound holds in order $d=2$ with constant $8$:

Unfolded, this means that for every dimension $n$, every compactly supported isotropic log-concave probability measure $\mu$ on $\mathbb R^n$, and every vector $u$, the sum of squared third cumulants indexed by pairs of basis directions is at most

The declaration treats LetwinCompactBound as a hypothesis; it does not prove that hypothesis or a general KLS bound.

Original Lean declaration header

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

theorem cumulantBoundCompact_two_of_letwinCompact (h : LetwinCompactBound) :
    CumulantBoundCompact 2 8

Module navigation

Module: KLS/BKL/CompactReduction.

Supporting theorems: sum_sq_cumulant_three_le_of_letwin_of_integrable_exp_basis, exists_integrable_exp_norm.

Next: norm_sub_one_le_of_isPositive_mul_self.

Source excerpt, lines 53–54 · Frozen source 408915f.