Convergence of Cumulants Under Ball Conditioning

This formalizes the cumulant-convergence reduction associated with Theorem 4.1 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), p. 18.

Let $E$ be a complete finite-dimensional real inner-product space with its Borel measurable structure, and let $\nu$ be a probability measure on $E$. Assume:

1. $r>0$.
2. $\int e^{r\|x\|}\,d\nu(x)<\infty$.
3. $k\in\mathbb N$.

For the conditional probability measure $\nu[\mid\overline B(0,R)]$ on the closed ball of radius $R$, its $k$th cumulant converges to the $k$th cumulant of $\nu$:

The result is a technical truncation theorem that permits passage from compactly supported conditional laws to the original law in fixed cumulant order.

Formalization Note cumulant is a formal multilinear-series object. The conditioning is Lean's ProbabilityTheory.cond on Metric.closedBall (0 : E) R; the limit parameter is $R\in\mathbb N$.

Original Lean declaration header

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

theorem tendsto_cumulant_cond_closedBall {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (ν : Measure E) [IsProbabilityMeasure ν] {r : ℝ} (hr : 0 < r)
    (hexp : Integrable (fun x => Real.exp (r * ‖x‖)) ν) (k : ℕ) :
    Tendsto (fun R : ℕ => cumulant (ν[|Metric.closedBall (0 : E) R]) k) atTop
      (𝓝 (cumulant ν k))

Module navigation

Module: Analysis/BakryEmery/Cumulant/Truncation.

Definition modules: Analysis/BakryEmery/Cumulant/Basic.

Supporting theorems: cumulant_eq_taylorComp_cond, tendsto_iteratedFDeriv_laplace_cond_closedBall.

Previous: cumulant_eq_taylorComp_cond.

Source excerpt, lines 215–220 · Frozen source 408915f.