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

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

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

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

theorem ContinuousLinearMap.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 ∈ A.resolventSet) (hr : ‖A.resolvent lambda‖ ≤ r) (hB : ‖B‖ * r < 1) : ‖(↑B +ᵥ A).resolvent lambda‖ ≤ r / (1 - ‖B‖ * r)

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