Cumulant Norm Bound from Moment Bounds

Proved

FunctionalInequalities.Analysis.BakryEmery.norm_cumulant_le_of_moment_bounds_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is a moment-to-cumulant estimate.

Let $\nu$ be a probability measure on a finite-dimensional real inner-product space $E$ . Suppose $r>0$ , $e^{r\|x\|}$ is integrable with respect to $\nu$ , and for some $m\in\mathbb N$ and $D\in\mathbb R$ ,

\int\|x\|^i\,d\nu(x)\le D^i\qquad(1\le i\le m).

Then the norm of the $m$ -th cumulant tensor satisfies

\|\kappa_m(\nu)\|\le (m!)^2D^m.

This gives a general quantitative bound on cumulants in terms of moments and is independent of any log-concavity assumption.

Original Lean declaration header

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

theorem norm_cumulant_le_of_moment_bounds
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (ν : Measure E) [IsProbabilityMeasure ν] {r : ℝ} (hr : 0 < r)
    (hexp : Integrable (fun x => Real.exp (r * ‖x‖)) ν) {m : ℕ} {D : ℝ}
    (hD : ∀ i : ℕ, 1 ≤ i → i ≤ m → (∫ x, ‖x‖ ^ i ∂ν) ≤ D ^ i) :
    ‖cumulant ν m‖ ≤ (m.factorial : ℝ) ^ 2 * D ^ m

Module navigation

Module: Analysis/BakryEmery/Cumulant/MomentBound.

Definition modules: Analysis/BakryEmery/Cumulant/Basic.

Source excerpt, lines 17–23 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Cumulant_MomentBound

open MeasureTheory

Formal statement


theorem FunctionalInequalities.Analysis.BakryEmery.norm_cumulant_le_of_moment_bounds_readable
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (ν : Measure E) [IsProbabilityMeasure ν] {r : ℝ} (hr : 0 < r)
    (hexp : Integrable (fun x => Real.exp (r * ‖x‖)) ν) {m : ℕ} {D : ℝ}
    (hD : ∀ i : ℕ, 1 ≤ i → i ≤ m → (∫ x, ‖x‖ ^ i ∂ν) ≤ D ^ i) :
    ‖cumulant ν m‖ ≤ (m.factorial : ℝ) ^ 2 * D ^ m := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/Cumulant/MomentBound.lean#L16-L43 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.Cumulant.MomentBound`, declaration `FunctionalInequalities.Analysis.BakryEmery.norm_cumulant_le_of_moment_bounds`; the repository is private at upload time).

View graph