Cumulant Bound From the Cutoff Energy Claim

This formalizes the cutoff-to-cumulant implication associated with the cumulant bounds in Theorem 4.1 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), p. 18.

Let $K\in\mathbb R$ satisfy $0\le K$, and let $d\in\mathbb N$. Assume CutoffEnergyClaim K d. Then the compact cumulant bound holds with parameter envelope K (d + 1):

The definition CumulantBoundCompact quantifies over finite dimensions, isotropic log-concave probability measures, compact-support hypotheses, and vectors $u$, and bounds the corresponding sum of squared cumulants by

This declaration is an auxiliary interface converting the stated cutoff-energy hypothesis into the compact cumulant-bound formulation.

Original Lean declaration header

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

theorem cumulantBoundCompact_of_cutoffEnergyClaim {K : ℝ} (hK : 0 ≤ K) {d : ℕ} (h : CutoffEnergyClaim K d) :
    LogConcave.Suspension.CumulantBoundCompact d (envelope K (d + 1))

Module navigation

Module: KLS/BKL/Localization/CutoffEnergy/ToCumulant.

Definition modules: KLS/BKL/Localization/CutoffEnergy/Basic, KLS/BKL/CumulantEnvelope, KLS/BKL/CompactReduction.

Supporting theorems: exists_isEldanCutoff, IsBrownianFiltration.rightCont, MultidimBrownianMotion.exists, isBrownianFiltration_natural.

Source excerpt, lines 47–48 · Frozen source 408915f.