Posterior Cumulants as Log-Partition Derivatives

Proved

FunctionalInequalities.Probability.Posterior.cumulant_compactPosterior_readable

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

bkl2026functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes the derivative representation of posterior cumulants used in Lemma 4.3 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), cited there for cumulant dynamics.

Let $E$ be a complete finite-dimensional real inner-product space, let $\mu$ be a compactly supported probability law, let $c\in E$ , let $Q:E\to E$ be continuous linear, and let $m\ge1$ . Then the $m$ th cumulant tensor of the compact posterior equals the $m$ th iterated derivative in the linear parameter $c$ of the log-partition function:

\kappa_m(\mu_{c,Q}) = D_c^m\bigl[y\mapsto\psi(y,Q)\bigr](c).

In Lean, the derivative is iteratedFDeriv ℝ m and the cumulant is Analysis.BakryEmery.cumulant. This identity is the deterministic bridge between posterior cumulants and smooth parameter calculus.

Original Lean declaration header

Within namespace FunctionalInequalities.Probability.Posterior. Shown in its original module context. Proof omitted.

theorem cumulant_compactPosterior (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) (c : E) (Q : E →L[ℝ] E) {m : ℕ} (hm : 1 ≤ m) :
    Analysis.BakryEmery.cumulant (compactPosterior μ hc c Q : Measure E) m =
      iteratedFDeriv ℝ m (fun y => logPartition μ y Q) c

Module navigation

Module: Probability/Posterior/LogPartition.

Definition modules: Analysis/BakryEmery/Cumulant/Basic, Probability/Posterior/CompactDomain.

Supporting theorems: contDiff_logPartition_joint, logLaplace_compactPosterior.

Previous: logLaplace_compactPosterior · Next: fderiv_logPartition_c_apply.

Source excerpt, lines 241–244 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_LogPartition

open MeasureTheory ProbabilityTheory
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]

Formal statement


theorem FunctionalInequalities.Probability.Posterior.cumulant_compactPosterior_readable (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) (c : E) (Q : E →L[ℝ] E) {m : ℕ} (hm : 1 ≤ m) :
    Analysis.BakryEmery.cumulant (compactPosterior μ hc c Q : Measure E) m =
      iteratedFDeriv ℝ m (fun y => logPartition μ y Q) c := by sorry

Source

Source: Bizeul–Klartag–Lehec, Presenting a proof of the Kannan–Lovász–Simonovits conjecture (arXiv:2610.05474v1), Lemma 4.3, p. 20. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/Posterior/LogPartition.lean#L240-L303 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.Posterior.LogPartition`, declaration `FunctionalInequalities.Probability.Posterior.cumulant_compactPosterior`; the repository is private at upload time).

View graph