Fixed-Dimension Cumulant Norm Bound

This statement gives an a-priori cumulant bound in each fixed dimension.

For every $n,m\in\mathbb{N}$, there exists a constant $C\ge0$ such that every probability law $\nu$ on $\operatorname{EuclideanSpace}(\mathbb{R},\operatorname{Fin}n)$ that is log-concave, isotropic, and compactly supported satisfies

The constant may depend on both $n$ and $m$; the statement does not assert a universal or dimension-free bound. It provides fixed-dimensional control for later energy estimates.

Original Lean declaration header

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

theorem exists_norm_cumulant_le_isotropic (m : ℕ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ ν : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)),
      KLS.LogConcave ν → KLS.Isotropic ν → IsCompact (ν : Measure (EuclideanSpace ℝ (Fin n))).support →
        ‖cumulant (ν : Measure (EuclideanSpace ℝ (Fin n))) m‖ ≤ C

Module navigation

Module: KLS/BKL/CumulantEnergy/Bound.

Definition modules: Probability/LogConcave, KLS/Isotropic, Analysis/BakryEmery/Cumulant/Basic.

Supporting theorems: norm_cumulant_le_of_moment_bounds, Isotropic.integral_norm_sq.

Next: exists_sum_sq_cumulant_le_isotropic.

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