Left Semigroup Derivative on Positive Times

This is the left derivative formula for a generated semigroup orbit.

Let $H_0,H_1$ be complete real Hilbert spaces, let $T:H_0\to H_1$ be closed with dense domain, let $A=T^\dagger T$, and let $f\in D(A)$. For $t>0$, the function $s\mapsto P_s f$ has a derivative at $t$ from the set $(-\infty,t]$:

Formally, HasDerivWithinAt is taken on Iic t, and the derivative is represented using the domain witness that $P_t f\in D(A)$. This is a one-sided derivative statement, not an unrestricted derivative assertion.

Original Lean declaration header

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

theorem hasDerivWithinAt_apply_Iic (f : (adjointComp T).domain) {t : ℝ} (ht : 0 < t) :
    HasDerivWithinAt (fun s => apply T hT hd s f)
      (-adjointComp T ⟨apply T hT hd t f, preserves_domain T hT hd f ht.le⟩) (Iic t) t

Module navigation

Module: Analysis/Semigroup/Generated/TimeDerivative.

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

Supporting theorems: continuousOn.

Next: hasDerivAt_apply_of_pos.

Source excerpt, lines 79–81 · Frozen source 408915f.