Third Cumulant as a Centered Third Moment

Proved

FunctionalInequalities.Analysis.BakryEmery.cumulant_three_eq_integral_of_integrable_exp_readable

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

bkl2026functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes the third-cumulant identity from Bizeul–Klartag–Lehec, Lemma 4.2, p. 18, in its stated local form.

Let $E$ be a finite-dimensional real inner-product space with Borel structure, let $\mu$ be a probability measure, and let $r>0$ satisfy

\int e^{r\|x\|}\,d\mu(x)<\infty.

Assume that $\mu$ is centered, meaning $\int\langle v,x\rangle\,d\mu(x)=0$ for every $v\in E$ . Then for all $u,v,w\in E$ ,

\kappa_3^\mu(u,v,w) = \int \langle u,x\rangle\langle v,x\rangle\langle w,x\rangle\,d\mu(x).

The cumulant is evaluated on the three directions using cumulant μ 3 ![u, v, w]. The result assumes only one positive exponential moment, not all exponential moments or log-concavity.

Original Lean declaration header

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

theorem cumulant_three_eq_integral_of_integrable_exp (μ : Measure E) [IsProbabilityMeasure μ]
    {r : ℝ} (hr : 0 < r) (hexp : Integrable (fun x => Real.exp (r * ‖x‖)) μ)
    (hc : ∀ v : E, ∫ x, ⟪v, x⟫ ∂μ = 0) (u v w : E) :
    cumulant μ 3 ![u, v, w] = ∫ x, ⟪u, x⟫ * ⟪v, x⟫ * ⟪w, x⟫ ∂μ

Module navigation

Module: Analysis/BakryEmery/Cumulant/Local.

Definition modules: Analysis/BakryEmery/Cumulant/Basic.

Supporting theorems: contDiffOn_logLaplace_ball, inner_exp_weights, tiltAverage_inner_eq_fderiv_logLaplace_of_lt.

Previous: inner_exp_weights · Next: memLp_of_polynomial_bound_of_integrable_exp.

Source excerpt, lines 101–104 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Cumulant_Local

open MeasureTheory Filter Topology
open scoped RealInnerProductSpace ContDiff
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]

Formal statement


theorem FunctionalInequalities.Analysis.BakryEmery.cumulant_three_eq_integral_of_integrable_exp_readable (μ : Measure E) [IsProbabilityMeasure μ]
    {r : ℝ} (hr : 0 < r) (hexp : Integrable (fun x => Real.exp (r * ‖x‖)) μ)
    (hc : ∀ v : E, ∫ x, ⟪v, x⟫ ∂μ = 0) (u v w : E) :
    cumulant μ 3 ![u, v, w] = ∫ x, ⟪u, x⟫ * ⟪v, x⟫ * ⟪w, x⟫ ∂μ := by sorry

Source

Source: Bizeul–Klartag–Lehec, Presenting a proof of the Kannan–Lovász–Simonovits conjecture (arXiv:2610.05474v1), Lemma 4.2, p. 18. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/Cumulant/Local.lean#L99-L170 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.Cumulant.Local`, declaration `FunctionalInequalities.Analysis.BakryEmery.cumulant_three_eq_integral_of_integrable_exp`; the repository is private at upload time).

View graph