The resolvent of a bounded perturbation of a generator

For a semigroup S of growth (omega, M) and a bounded operator B, the sharp Hille--Yosida bound ‖R(lambda, S.generator)‖ ≤ M / (lambda - omega) makes the perturbation B +ᵥ S.generator small against the resolvent as soon as lambda > omega + M ‖B‖. The Neumann perturbation of a resolvent point (TauCeti.LinearPMap.mem_resolventSet_vadd) then puts every such lambda in the resolvent set of the perturbed generator, with ‖R(lambda, B + S.generator)‖ ≤ M / (lambda - omega - M ‖B‖).

Only the first power of the perturbed resolvent is controlled this way: iterating the Neumann bound costs M ^ n rather than M, so it does not feed Hille--Yosida at M > 1. The general generation theorem instead passes to an equivalent norm, reducing the operator argument to the M = 1 case; see TauCeti/Analysis/Semigroups/Generation/BoundedPerturbation.lean.

Main results

• TauCeti.Semigroups.StronglyContinuousSemigroup.mem_resolventSet_generator_vadd: the resolvent set of the perturbed generator contains (omega + M ‖B‖, ∞).
• TauCeti.Semigroups.StronglyContinuousSemigroup.norm_resolvent_generator_vadd_le: the norm bound for the perturbed generator resolvent.

References

Engel--Nagel, One-Parameter Semigroups for Linear Evolution Equations, Section III.1; Pazy, Semigroups of Linear Operators and Applications to Partial Differential Equations, Chapter 3, Theorem 1.1.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.mem_resolventSet_generator_vadd {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {omega M lambda : ℝ} (S : StronglyContinuousSemigroup X) (hb : S.HasGrowthBound omega M) (B : X →L[ℝ] X) (hlambda : omega + M * ‖B‖ < lambda) : lambda ∈ LinearPMap.resolventSet (↑B +ᵥ S.generator)

The resolvent set of a bounded perturbation of a generator. For a semigroup of growth (omega, M) and a bounded B, every lambda > omega + M ‖B‖ lies in the resolvent set of B +ᵥ S.generator.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.norm_resolvent_generator_vadd_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {omega M lambda : ℝ} (S : StronglyContinuousSemigroup X) (hb : S.HasGrowthBound omega M) (B : X →L[ℝ] X) (hlambda : omega + M * ‖B‖ < lambda) : ‖LinearPMap.resolvent (↑B +ᵥ S.generator) lambda‖ ≤ M / (lambda - omega - M * ‖B‖)

The resolvent bound for a bounded perturbation of a generator. For a semigroup of growth (omega, M) and a bounded B, the resolvent of B +ᵥ S.generator obeys ‖R(lambda, B + S.generator)‖ ≤ M / (lambda - omega - M ‖B‖) for lambda > omega + M ‖B‖.