Poincaré Bound From Curvature And Ergodicity

This formalizes the ergodic-interface form of Proposition 4.8.1 of Bakry–Gentil–Ledoux (2014), p. 212.

Let $V$, $\nu$, $m$, and $U$ satisfy the heat-model assumptions, with $\nu=m.\operatorname{tilted}(-U)$ and $U\in C^2$. Let $\rho>0$ satisfy

$$\rho\|v\|^2\le D^2U(x)[v,v]\qquad(x,v\in V).$$

Assume that for every $u\in D(\overline{\nabla})$, the centered heat evolution converges in norm:

$$\|\operatorname{center}_\nu(P_tu)\|\longrightarrow0\qquad(t\to\infty).$$

Then

$$C_P(\nu)\le\operatorname{ofReal}(\rho^{-1}).$$

This declaration isolates the passage from a finite-time curvature estimate and an explicit ergodicity hypothesis to the Poincaré constant bound.

Formalization Note. The conclusion is in ENNReal; ENNReal.ofReal is applied to the real number $\rho^{-1}$.

Original Lean declaration header

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

theorem literatureConstant_le_inv_of_tendsto {ρ : ℝ} (hρ : 0 < ρ)
    (hH : ∀ x v, ρ * ‖v‖ ^ 2 ≤ bilinearIteratedFDerivTwo ℝ U x v v)
    (herg : ∀ u : (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain,
      Tendsto (fun t : ℝ => ‖L2.center ν (Generated.apply
        (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi)
        (hν.closedWeightedOperator_isClosed m (ContinuousLinearMap.id ℝ V) hi)
        (hν.dense_domain_closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi) t u)‖)
        atTop (𝓝 0)) :
    Poincare.LocalSlope.Intrinsic.constant ν ≤ ENNReal.ofReal ρ⁻¹

Module navigation

Module: KLS/LogConcave/HeatSemigroup/Curvature.

Definition modules: KLS/LogConcave/WeightedGradient/Closure, Probability/LogConcave, Poincare/LocalSlope/Basic, Analysis/Semigroup/Generated/Basic, L2/MeanVariance.

Supporting theorems: literatureConstant_le_of_gap, norm_center_sq_sub_le.

Previous: literatureConstant_le_of_gap · Next: closedWeightedOperator_eq_zero_iff.

Source excerpt, lines 400–408 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Curvature

open MeasureTheory Filter Topology InnerProductSpace
open FunctionalInequalities.Analysis.Semigroup FunctionalInequalities.Analysis.BakryEmery
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 → ℝ}
  (hνU : (ν : MeasureTheory.Measure V) = m.tilted (-U)) (hU : ContDiff ℝ 2 U)
include hνU hU

theorem FunctionalInequalities.KLS.LogConcave.literatureConstant_le_inv_of_tendsto_readable {ρ : ℝ} (hρ : 0 < ρ)
    (hH : ∀ x v, ρ * ‖v‖ ^ 2 ≤ bilinearIteratedFDerivTwo ℝ U x v v)
    (herg : ∀ u : (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain,
      Tendsto (fun t : ℝ => ‖L2.center ν (Generated.apply
        (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi)
        (hν.closedWeightedOperator_isClosed m (ContinuousLinearMap.id ℝ V) hi)
        (hν.dense_domain_closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi) t u)‖)
        atTop (𝓝 0)) :
    Poincare.LocalSlope.Intrinsic.constant ν ≤ ENNReal.ofReal ρ⁻¹ := by sorry