Exponential Energy Decay on the Form Domain

This is the exponential energy estimate on the full form domain under the curvature bound.

Let $H_0,H_1$ be real complete inner-product spaces, let $T:H_0\to H_1$ be closed with dense domain, and set $A=T^\dagger T$. Let $\rho\in\mathbb R$ and assume

Then for every $f\in D(T)$ and every $t\ge0$,

This extends the decay estimate from $D(A)$ to $D(T)$ and is the principal semigroup energy estimate in this development.

Formalization Note. The conclusion concerns the form domain $D(T)$, while the curvature hypothesis ranges over $D(A)$; $P_t$ is Generated.apply T hT hd t.

Original Lean declaration header

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

theorem norm_map_apply_sq_le_exp {ρ : ℝ}
    (hcurv : ∀ y : (adjointComp T).domain, ρ * ‖T ⟨y, y.2.2⟩‖ ^ 2 ≤ ‖adjointComp T y‖ ^ 2)
    (f : T.domain) {t : ℝ} (ht : 0 ≤ t) :
    ‖T ⟨apply T hT hd t f, preserves_form_domain T hT hd f ht⟩‖ ^ 2 ≤
      Real.exp (-2 * ρ * t) * ‖T f‖ ^ 2

Module navigation

Module: Analysis/Semigroup/Generated/Curvature.

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

Supporting theorems: norm_map_apply_sq_le_exp_of_mem_adjointComp.

Previous: norm_map_apply_sq_le_exp_of_mem_adjointComp · Next: norm_sq_sub_norm_apply_sq_le.

Source excerpt, lines 307–311 · Frozen source 408915f.