Second Cumulant as a Centered Second Moment

Proved

FunctionalInequalities.Analysis.BakryEmery.cumulant_two_eq_centered_moment_of_integrable_exp_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This gives the covariance formula for the second cumulant.

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.

For every $u,v\in E$ ,

\kappa_2^\mu(u,v) = \int\langle u,x\rangle\langle v,x\rangle\,d\mu(x) - \left(\int\langle u,x\rangle\,d\mu(x)\right) \left(\int\langle v,x\rangle\,d\mu(x)\right).

Thus the second cumulant is the centered second-moment or covariance pairing. The statement requires no centering assumption, only one positive exponential moment.

Original Lean declaration header

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

theorem cumulant_two_eq_centered_moment_of_integrable_exp (μ : Measure E) [IsProbabilityMeasure μ]
    {r : ℝ} (hr : 0 < r) (hexp : Integrable (fun x => Real.exp (r * ‖x‖)) μ) (u v : E) :
    cumulant μ 2 ![u, v] =
      (∫ x, ⟪u, x⟫ * ⟪v, x⟫ ∂μ) - (∫ x, ⟪u, x⟫ ∂μ) * (∫ x, ⟪v, 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: sum_sq_cumulant_three_le_of_letwin_of_integrable_exp_basis · Next: iteratedFDeriv_centeredGradient_logLaplace_zero_of_compact.

Source excerpt, lines 386–389 · 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_two_eq_centered_moment_of_integrable_exp_readable (μ : Measure E) [IsProbabilityMeasure μ]
    {r : ℝ} (hr : 0 < r) (hexp : Integrable (fun x => Real.exp (r * ‖x‖)) μ) (u v : E) :
    cumulant μ 2 ![u, v] =
      (∫ x, ⟪u, x⟫ * ⟪v, x⟫ ∂μ) - (∫ x, ⟪u, x⟫ ∂μ) * (∫ x, ⟪v, x⟫ ∂μ) := by sorry

Source

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

View graph