Bounded perturbations of a resolvent point

Adding a bounded operator B to an unbounded operator A does not change the domain, so the perturbed operator is Mathlib's B +ᵥ A. On D(A) the two operators are related by the factorisation

lambda • I - (B + A) = (I - B R(lambda, A)) (lambda • I - A),

whose first factor is invertible by the geometric series as soon as ‖B‖ ‖R(lambda, A)‖ < 1. This file turns that observation into the three facts a perturbation theorem needs: the resolvent point survives, the perturbed resolvent is R(lambda, A) (I - B R(lambda, A))⁻¹, and it obeys the bound r / (1 - ‖B‖ r).

All the statements take an upper bound r for ‖R(lambda, A)‖ rather than that norm itself, because that is the form in which callers have their information: a semigroup growth bound (omega, M) supplies r = M / (lambda - omega), and the conclusion then reads M / (lambda - omega - M ‖B‖).

Main results

• TauCeti.LinearPMap.isResolventAt_vadd: the perturbed inverse, as an IsResolventAt witness.
• TauCeti.LinearPMap.mem_resolventSet_vadd: a resolvent point survives a bounded perturbation small against the resolvent.
• TauCeti.LinearPMap.resolvent_vadd: the perturbed resolvent in closed form.
• TauCeti.LinearPMap.norm_resolvent_vadd_le: the norm bound for the perturbed 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.LinearPMap.isResolventAt_vadd {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {lambda r : ℝ} (B : X →L[ℝ] X) (h : lambda ∈ resolventSet A) (hr : ‖resolvent A lambda‖ ≤ r) (hB : ‖B‖ * r < 1) : IsResolventAt (↑B +ᵥ A) lambda (resolvent A lambda * Ring.inverse (1 - B * resolvent A lambda))

The inverse of a small bounded perturbation. If lambda lies in the resolvent set of A and the bounded operator B satisfies ‖B‖ * r < 1 for some bound r on ‖R(lambda, A)‖, then R(lambda, A) (I - B R(lambda, A))⁻¹ inverts lambda • I - (B + A).

theorem TauCeti.LinearPMap.mem_resolventSet_vadd {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {lambda r : ℝ} (B : X →L[ℝ] X) (h : lambda ∈ resolventSet A) (hr : ‖resolvent A lambda‖ ≤ r) (hB : ‖B‖ * r < 1) : lambda ∈ resolventSet (↑B +ᵥ A)

A resolvent point survives a small bounded perturbation. If lambda lies in the resolvent set of A and the bounded operator B satisfies ‖B‖ * r < 1 for some bound r on ‖R(lambda, A)‖, then lambda lies in the resolvent set of B +ᵥ A.

theorem TauCeti.LinearPMap.resolvent_vadd {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {lambda r : ℝ} (B : X →L[ℝ] X) (h : lambda ∈ resolventSet A) (hr : ‖resolvent A lambda‖ ≤ r) (hB : ‖B‖ * r < 1) : resolvent (↑B +ᵥ A) lambda = resolvent A lambda * Ring.inverse (1 - B * resolvent A lambda)

The perturbed resolvent in closed form. Under the hypotheses of TauCeti.LinearPMap.mem_resolventSet_vadd, the resolvent of B +ᵥ A is R(lambda, A) (I - B R(lambda, A))⁻¹.

theorem TauCeti.LinearPMap.norm_resolvent_vadd_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {lambda r : ℝ} (B : X →L[ℝ] X) (h : lambda ∈ resolventSet A) (hr : ‖resolvent A lambda‖ ≤ r) (hB : ‖B‖ * r < 1) : ‖resolvent (↑B +ᵥ A) lambda‖ ≤ r / (1 - ‖B‖ * r)

The perturbed resolvent bound. Under the hypotheses of TauCeti.LinearPMap.mem_resolventSet_vadd, the resolvent of B +ᵥ A is bounded by r / (1 - ‖B‖ r).