Cumulant Bound On The Suspension Joint Space

This formalizes the joint-space adapter used in Proposition 7.1 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), p. 28.

Let $N,n,d\in\mathbb N$ and $b\in\mathbb R$. Assume CumulantBound d b, and let $\nu$ be an isotropic log-concave probability measure on

For every $u$ in this joint space, the coordinate cumulants satisfy

where the sum ranges over functions $J:\operatorname{Fin}d\to\operatorname{Option}(\operatorname{Fin}N\times\operatorname{Fin}n)$ and the $e_{J_i}$ are the corresponding coordinate basis vectors.

The declaration transports a cumulant bound through the coordinate equivalence between the joint space and a standard Euclidean space. It is a technical reuse lemma for suspension arguments.

Original Lean declaration header

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

theorem cumulantBound_jointSpace {N n d : ℕ} {b : ℝ} (hb : CumulantBound d b)
    {ν : ProbabilityMeasure (JointSpace N n)} (hiso : KLS.Isotropic ν) (hlc : KLS.LogConcave ν)
    (u : JointSpace N n) :
    ∑ J : Fin d → Option (Fin N × Fin n),
      cumulant (ν : Measure (JointSpace N n)) (d + 1)
        (Fin.cons u fun k => EuclideanSpace.basisFun _ ℝ (J k)) ^ 2 ≤ b * ‖u‖ ^ 2

Module navigation

Module: KLS/BKL/Suspension/Law.

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

Supporting theorems: cumulant_map_linearIsometryEquiv, Isotropic.map_linearIsometryEquiv.

Previous: logConcave_jointLaw_of_eq_tilted.

Source excerpt, lines 281–286 · Frozen source 408915f.