Semigroup Orbit Derivative at Positive Times

This is the classical derivative formula for the generated semigroup orbit at positive times.

Let $H_0,H_1$ be complete real Hilbert spaces, let $T:H_0\to H_1$ be closed with dense domain, and let $A=T^\dagger T$. For arbitrary $g\in H_0$ and every $t>0$, the orbit $s\mapsto P_s g$ is differentiable at $t$ and

The type asserts HasDerivAt at each strictly positive time and includes the domain witness establishing $P_tg\in D(A)$. No differentiability at $t=0$ is claimed.

Original Lean declaration header

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

theorem hasDerivAt_apply_of_pos (g : H₀) {t : ℝ} (ht : 0 < t) :
    HasDerivAt (fun s => apply T hT hd s g)
      (-adjointComp T ⟨apply T hT hd t g, mem_adjointComp_domain_apply_of_pos T hT hd g ht⟩) t

Module navigation

Module: Analysis/Semigroup/Generated/TimeDerivative.

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

Supporting theorems: hasDerivWithinAt_apply_Iic.

Previous: hasDerivWithinAt_apply_Iic.

Source excerpt, lines 330–332 · Frozen source 408915f.