Ergodic Decay Of The Centered Heat Evolution

This statement proves ergodicity of the heat semigroup in centered norm.

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

Here $P_t$ is the semigroup generated by the closed weighted gradient operator.

This supplies the ergodicity hypothesis required by the curvature-to-Poincaré interface and applies to every $L^2(\nu)$ input, not only operator-domain inputs.

Formalization Note. The limit is formulated as a filter limit along real $t\to+\infty$; the conclusion concerns the norm of the centered class.

Original Lean declaration header

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

theorem tendsto_norm_center_apply (u : Lp ℝ 2 (ν : Measure V)) :
    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)

Module navigation

Module: KLS/LogConcave/HeatSemigroup/Curvature.

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

Supporting theorems: mem_closure_range_of_inner_eq_zero, tendsto_apply_of_mem_closure_range, closedWeightedOperator_one_eq_zero, inner_center_eq_zero_of_closedWeightedOperator_eq_zero.

Previous: inner_center_eq_zero_of_closedWeightedOperator_eq_zero.

Source excerpt, lines 572–577 · Frozen source 408915f.