The resolvent set of an unbounded operator

Mathlib's resolventSet and resolvent are Banach-algebra notions: they ask that algebraMap R A r - a be a unit of the algebra, which only makes sense for an element a of that algebra. The infinitesimal generator of a C₀-semigroup is not such an element — it is an unbounded operator, carried here by LinearPMap — so it needs its own resolvent notion.

The continuous-inverse foundation is defined in TauCeti.Topology.Algebra.Module.LinearPMap.Resolvent. This file develops its normed theory over an arbitrary nontrivially normed field. For A : X →ₗ.[𝕜] X and lambda : 𝕜 we say that a bounded operator R : X →L[𝕜] X is a resolvent of A at lambda (LinearPMap.IsResolventAt) when R takes values in D(A) and is a two-sided inverse of lambda • I - A : D(A) → X. Such an R is unique when it exists, so the resolvent set LinearPMap.resolventSet and the resolvent LinearPMap.resolvent are well defined, and the resolvent obeys the usual identities.

Nothing here mentions semigroups: the theory is stated for an arbitrary A : X →ₗ.[𝕜] X, which is what makes it usable for an operator not yet known to generate anything — the situation of the Hille--Yosida generation theorem, whose hypotheses read (ω, ∞) ⊆ resolventSet A together with a bound on ‖resolvent A l ^ n‖.

Two bridges keep this from being a parallel universe.

• To Mathlib's bounded notion. A bounded operator T : X →L[𝕜] X, read as the everywhere defined unbounded operator (T : X →ₗ[𝕜] X).toPMap ⊤, has exactly Mathlib's resolvent set and resolvent (ContinuousLinearMap.mem_resolventSet_toPMap_top_iff, ContinuousLinearMap.resolvent_toPMap_top), proved here.
• To the Laplace-transform resolvent. For a C₀-semigroup S with growth bound (ω, M), every lambda > ω lies in the resolvent set of the generator and the resolvent there is the Laplace transform ∫₀^∞ e^{-λt} S(t) x dt (StronglyContinuousSemigroup.generator_resolvent_eq). That bridge is proved downstream, in TauCeti/Analysis/Semigroups/Resolvent/Identity.lean, which then derives the semigroup resolvent identity from the abstract one below.

Definitions from the continuous-inverse foundation

• LinearPMap.IsResolventAt: R inverts lambda • I - A.
• LinearPMap.resolventSet: the set of lambda at which such an R exists.
• LinearPMap.resolvent: that R, chosen by Classical.choose.

Main results

• LinearPMap.IsResolventAt.unique: the inverse is unique, so the resolvent is well defined.
• LinearPMap.isResolventAt_iff_forall_mem_graph: the inverse condition read on the graph of A.
• TauCeti.LinearPMap.resolvent_sub_resolvent: the resolvent identity R(lambda) - R(mu) = (mu - lambda) R(lambda) R(mu), and TauCeti.LinearPMap.resolvent_comm.
• TauCeti.LinearPMap.mem_resolventSet_of_norm_mul_lt_one and LinearPMap.isOpen_resolventSet: the Neumann-series perturbation of a resolvent point, and the openness of the resolvent set it gives.
• TauCeti.LinearPMap.resolvent_eq_mul_inverse_one_sub: the local Neumann formula for the resolvent itself.
• LinearPMap.eq_of_le_of_mem_resolventSet: an operator has no proper extension sharing a resolvent point.
• ContinuousLinearMap.mem_resolventSet_toPMap_top_iff and ContinuousLinearMap.resolvent_toPMap_top: the bounded bridge.

References

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

The resolvent identity

theorem TauCeti.LinearPMap.resolvent_sub_resolvent_apply {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {A : X →ₗ.[𝕜] X} {lambda mu : 𝕜} (hl : lambda ∈ A.resolventSet) (hm : mu ∈ A.resolventSet) (y : X) : (A.resolvent lambda) y - (A.resolvent mu) y = (mu - lambda) • (A.resolvent lambda) ((A.resolvent mu) y)

Pointwise form of the resolvent identity R(lambda) - R(mu) = (mu - lambda) R(lambda) R(mu).

theorem TauCeti.LinearPMap.resolvent_sub_resolvent {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {A : X →ₗ.[𝕜] X} {lambda mu : 𝕜} (hl : lambda ∈ A.resolventSet) (hm : mu ∈ A.resolventSet) : A.resolvent lambda - A.resolvent mu = (mu - lambda) • A.resolvent lambda ∘SL A.resolvent mu

The resolvent identity R(lambda) - R(mu) = (mu - lambda) R(lambda) R(mu), as an equality of bounded operators.

theorem TauCeti.LinearPMap.resolvent_comm {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {A : X →ₗ.[𝕜] X} {lambda mu : 𝕜} (hl : lambda ∈ A.resolventSet) (hm : mu ∈ A.resolventSet) : A.resolvent lambda ∘SL A.resolvent mu = A.resolvent mu ∘SL A.resolvent lambda

Resolvents at two points of the resolvent set commute.

Neumann perturbations and openness of the resolvent set

theorem ContinuousLinearMap.isResolventAt_vadd_of_isUnit_one_sub_mul_resolvent {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {A : X →ₗ.[𝕜] X} {lambda : 𝕜} (B : X →L[𝕜] X) (h : lambda ∈ A.resolventSet) (hB : IsUnit (1 - B * A.resolvent lambda)) : (↑B +ᵥ A).IsResolventAt lambda (A.resolvent lambda * Ring.inverse (1 - B * A.resolvent lambda))

The common invertible perturbation witness. If lambda lies in the resolvent set of A and I - B R(lambda, A) is invertible, then R(lambda, A) (I - B R(lambda, A))⁻¹ inverts lambda • I - (B + A).

This is the lower-level construction shared by bounded perturbations and perturbations of the spectral parameter.

theorem ContinuousLinearMap.isResolventAt_vadd_of_norm_mul_resolvent_lt_one {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {A : X →ₗ.[𝕜] X} {lambda : 𝕜} [CompleteSpace X] (B : X →L[𝕜] X) (h : lambda ∈ A.resolventSet) (hB : ‖B * A.resolvent lambda‖ < 1) : (↑B +ᵥ A).IsResolventAt lambda (A.resolvent lambda * Ring.inverse (1 - B * A.resolvent lambda))

If lambda lies in the resolvent set of A and ‖B R(lambda, A)‖ < 1, then R(lambda, A) (I - B R(lambda, A))⁻¹ inverts lambda • I - (B + A).

theorem TauCeti.LinearPMap.mem_resolventSet_of_norm_mul_lt_one {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {A : X →ₗ.[𝕜] X} {lambda mu : 𝕜} [CompleteSpace X] (h : lambda ∈ A.resolventSet) (hmu : ‖mu - lambda‖ * ‖A.resolvent lambda‖ < 1) : mu ∈ A.resolventSet

The Neumann perturbation of a resolvent point. If lambda lies in the resolvent set and ‖mu - lambda‖ * ‖R(lambda)‖ < 1, then mu lies in it too.

theorem TauCeti.LinearPMap.resolvent_eq_mul_inverse_one_sub {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {A : X →ₗ.[𝕜] X} {lambda mu : 𝕜} [CompleteSpace X] (h : lambda ∈ A.resolventSet) (hmu : ‖mu - lambda‖ * ‖A.resolvent lambda‖ < 1) : A.resolvent mu = A.resolvent lambda * Ring.inverse (1 - (lambda - mu) • A.resolvent lambda)

Local Neumann formula for the resolvent. Inside the ball ‖mu - lambda‖ * ‖R(lambda)‖ < 1, the resolvent at mu is obtained by multiplying R(lambda) by the ring inverse of 1 - (lambda - mu) R(lambda).

theorem LinearPMap.isOpen_resolventSet {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] [CompleteSpace X] (A : X →ₗ.[𝕜] X) : IsOpen A.resolventSet

The resolvent set is open.

The bridge to Mathlib's Banach-algebra resolvent

A bounded operator T : X →L[𝕜] X becomes an everywhere defined unbounded operator (T : X →ₗ[𝕜] X).toPMap ⊤. Its resolvent set and resolvent in the sense above are Mathlib's resolventSet 𝕜 T and resolvent T, computed in the Banach algebra X →L[𝕜] X.

theorem LinearPMap.IsResolventAt.isUnit_toPMap_top {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {lambda : 𝕜} {R T : X →L[𝕜] X} (h : ((↑T).toPMap ⊤).IsResolventAt lambda R) : IsUnit ((algebraMap 𝕜 (X →L[𝕜] X)) lambda - T)

An inverse of lambda • I - T in the unbounded sense is a two-sided inverse in the algebra X →L[𝕜] X, so lambda • I - T is a unit there.

theorem IsUnit.isResolventAt_toPMap_top {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {lambda : 𝕜} {T : X →L[𝕜] X} (h : IsUnit ((algebraMap 𝕜 (X →L[𝕜] X)) lambda - T)) : ((↑T).toPMap ⊤).IsResolventAt lambda ↑h.unit⁻¹

A unit lambda • I - T of the algebra X →L[𝕜] X inverts lambda • I - T in the unbounded sense, with the algebra inverse as the resolvent.

@[simp]

theorem ContinuousLinearMap.mem_resolventSet_toPMap_top_iff {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] (T : X →L[𝕜] X) (lambda : 𝕜) : lambda ∈ ((↑T).toPMap ⊤).resolventSet ↔ lambda ∈ resolventSet 𝕜 T

The bounded bridge, membership half. For a bounded operator the unbounded resolvent set of T and Mathlib's Banach-algebra resolvent set agree.

@[simp]

theorem ContinuousLinearMap.resolvent_toPMap_top {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] (T : X →L[𝕜] X) {lambda : 𝕜} (h : lambda ∈ resolventSet 𝕜 T) : ((↑T).toPMap ⊤).resolvent lambda = resolvent T lambda

The bounded bridge, value half. For a bounded operator the unbounded resolvent is Mathlib's Banach-algebra resolvent.