Finite-Time Centered Energy Decay

This statement gives the finite-time Poincaré estimate for the heat semigroup.

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).$$

For $u$ in the domain of the closed weighted gradient and $t\ge0$,

$$\|\operatorname{center}_\nu u\|^2- \|\operatorname{center}_\nu(P_tu)\|^2 \le\frac{1-e^{-2\rho t}}{\rho}\,\|\overline{\nabla}u\|^2,$$

where $P_t$ is the heat-semigroup operator.

This estimate measures the decrease of centered $L^2$ energy over finite time and is the dynamical input for the limiting Poincaré bound.

Formalization Note. The assumption $t\ge0$ is explicit, and the displayed expression is an inequality of real numbers.

Original Lean declaration header

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

theorem norm_center_sq_sub_le {ρ : ℝ} (hρ : 0 < ρ)
    (hH : ∀ x v, ρ * ‖v‖ ^ 2 ≤ bilinearIteratedFDerivTwo ℝ U x v v)
    (u : (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain) {t : ℝ}
    (ht : 0 ≤ t) :
    ‖L2.center ν (u : Lp ℝ 2 (ν : Measure V))‖ ^ 2 -
        ‖L2.center ν
          (HeatSemigroup.operator m (ContinuousLinearMap.id ℝ V) hν hi ht u)‖ ^ 2 ≤
      (1 - Real.exp (-2 * ρ * t)) / ρ *
        ‖hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi u‖ ^ 2

Module navigation

Module: KLS/LogConcave/HeatSemigroup/Curvature.

Definition modules: KLS/LogConcave/WeightedGradient/Closure, Probability/LogConcave, KLS/LogConcave/HeatSemigroup/Basic, L2/MeanVariance.

Supporting theorems: norm_sq_sub_norm_apply_sq_le, closedWeightedOperator_center, closedWeightedOperator_one_eq_zero, mul_norm_closedWeightedOperator_sq_le.

Previous: closedWeightedOperator_center · Next: literatureConstant_le_of_gap.

Source excerpt, lines 292–300 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Curvature

open MeasureTheory Filter Topology InnerProductSpace
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.norm_center_sq_sub_le_readable {ρ : ℝ} (hρ : 0 < ρ)
    (hH : ∀ x v, ρ * ‖v‖ ^ 2 ≤ bilinearIteratedFDerivTwo ℝ U x v v)
    (u : (hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi).domain) {t : ℝ}
    (ht : 0 ≤ t) :
    ‖L2.center ν (u : Lp ℝ 2 (ν : Measure V))‖ ^ 2 -
        ‖L2.center ν
          (HeatSemigroup.operator m (ContinuousLinearMap.id ℝ V) hν hi ht u)‖ ^ 2 ≤
      (1 - Real.exp (-2 * ρ * t)) / ρ *
        ‖hν.closedWeightedOperator m (ContinuousLinearMap.id ℝ V) hi u‖ ^ 2 := by sorry