Taylor-Coefficient Criterion For The Poincaré Constant

Let $V$ be finite-dimensional, let $\nu$ be log-concave with nonempty support interior, and let $m$ be an additive Haar measure. Let $U:V\to\mathbb R$ have temperate growth and satisfy

$$\nu=m.\operatorname{tilted}(-U),$$

with all exponential moments finite. Assume:

1. $U$ has Hessian lower bound $D^2U(x)[v,v]\ge a\|v\|^2$ for some $a>0$ and all $x,v$;
2. $\int\langle v,x\rangle^2\,d\nu(x)\le\|v\|^2$ for every $v\in V$;
3. $R\ge1$; and
4. for every $u\in L^2(\nu)$ and every $d\ge1$, the Taylor bound

$$\|T_du\|\le R^d\|u\|$$

holds in the standard-basis Hilbert–Schmidt norm.

Then

$$C_P(\nu)\le\operatorname{ofReal}(K R^2),$$

where $K$ is taylorCriterionConstant.

This is the principal criterion converting uniform Taylor-coefficient control into a Poincaré bound under the stated heat-model hypotheses. It is a finite-dimensional, measure-specific implication rather than a dimension-free universal assertion.

Formalization Note. The conclusion is an ENNReal inequality, expressed using ENNReal.ofReal; the covariance condition is stated without an explicit centering assumption.

Original Lean declaration header

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

theorem taylorCriterion
    (hνU : (ν : Measure V) = m.tilted (-U)) (hU : U.HasTemperateGrowth)
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) (ν : Measure V))
    {a : ℝ} (ha : 0 < a) (hUa : ∀ x v, a * ‖v‖ ^ 2 ≤ bilinearIteratedFDerivTwo ℝ U x v v)
    (hcov : ∀ v : V, ∫ x, ⟪v, x⟫ ^ 2 ∂(ν : Measure V) ≤ ‖v‖ ^ 2)
    {R : ℝ} (hR : 1 ≤ R)
    (h29 : ∀ (u : Lp ℝ 2 (ν : Measure V)) (d : ℕ), 1 ≤ d →
      ‖coordTensor (stdOrthonormalBasis ℝ V) (taylorTensor (ν : Measure V) (⇑u) d)‖ ≤
        R ^ d * ‖u‖) :
    Poincare.LocalSlope.Intrinsic.constant ν ≤
      ENNReal.ofReal (taylorCriterionConstant * R ^ 2)

Module navigation

Module: KLS/BKL/PoissonIterate/Criterion.

Definition modules: Analysis/Tensor/Coefficients, Analysis/Tensor/Coordinate, Probability/LogConcave, Analysis/BakryEmery/Tilt/Basic, Poincare/LocalSlope/Basic.

Selected supporting theorems: integral_hessianSq_add_le_of_hasTemperateGrowth, summable_and_tendsto_zero_of_energy, taylorTensor_const_mul, inv_le_scale_sq_step, le_of_iterate_bounds.

Previous: norm_taylorField_sq_le.

Source excerpt, lines 489–499 · Frozen source 408915f.

Literature

This formalizes Theorem 3.1 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), p. 10.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_Criterion

open MeasureTheory Filter Topology Finset
open FunctionalInequalities.Analysis.Semigroup FunctionalInequalities.Analysis.BakryEmery
open FunctionalInequalities.Analysis.Tensor
open scoped ENNReal NNReal RealInnerProductSpace InnerProductSpace ContDiff
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
  {ν : MeasureTheory.ProbabilityMeasure V} (m : MeasureTheory.Measure V) [m.IsAddHaarMeasure] (hν : FunctionalInequalities.KLS.LogConcave ν)
  (hi : (interior (ν : MeasureTheory.Measure V).support).Nonempty) {U : V → ℝ}
local notation "T̄" => hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi
include hν hi

theorem FunctionalInequalities.KLS.LogConcave.PoissonIterate.taylorCriterion_readable
    (hνU : (ν : Measure V) = m.tilted (-U)) (hU : U.HasTemperateGrowth)
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) (ν : Measure V))
    {a : ℝ} (ha : 0 < a) (hUa : ∀ x v, a * ‖v‖ ^ 2 ≤ bilinearIteratedFDerivTwo ℝ U x v v)
    (hcov : ∀ v : V, ∫ x, ⟪v, x⟫ ^ 2 ∂(ν : Measure V) ≤ ‖v‖ ^ 2)
    {R : ℝ} (hR : 1 ≤ R)
    (h29 : ∀ (u : Lp ℝ 2 (ν : Measure V)) (d : ℕ), 1 ≤ d →
      ‖coordTensor (stdOrthonormalBasis ℝ V) (taylorTensor (ν : Measure V) (⇑u) d)‖ ≤
        R ^ d * ‖u‖) :
    Poincare.LocalSlope.Intrinsic.constant ν ≤
      ENNReal.ofReal (taylorCriterionConstant * R ^ 2) := by sorry