Exponential Energy Decay on the Operator Domain

This is the exponential energy estimate under an integrated 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 put $A=T^\dagger T$. Let $\rho\in\mathbb R$ and assume that for every $y\in D(A)$,

$$\rho\,\|Ty\|^2\le \|Ay\|^2.$$

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

$$\|T(P_t f)\|^2\le e^{-2\rho t}\,\|Tf\|^2,$$

where $P_t$ is Generated.apply T hT hd t.

This is the domain-level energy-decay estimate from which the estimate on the whole form domain is obtained.

Formalization Note. The parameter $\rho$ is only assumed real; no positivity hypothesis on $\rho$ appears in the type.

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_of_mem_adjointComp {ρ : ℝ}
    (hcurv : ∀ y : (adjointComp T).domain, ρ * ‖T ⟨y, y.2.2⟩‖ ^ 2 ≤ ‖adjointComp T y‖ ^ 2)
    (f : (adjointComp T).domain) {t : ℝ} (ht : 0 ≤ t) :
    ‖T ⟨apply T hT hd t f, (preserves_domain T hT hd f ht).2⟩‖ ^ 2 ≤
      Real.exp (-2 * ρ * t) * ‖T ⟨f, f.2.2⟩‖ ^ 2

Module navigation

Module: Analysis/Semigroup/Generated/Curvature.

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

Supporting theorems: continuousOn, hasDerivAt_inner_apply, le_exp_mul_of_hasDerivAt_le, norm_map_apply_sq_eq_inner.

Previous: le_exp_mul_of_hasDerivAt_le · Next: norm_map_apply_sq_le_exp.

Source excerpt, lines 226–230 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Semigroup_Generated_Curvature

variable {H₀ H₁ : Type*} [NormedAddCommGroup H₀] [InnerProductSpace ℝ H₀] [CompleteSpace H₀]
  [NormedAddCommGroup H₁] [InnerProductSpace ℝ H₁] [CompleteSpace H₁]
  (T : H₀ →ₗ.[ℝ] H₁) (hT : T.IsClosed) (hd : Dense (T.domain : Set H₀))

theorem FunctionalInequalities.Analysis.Semigroup.Generated.norm_map_apply_sq_le_exp_of_mem_adjointComp_readable {ρ : ℝ}
    (hcurv : ∀ y : (adjointComp T).domain, ρ * ‖T ⟨y, y.2.2⟩‖ ^ 2 ≤ ‖adjointComp T y‖ ^ 2)
    (f : (adjointComp T).domain) {t : ℝ} (ht : 0 ≤ t) :
    ‖T ⟨apply T hT hd t f, (preserves_domain T hT hd f ht).2⟩‖ ^ 2 ≤
      Real.exp (-2 * ρ * t) * ‖T ⟨f, f.2.2⟩‖ ^ 2 := by sorry