Differentiating a semigroup resolvent in the spectral parameter

The Laplace-transform resolvent R(lambda) x = ∫₀^∞ e^{-lambda t} S(t)x dt of a C₀-semigroup S with growth bound (omega, M) is defined for lambda > omega, and it carries the proof omega < lambda as an argument; StronglyContinuousSemigroup.resolventFun packages it as an honest function of lambda, extended by the junk value 0 below the growth exponent.

The resolvent identity then upgrades to a second-order expansion

R(mu) - R(lambda) + (mu - lambda) R(lambda)² = (mu - lambda)² R(lambda)² R(mu),

whose right-hand side is O((mu - lambda)²) because ‖R(mu)‖ ≤ M / (mu - omega) stays bounded near lambda. Hence lambda ↦ R(lambda) is differentiable in operator norm with

R'(lambda) = -R(lambda)²,

and inductively dᵏR(lambda)/dlambdaᵏ = (-1)ᵏ k! R(lambda)^{k+1}; in particular the resolvent is smooth on (omega, ∞).

Main results

• TauCeti.Semigroups.StronglyContinuousSemigroup.hasDerivAt_resolventFun: R'(lambda) = -R(lambda)².
• TauCeti.Semigroups.StronglyContinuousSemigroup.hasDerivAt_resolventFun_pow: the derivative of lambda ↦ R(lambda)ⁿ is -n R(lambda)ⁿ⁺¹.
• TauCeti.Semigroups.StronglyContinuousSemigroup.iteratedDeriv_resolventFun: dᵏR(lambda)/dlambdaᵏ = (-1)ᵏ k! R(lambda)^{k+1}.
• TauCeti.Semigroups.StronglyContinuousSemigroup.contDiffOn_resolventFun: the resolvent is smooth on (omega, ∞).

The contraction case (omega, M) = (0, 1) is recorded as a corollary.

Implementation notes

Mathlib's spectrum.hasDerivAt_resolvent_const_left proves the same derivative formula for the resolvent of an element of a Banach algebra. It does not apply here: the generator of a C₀-semigroup need not be bounded (it is a densely defined operator on a subspace, and is bounded exactly for the uniformly continuous semigroups), so in general there is no algebra element a with R(lambda) = resolvent a lambda. The present proof therefore runs off the semigroup resolvent identity instead of off differentiability of Ring.inverse.

References

Engel--Nagel, One-Parameter Semigroups for Linear Evolution Equations, Theorem II.1.10 and Corollary IV.1.3; Pazy, Semigroups of Linear Operators and Applications to PDE, Chapter 1.

The first derivative

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.hasDerivAt_resolventFun {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {omega M : ℝ} (hb : S.HasGrowthBound omega M) {lambda : ℝ} (hl : omega < lambda) : HasDerivAt (S.resolventFun hb) (-S.resolventFun hb lambda ^ 2) lambda

The resolvent is differentiable in the spectral parameter, with derivative -R(lambda)² taken in the operator norm. This is the semigroup analogue of Mathlib's spectrum.hasDerivAt_resolvent_const_left, proved from the resolvent identity because the generator need not be a bounded operator.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.deriv_resolventFun {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {omega M : ℝ} (hb : S.HasGrowthBound omega M) {lambda : ℝ} (hl : omega < lambda) : deriv (S.resolventFun hb) lambda = -S.resolventFun hb lambda ^ 2

The derivative of the resolvent in the spectral parameter.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.differentiableOn_resolventFun {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {omega M : ℝ} (hb : S.HasGrowthBound omega M) : DifferentiableOn ℝ (S.resolventFun hb) (Set.Ioi omega)

The resolvent is differentiable on the half-line above the growth exponent.

Higher derivatives

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.hasDerivAt_resolventFun_pow {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {omega M : ℝ} (hb : S.HasGrowthBound omega M) {lambda : ℝ} (hl : omega < lambda) (n : ℕ) : HasDerivAt (fun (l : ℝ) => S.resolventFun hb l ^ n) (-(n • S.resolventFun hb lambda ^ (n + 1))) lambda

The derivative of lambda ↦ R(lambda)ⁿ is -n R(lambda)ⁿ⁺¹.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.iteratedDeriv_resolventFun {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {omega M : ℝ} (hb : S.HasGrowthBound omega M) (n : ℕ) {lambda : ℝ} (hl : omega < lambda) : iteratedDeriv n (S.resolventFun hb) lambda = ((-1) ^ n * ↑n.factorial) • S.resolventFun hb lambda ^ (n + 1)

The iterated derivative of the resolvent: dⁿR(lambda)/dlambdaⁿ = (-1)ⁿ n! R(lambda)ⁿ⁺¹.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.contDiffOn_resolventFun {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {omega M : ℝ} (hb : S.HasGrowthBound omega M) : ContDiffOn ℝ (↑⊤) (S.resolventFun hb) (Set.Ioi omega)

The resolvent is smooth on the half-line above the growth exponent.

The contraction case

theorem TauCeti.Semigroups.ContractionSemigroup.hasDerivAt_resolventFun {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : ContractionSemigroup X) {lambda : ℝ} (h : 0 < lambda) : HasDerivAt S.resolventFun (-S.resolventFun lambda ^ 2) lambda

The derivative of the contraction resolvent is -R(lambda)².

theorem TauCeti.Semigroups.ContractionSemigroup.iteratedDeriv_resolventFun {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : ContractionSemigroup X) (n : ℕ) {lambda : ℝ} (h : 0 < lambda) : iteratedDeriv n S.resolventFun lambda = ((-1) ^ n * ↑n.factorial) • S.resolventFun lambda ^ (n + 1)

The iterated derivative of the contraction resolvent.

theorem TauCeti.Semigroups.ContractionSemigroup.contDiffOn_resolventFun {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : ContractionSemigroup X) : ContDiffOn ℝ (↑⊤) S.resolventFun (Set.Ioi 0)

The contraction resolvent is smooth on (0, ∞).