Fixed-Dimension Cumulant Energy Bound

Proved

FunctionalInequalities.KLS.BKL.exists_sum_sq_cumulant_le_isotropic_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement gives a fixed-dimensional bound for the squared coordinate sum of a cumulant tensor.

For every $n,d\in\mathbb{N}$ , there exists $b\ge0$ such that every compactly supported isotropic log-concave probability law $\nu$ on $\operatorname{EuclideanSpace}(\mathbb{R},\operatorname{Fin}n)$ and every $u$ satisfy

\sum_{J:\operatorname{Fin}d\to\operatorname{Fin}n} \kappa_{d+1}\bigl(\nu;u,e_{J_1},\ldots,e_{J_d}\bigr)^2 \le b\,\|u\|^2.

The constant is allowed to depend on $n$ and $d$ ; this is an a-priori fixed-dimension estimate rather than a dimension-free theorem.

Original Lean declaration header

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

theorem exists_sum_sq_cumulant_le_isotropic (d : ℕ) :
    ∃ b : ℝ, 0 ≤ b ∧ ∀ ν : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)),
      KLS.LogConcave ν → KLS.Isotropic ν → IsCompact (ν : Measure (EuclideanSpace ℝ (Fin n))).support →
        ∀ u : EuclideanSpace ℝ (Fin n),
          ∑ J : Fin d → Fin n, cumulant (ν : Measure (EuclideanSpace ℝ (Fin n))) (d + 1)
            (Fin.cons u fun k => EuclideanSpace.basisFun (Fin n) ℝ (J k)) ^ 2 ≤ b * ‖u‖ ^ 2

Module navigation

Module: KLS/BKL/CumulantEnergy/Bound.

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

Supporting theorems: exists_norm_cumulant_le_isotropic.

Previous: exists_norm_cumulant_le_isotropic.

Source excerpt, lines 52–57 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_CumulantEnergy_Bound

open MeasureTheory
open FunctionalInequalities.Analysis.BakryEmery
variable {n : ℕ}

Formal statement


theorem FunctionalInequalities.KLS.BKL.exists_sum_sq_cumulant_le_isotropic_readable (d : ℕ) :
    ∃ b : ℝ, 0 ≤ b ∧ ∀ ν : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)),
      KLS.LogConcave ν → KLS.Isotropic ν → IsCompact (ν : Measure (EuclideanSpace ℝ (Fin n))).support →
        ∀ u : EuclideanSpace ℝ (Fin n),
          ∑ J : Fin d → Fin n, cumulant (ν : Measure (EuclideanSpace ℝ (Fin n))) (d + 1)
            (Fin.cons u fun k => EuclideanSpace.basisFun (Fin n) ℝ (J k)) ^ 2 ≤ b * ‖u‖ ^ 2 := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/CumulantEnergy/Bound.lean#L51-L87 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.CumulantEnergy.Bound`, declaration `FunctionalInequalities.KLS.BKL.exists_sum_sq_cumulant_le_isotropic`; the repository is private at upload time).

View graph