Finite-Time Poincaré Energy Bound

In an abstract semigroup setting, this formalizes Proposition 4.8.1 (Poincaré inequality under CD($\rho,\infty$)) of Bakry–Gentil–Ledoux (2014), p. 212.

Let $H_0,H_1$ be real complete inner-product spaces, let $T:H_0\to H_1$ be closed with dense domain, and write $A=T^\dagger T$. Assume:

1. $\rho>0$.
2. For every $y\in D(A)$, $\rho\|Ty\|^2\le\|Ay\|^2$.
3. $f\in D(T)$ and $t\ge0$.

Then

This is the finite-time energy form of the Poincaré estimate; it does not assert a limiting or ergodic statement.

Formalization Note. The semigroup is Generated.apply T hT hd; all quantities in this declaration are real norms, and the bound explicitly requires $\rho>0$.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis.Semigroup.Generated. Shown in its original module context. Proof omitted.

theorem norm_sq_sub_norm_apply_sq_le {ρ : ℝ} (hρ : 0 < ρ)
    (hcurv : ∀ y : (adjointComp T).domain, ρ * ‖T ⟨y, y.2.2⟩‖ ^ 2 ≤ ‖adjointComp T y‖ ^ 2)
    (f : T.domain) {t : ℝ} (ht : 0 ≤ t) :
    ‖(f : H₀)‖ ^ 2 - ‖apply T hT hd t f‖ ^ 2 ≤
      (1 - Real.exp (-2 * ρ * t)) / ρ * ‖T f‖ ^ 2

Module navigation

Module: Analysis/Semigroup/Generated/Curvature.

Definition modules: Analysis/Semigroup/AdjointComp, Analysis/Semigroup/Generated/Basic.

Supporting theorems: continuousOn, hasDerivAt_apply_of_pos, norm_map_apply_sq_le_exp.

Previous: norm_map_apply_sq_le_exp.

Source excerpt, lines 431–435 · Frozen source 408915f.