Poincaré Bound for Isotropic Regular Laws

This formalizes the regular-law part of the Bizeul–Klartag–Lehec reduction described on p. 30; it is conditional on the cumulant bounds used there.

There exists a real constant $C>0$ such that, for every $K\in\mathbb R$ with $1\le K$, the following implication holds: if, for every $d\in\mathbb N$ with $2\le d$, CumulantBound d ((d!)² K^d) holds, then for every $n\in\mathbb N$, every $V:\operatorname{EuclideanSpace}(\mathbb R,\operatorname{Fin} n)\to\mathbb R$, every $a,b\in\mathbb R$, and every regular potential $hV : KLS.RegularPotential V a b$ whose law is isotropic,

Here Poincare.LocalSlope.Intrinsic.constant is the Poincaré constant used by the formalization, with values in $[0,\infty]$.

This declaration supplies the regular finite-dimensional estimate that is later extended from regular laws to arbitrary finite-dimensional isotropic log-concave probability measures.

Formalization Note: The conclusion is an inequality in ENNReal; the right-hand side is ENNReal.ofReal (2 * C * K). No universal cumulant bound is discharged by this declaration.

Original Lean declaration header

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

theorem poincare_le_of_cumulantBound :
    ∃ C : ℝ, 0 < C ∧ ∀ K : ℝ, 1 ≤ K →
      (∀ d : ℕ, 2 ≤ d → CumulantBound d ((d.factorial : ℝ) ^ 2 * K ^ d)) →
      ∀ (n : ℕ) (V : EuclideanSpace ℝ (Fin n) → ℝ) (a b : ℝ) (hV : KLS.RegularPotential V a b),
        KLS.Isotropic hV.law →
        Poincare.LocalSlope.Intrinsic.constant hV.law ≤ ENNReal.ofReal (2 * C * K)

Module navigation

Module: KLS/BKL/Reduction.

Definition modules: KLS/BKL/Suspension/Law, KLS/Isotropic, KLS/LogConcave/Regular/Basic, Poincare/LocalSlope/Basic.

Selected supporting theorems: convexOn_of_hessian_ge, sum_coordTensor_sq_eq, Isotropic.norm_coordTensor_taylorTensor_one_le_of_entries, taylorCriterion, norm_coordTensor_taylorTensor_sq_le_two_mul.

Previous: Isotropic.norm_coordTensor_taylorTensor_one_le_of_entries · Next: localSlope_le_of_cumulantBound_all.

Source excerpt, lines 181–186 · Frozen source 408915f.