Cumulants as Composed Taylor Jets

Proved

FunctionalInequalities.Analysis.BakryEmery.cumulant_eq_taylorComp_cond_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This identifies cumulants with the Faà di Bruno composition of the Taylor jets of the logarithm and the Laplace transform.

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

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

For every $k\in\mathbb N$ ,

\kappa_k^\mu = \operatorname{TaylorComp}_k\!\left( \operatorname{Taylor}(\log,1), \operatorname{Taylor}\!\left(z\mapsto\int e^{\langle z,x\rangle}\,d\mu(x),0\right) \right).

In Lean this is the equality between cumulant μ k and FormalMultilinearSeries.taylorComp applied to the indicated ftaylorSeriesWithin objects. The statement is conditional on one positive exponential moment and applies to all orders $k$ .

Original Lean declaration header

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

theorem cumulant_eq_taylorComp_cond (μ : Measure E) [IsProbabilityMeasure μ] {r : ℝ} (hr : 0 < r)
    (hexp : Integrable (fun x => Real.exp (r * ‖x‖)) μ) (k : ℕ) :
    cumulant μ k = (ftaylorSeriesWithin ℝ Real.log {0}ᶜ 1).taylorComp
      (ftaylorSeriesWithin ℝ (fun z => ∫ x, Real.exp ⟪z, x⟫ ∂μ) (Metric.ball 0 r) 0) k

Module navigation

Module: Analysis/BakryEmery/Cumulant/Truncation.

Definition modules: Analysis/BakryEmery/Cumulant/Basic.

Previous: tendsto_iteratedFDeriv_laplace_cond_closedBall · Next: tendsto_cumulant_cond_closedBall.

Source excerpt, lines 159–162 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Cumulant_Truncation

open MeasureTheory ProbabilityTheory 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_eq_taylorComp_cond_readable (μ : Measure E) [IsProbabilityMeasure μ] {r : ℝ} (hr : 0 < r)
    (hexp : Integrable (fun x => Real.exp (r * ‖x‖)) μ) (k : ℕ) :
    cumulant μ k = (ftaylorSeriesWithin ℝ Real.log {0}ᶜ 1).taylorComp
      (ftaylorSeriesWithin ℝ (fun z => ∫ x, Real.exp ⟪z, x⟫ ∂μ) (Metric.ball 0 r) 0) k := by sorry

Source

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

View graph