Derivative of the Semigroup Energy Inner Product

This is an auxiliary differentiation identity for a semigroup generated by an operator composition.

Let $H_0$ and $H_1$ be real complete inner-product spaces, let $T$ be a closed linear partial map from $H_0$ to $H_1$, and assume that the domain of $T$ is dense in $H_0$. Write $A=T^\dagger T$ for adjointComp T, let $P_s$ denote Generated.apply T hT hd s, and let $f\in D(A)$. If $s>0$, then the map $r\mapsto\langle P_r(Af),P_r f\rangle$ has derivative at $s$ equal to minus twice the squared norm of $A(P_s f)$:

The identity supplies the differential relation used in energy-decay estimates for the generated semigroup.

Formalization Note. Domain-membership proofs are encoded by subtype terms, and the conclusion is a HasDerivAt statement over real parameters.

Original Lean declaration header

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

theorem hasDerivAt_inner_apply (f : (adjointComp T).domain) {s : ℝ} (hs : 0 < s) :
    HasDerivAt (fun r => ⟪apply T hT hd r (adjointComp T f), apply T hT hd r f⟫)
      (-2 * ‖adjointComp T ⟨apply T hT hd s f, preserves_domain T hT hd f hs.le⟩‖ ^ 2) s

Module navigation

Module: Analysis/Semigroup/Generated/Curvature.

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

Supporting theorems: hasDerivAt_apply_of_pos.

Previous: norm_map_apply_sq_eq_inner · Next: le_exp_mul_of_hasDerivAt_le.

Source excerpt, lines 66–68 · Frozen source 408915f.