Singleton Cumulant Allocation Identity

This formalizes the singleton allocation identity in Theorem 4.1 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), cited at p. 21.

Let $E$ be a finite-dimensional real inner-product space and let $\mu$ be a compactly supported probability measure on $E$. Assume that the covariance operator $A=\operatorname{Cov}(\mu)$ is a unit in the relevant operator ring, so that $A^{-1}$ is available. For every finite list $h_s$ in $E$ and every $w\in E$,

In Lean, the cumulant vectors are represented by cumulantVector, the covariance operator by Covariance.operator, and the inverse by Ring.inverse. The statement is a reusable reduction of a covariance-inverse pairing to a higher cumulant.

Original Lean declaration header

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

theorem inner_cumulantVector_single_ringInverse_cumulantVector (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) (hA : IsUnit (Covariance.operator (μ : Measure E)))
    (hs : List E) (w : E) :
    ⟪cumulantVector (μ : Measure E) [w],
        Ring.inverse (Covariance.operator (μ : Measure E)) (cumulantVector (μ : Measure E) hs)⟫ =
      cumulant (μ : Measure E) (hs.length + 1) (Fin.snoc (fun i => hs.get i) w)

Module navigation

Module: Analysis/BakryEmery/Cumulant/Local.

Definition modules: Probability/Covariance/Basic, Analysis/BakryEmery/Cumulant/Basic.

Supporting theorems: cumulant_two_eq_centered_moment_of_integrable_exp, memLp_of_polynomial_bound_of_integrable_exp.

Previous: iteratedFDeriv_centeredGradient_logLaplace_zero_of_compact.

Source excerpt, lines 660–665 · Frozen source 408915f.