Cumulant Energy Generator Lower Bound

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

Let $\mu$ be an isotropic, compactly supported, log-concave probability measure on $\mathrm{EuclideanSpace}\,\mathbb R\,(\mathrm{Fin}\,n)$. Assume the compact cumulant bound CumulantBoundCompact 2 8. Let $r\ge2$, let $u$ be a direction, and let $p=(c,Q)$ be a localization parameter. Assume $Q$ is self-adjoint and positive semidefinite: $\langle Qx,x\rangle\ge0$ for every $x$.

Writing $E_r=\operatorname{cumulantEnergy}(\mu_p,r,u)$ and $L_r$ for the displayed lower-drift pairing, the conclusion is

More explicitly, $L_r$ is the finite sum over $K:\mathrm{Fin}(r)\to\mathrm{Fin}(n)$ of the $(r+1)$st cumulant evaluated on $u$ and the whitened basis directions, multiplied by lowerDrift at slot $0$. This is a quantitative auxiliary inequality with the explicit constant $17$.

Original Lean declaration header

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

theorem generator_cumulantEnergy_ge (hiso : KLS.Isotropic μ) (hLC : KLS.LogConcave μ)
    (h8 : LogConcave.Suspension.CumulantBoundCompact 2 8) {r : ℕ} (hr : 2 ≤ r)
    (u : EuclideanSpace ℝ (Fin n)) (p : Param n) (hSym : IsSelfAdjoint p.2) (hQ : ∀ x, 0 ≤ ⟪p.2 x, x⟫) :
    (1 / 2 : ℝ) * cumulantEnergy (compactPosterior μ hc p.1 p.2 : Measure (EuclideanSpace ℝ (Fin n))) (r + 1) u
        - 17 * ((r : ℝ) + 1) ^ 2 *
          cumulantEnergy (compactPosterior μ hc p.1 p.2 : Measure (EuclideanSpace ℝ (Fin n))) r u
        - 2 * ∑ K : Fin r → Fin n,
            cumulant (compactPosterior μ hc p.1 p.2 : Measure (EuclideanSpace ℝ (Fin n))) (r + 1)
                (Fin.cons u fun s => inverseSqrt (cov μ hc p) (EuclideanSpace.basisFun (Fin n) ℝ (K s))) *
              lowerDrift (compactPosterior μ hc p.1 p.2 : Measure (EuclideanSpace ℝ (Fin n)))
                (Fin.cons u fun s => inverseSqrt (cov μ hc p) (EuclideanSpace.basisFun (Fin n) ℝ (K s))) 0 ≤
      generator μ hc
        (fun q : Param n => cumulantEnergy (compactPosterior μ hc q.1 q.2 : Measure (EuclideanSpace ℝ (Fin n))) r u) p

Module navigation

Module: KLS/BKL/Localization/Energy/Generator.

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

Selected supporting theorems: contDiffAt_energyForm, deriv_deriv_energyForm_line, drift_expression_ge, fderiv_fderiv_apply_eq_deriv_deriv_line, hasDerivAt_energyForm_line.

Previous: generator_cumulantEnergy_eq.

Source excerpt, lines 497–509 · Frozen source 408915f.