Standardized Compact Posterior Cumulant Bound

This formalizes the standardized posterior cumulant estimate associated with Theorem 4.1 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), cited there as an alternative formulation of the cumulant bounds.

Work in $E=\operatorname{EuclideanSpace}(\mathbb{R},\operatorname{Fin}n)$. Let $\mu$ be a compactly supported isotropic log-concave probability law. Let $c\in E$ and let $Q:E\to E$ be self-adjoint and positive semidefinite. Put

Assume $d\ge1$, assume CumulantBoundCompact d b, and let $v\in E$. Then

where $(e_j)$ is the standard orthonormal basis and $\kappa_{d+1}$ is cumulant of the posterior measure.

The result transfers a compact cumulant bound for the standardized posterior back to the original posterior, with the covariance quadratic form on the right-hand side. It is stated in every finite dimension, including $n=0$.

Original Lean declaration header

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

theorem compactPosterior_cumulant_bound {n : ℕ}
    (μ : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
    (hc : IsCompact (μ : Measure (EuclideanSpace ℝ (Fin n))).support)
    (hiso : KLS.Isotropic μ) (hLC : KLS.LogConcave μ)
    (c : EuclideanSpace ℝ (Fin n)) (Q : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n))
    (hSym : IsSelfAdjoint Q) (hQ : ∀ x, 0 ≤ ⟪Q x, x⟫)
    {d : ℕ} (hd : 1 ≤ d) {b : ℝ} (h : LogConcave.Suspension.CumulantBoundCompact d b)
    (v : EuclideanSpace ℝ (Fin n)) :
    ∑ J : Fin d → Fin n,
        cumulant (compactPosterior μ hc c Q : Measure (EuclideanSpace ℝ (Fin n))) (d + 1)
          (Fin.cons v fun k => inverseSqrt (Covariance.operator
            (compactPosterior μ hc c Q : Measure (EuclideanSpace ℝ (Fin n))))
              (EuclideanSpace.basisFun (Fin n) ℝ (J k))) ^ 2 ≤
      b * ⟪Covariance.operator (compactPosterior μ hc c Q : Measure (EuclideanSpace ℝ (Fin n))) v, v⟫

Module navigation

Module: KLS/BKL/Localization/Standardization.

Definition modules: Probability/Covariance/Basic, Probability/LogConcave, KLS/Isotropic, Analysis/Operator/InverseSqrt, Analysis/BakryEmery/Cumulant/Basic, Probability/Posterior/CompactDomain, KLS/BKL/CompactReduction.

Selected supporting theorems: cumulant_map_affine, inverseSqrt_mul_mul_inverseSqrt, Covariance.inner_operator_self_pos_of_affineSupport_eq_top, Isotropic.exists_inverseSqrt_equiv_isotropic_standardized, logConcave_of_concave_tilt.

Source excerpt, lines 26–39 · Frozen source 408915f.