Posterior Cumulant Generator Identity

This formalizes the generator form of BKL Lemma 4.3, equation (73), cited at p. 20 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).

Let $\mu$ be an isotropic probability measure on $\mathrm{EuclideanSpace}\,\mathbb R\,(\mathrm{Fin}\,n)$ with compact support. Let $m\in\mathbb N$ satisfy $3\le m$, let $h:\mathrm{Fin}(m)\to\mathrm{EuclideanSpace}\,\mathbb R\,(\mathrm{Fin}\,n)$ be a family of directions, let $i_0\in\mathrm{Fin}(m)$, and let $p$ be a localization parameter. For each parameter $q$, evaluate the $m$th cumulant of the compact posterior at $q$ on $h$.

Then

where lowerDrift is the middle-term contribution at slot $i_0$. The theorem is an auxiliary pointwise identity for posterior cumulants and is used in generator-based energy estimates.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.BKL.Localization. Shown in its original module context. Proof omitted.

theorem generator_cumulant_posterior (hiso : KLS.Isotropic μ) {m : ℕ} (hm : 3 ≤ m)
    (h : Fin m → EuclideanSpace ℝ (Fin n)) (i₀ : Fin m) (p : Param n) :
    generator μ hc
        (fun q : Param n => cumulant (compactPosterior μ hc q.1 q.2 : Measure (EuclideanSpace ℝ (Fin n))) m h) p =
      -((m : ℝ) * cumulant (compactPosterior μ hc p.1 p.2 : Measure (EuclideanSpace ℝ (Fin n))) m h +
        lowerDrift (compactPosterior μ hc p.1 p.2 : Measure (EuclideanSpace ℝ (Fin n))) h i₀)

Module navigation

Module: KLS/BKL/Localization/CumulantGenerator.

Definition modules: KLS/BKL/Localization/Coefficients, KLS/Isotropic, KLS/BKL/CumulantEnergy/Basic, Analysis/BakryEmery/Cumulant/Basic, Probability/Posterior/CompactDomain.

Selected supporting theorems: iteratedFDeriv_inner_centeredGradient_zero_grouped_of_compact, Covariance.inner_operator_self_pos_of_affineSupport_eq_top, generator_logLaplace_posterior, contDiff_logPartition_joint, fderiv_logPartition_c_apply.

Source excerpt, lines 225–230 · Frozen source 408915f.