Continuous inverses of shifts of partial linear maps

For a partial linear map A on a module over a ring, LinearPMap.IsResolventAt says that a continuous linear map inverts lambda • I - A on the domain of A. The inverse is unique, and its existence defines LinearPMap.resolventSet and the chosen map LinearPMap.resolvent. Its complement is LinearPMap.spectrum. These notions require only a topology on the module, with no norm or continuity assumptions on addition or scalar multiplication.

Over a noncommutative ring, the scalar expression x ↦ lambda • x - A x need not be linear. The predicate still requires its inverse to be linear over the full scalar ring; a parameter whose shift is not linear therefore does not belong to the resolvent set.

This file gives the graph characterization, the two inverse identities, the fact that a point of the resolvent set is not an eigenvalue, and the fact that an operator has no proper extension sharing a resolvent point. The pointwise resolvent identity holds over rings. Over division rings resolvents commute, and the resolvent at lambda acts on an eigenvector for the eigenvalue c as multiplication by (lambda - c)⁻¹. For topological additive groups, an invertible continuous linear perturbation gives another resolvent. Over commutative rings with continuous scalar multiplication by constants, the resolvent of an everywhere defined continuous linear operator agrees with Mathlib's algebraic resolvent, and their spectra agree.

On normed spaces over nontrivially normed fields the continuous linear inverse is bounded; Neumann perturbations and openness of the resolvent set are developed in TauCeti.Analysis.Normed.Operator.Resolvent.Unbounded.

References

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

Inverting lambda • I - A

structure LinearPMap.IsResolventAt {𝕜 : Type u_1} {X : Type u_2} [Ring 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] (A : X →ₗ.[𝕜] X) (lambda : 𝕜) (R : X →L[𝕜] X) : Prop

IsResolventAt A lambda R says that the continuous operator R : X →L[𝕜] X inverts lambda • I - A : D(A) → X: it takes its values in D(A), is a right inverse of lambda • I - A on all of X, and is a left inverse of it on D(A).

For an unbounded A this replaces the algebraic condition IsUnit (algebraMap 𝕜 (X →L[𝕜] X) lambda - A) behind Mathlib's resolventSet, which cannot be formed because A is not an element of X →L[𝕜] X. The two conditions agree when A is a continuous linear operator read as an everywhere defined LinearPMap; see ContinuousLinearMap.mem_resolventSet_toPMap_top_iff.

• mem_domain (y : X) : R y ∈ A.domain

  The inverse takes its values in the domain of A.

• smul_sub_apply (y : X) : lambda • R y - ↑A ⟨R y, ⋯⟩ = y

  R is a right inverse: (lambda • I - A) (R y) = y for every y : X.

• apply_smul_sub (x : ↥A.domain) : R (lambda • ↑x - ↑A x) = ↑x

  R is a left inverse: R ((lambda • I - A) x) = x for every x ∈ D(A).

theorem LinearPMap.IsResolventAt.unique {𝕜 : Type u_1} {X : Type u_2} [Ring 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] {A : X →ₗ.[𝕜] X} {lambda : 𝕜} {R : X →L[𝕜] X} (h : A.IsResolventAt lambda R) {R' : X →L[𝕜] X} (h' : A.IsResolventAt lambda R') : R = R'

An inverse of lambda • I - A is unique: a left inverse and a right inverse of the same map agree.

theorem LinearPMap.IsResolventAt.smul_sub_injective {𝕜 : Type u_1} {X : Type u_2} [Ring 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] {A : X →ₗ.[𝕜] X} {lambda : 𝕜} {R : X →L[𝕜] X} (h : A.IsResolventAt lambda R) : Function.Injective fun (x : ↥A.domain) => lambda • ↑x - ↑A x

lambda • I - A is injective on D(A) whenever it has a left inverse.

theorem LinearPMap.IsResolventAt.smul_sub_surjective {𝕜 : Type u_1} {X : Type u_2} [Ring 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] {A : X →ₗ.[𝕜] X} {lambda : 𝕜} {R : X →L[𝕜] X} (h : A.IsResolventAt lambda R) : Function.Surjective fun (x : ↥A.domain) => lambda • ↑x - ↑A x

lambda • I - A maps D(A) onto X whenever it has a right inverse.

theorem LinearPMap.IsResolventAt.smul_sub_bijective {𝕜 : Type u_1} {X : Type u_2} [Ring 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] {A : X →ₗ.[𝕜] X} {lambda : 𝕜} {R : X →L[𝕜] X} (h : A.IsResolventAt lambda R) : Function.Bijective fun (x : ↥A.domain) => lambda • ↑x - ↑A x

lambda • I - A : D(A) → X is a bijection at a point of the resolvent set.

theorem LinearPMap.isResolventAt_iff_forall_mem_graph {𝕜 : Type u_1} {X : Type u_2} [Ring 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] {A : X →ₗ.[𝕜] X} {lambda : 𝕜} {R : X →L[𝕜] X} : A.IsResolventAt lambda R ↔ (∀ (y : X), (R y, lambda • R y - y) ∈ A.graph) ∧ ∀ p ∈ A.graph, R (lambda • p.1 - p.2) = p.1

The graph form of IsResolventAt: R inverts lambda • I - A exactly when every (R y, lambda • R y - y) lies on the graph of A, and R (lambda • x - w) = x for every point (x, w) of that graph. This form transfers along any construction described by its graph.

The resolvent set and the resolvent

def LinearPMap.resolventSet {𝕜 : Type u_1} {X : Type u_2} [Ring 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] (A : X →ₗ.[𝕜] X) : Set 𝕜

The resolvent set of an unbounded operator A : X →ₗ.[𝕜] X: those lambda : 𝕜 for which lambda • I - A : D(A) → X is a bijection with continuous linear inverse.

theorem LinearPMap.mem_resolventSet_iff {𝕜 : Type u_1} {X : Type u_2} [Ring 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] {A : X →ₗ.[𝕜] X} {lambda : 𝕜} : lambda ∈ A.resolventSet ↔ ∃ (R : X →L[𝕜] X), A.IsResolventAt lambda R

Membership in the resolvent set unfolds to the existence of a continuous linear inverse of lambda • I - A.

def LinearPMap.spectrum {𝕜 : Type u_1} {X : Type u_2} [Ring 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] (A : X →ₗ.[𝕜] X) : Set 𝕜

The spectrum of a partial linear map consists of the scalars whose shifts do not admit continuous linear two-sided inverses.

@[simp]

theorem LinearPMap.mem_spectrum_iff {𝕜 : Type u_1} {X : Type u_2} [Ring 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] (A : X →ₗ.[𝕜] X) (z : 𝕜) : z ∈ A.spectrum ↔ z ∉ A.resolventSet

Membership in the partial-operator spectrum is failure of resolvent membership.

theorem LinearPMap.IsResolventAt.mem_resolventSet {𝕜 : Type u_1} {X : Type u_2} [Ring 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] {A : X →ₗ.[𝕜] X} {lambda : 𝕜} {R : X →L[𝕜] X} (h : A.IsResolventAt lambda R) : lambda ∈ A.resolventSet

Exhibiting an inverse puts lambda in the resolvent set.

noncomputable def LinearPMap.resolvent {𝕜 : Type u_1} {X : Type u_2} [Ring 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] (A : X →ₗ.[𝕜] X) (lambda : 𝕜) : X →L[𝕜] X

The resolvent R(lambda, A) = (lambda • I - A)⁻¹ of an unbounded operator, as a continuous linear operator on X.

Off the resolvent set the value is an unspecified junk value; every lemma below carries the hypothesis lambda ∈ resolventSet A. Uniqueness of the inverse (LinearPMap.IsResolventAt.unique) makes the choice immaterial on the resolvent set: LinearPMap.resolvent_eq_of_isResolventAt identifies it with any inverse one can exhibit.

theorem LinearPMap.isResolventAt_resolvent {𝕜 : Type u_1} {X : Type u_2} [Ring 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] {A : X →ₗ.[𝕜] X} {lambda : 𝕜} (h : lambda ∈ A.resolventSet) : A.IsResolventAt lambda (A.resolvent lambda)

On the resolvent set, resolvent A lambda really does invert lambda • I - A.

theorem LinearPMap.resolvent_eq_of_isResolventAt {𝕜 : Type u_1} {X : Type u_2} [Ring 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] {A : X →ₗ.[𝕜] X} {lambda : 𝕜} {R : X →L[𝕜] X} (h : A.IsResolventAt lambda R) : A.resolvent lambda = R

Any exhibited inverse of lambda • I - A is the resolvent.

theorem LinearPMap.resolvent_mem_domain {𝕜 : Type u_1} {X : Type u_2} [Ring 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] {A : X →ₗ.[𝕜] X} {lambda : 𝕜} (h : lambda ∈ A.resolventSet) (y : X) : (A.resolvent lambda) y ∈ A.domain

The resolvent takes its values in D(A).

theorem LinearPMap.smul_sub_apply_resolvent {𝕜 : Type u_1} {X : Type u_2} [Ring 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] {A : X →ₗ.[𝕜] X} {lambda : 𝕜} (h : lambda ∈ A.resolventSet) (y : X) : lambda • (A.resolvent lambda) y - ↑A ⟨(A.resolvent lambda) y, ⋯⟩ = y

The right-inverse identity (lambda • I - A) R(lambda) y = y.

@[simp]

theorem LinearPMap.resolvent_smul_sub_apply {𝕜 : Type u_1} {X : Type u_2} [Ring 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] {A : X →ₗ.[𝕜] X} {lambda : 𝕜} (h : lambda ∈ A.resolventSet) (x : ↥A.domain) : (A.resolvent lambda) (lambda • ↑x - ↑A x) = ↑x

The left-inverse identity R(lambda) (lambda • x - A x) = x on D(A).

@[simp]

theorem LinearPMap.apply_resolvent {𝕜 : Type u_1} {X : Type u_2} [Ring 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] {A : X →ₗ.[𝕜] X} {lambda : 𝕜} (h : lambda ∈ A.resolventSet) (y : X) : ↑A ⟨(A.resolvent lambda) y, ⋯⟩ = lambda • (A.resolvent lambda) y - y

The right-inverse identity solved for A: A R(lambda) y = lambda • R(lambda) y - y.

theorem LinearPMap.smul_sub_bijective {𝕜 : Type u_1} {X : Type u_2} [Ring 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] {A : X →ₗ.[𝕜] X} {lambda : 𝕜} (h : lambda ∈ A.resolventSet) : Function.Bijective fun (x : ↥A.domain) => lambda • ↑x - ↑A x

At a point of the resolvent set, lambda • I - A : D(A) → X is a bijection.

theorem LinearPMap.eq_zero_of_apply_eq_smul {𝕜 : Type u_1} {X : Type u_2} [Ring 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] {A : X →ₗ.[𝕜] X} {lambda : 𝕜} (h : lambda ∈ A.resolventSet) (x : ↥A.domain) (hx : ↑A x = lambda • ↑x) : x = 0

A point of the resolvent set is not an eigenvalue: A x = lambda • x forces x = 0.

theorem LinearPMap.eq_of_le_of_mem_resolventSet {𝕜 : Type u_1} {X : Type u_2} [Ring 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] {lambda : 𝕜} {A B : X →ₗ.[𝕜] X} (hAB : A ≤ B) (hA : lambda ∈ A.resolventSet) (hB : lambda ∈ B.resolventSet) : A = B

An operator has no proper extension sharing a resolvent point. If A ≤ B and some lambda lies in the resolvent set of both, then A = B.

A vector y ∈ D(B) has lambda • y - B y = lambda • x - A x for a unique x ∈ D(A), by surjectivity for A; injectivity for B then forces y = x, so D(B) ⊆ D(A).

This is the step that upgrades "A is a restriction of the generator" to "A is the generator" in the generation theorems.

theorem LinearPMap.resolvent_apply_comm {𝕜 : Type u_1} {X : Type u_2} [Ring 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] {A : X →ₗ.[𝕜] X} {lambda : 𝕜} (h : lambda ∈ A.resolventSet) (x : ↥A.domain) : (A.resolvent lambda) (↑A x) = ↑A ⟨(A.resolvent lambda) ↑x, ⋯⟩

The resolvent commutes with A on D(A): R(lambda) (A x) = A (R(lambda) x).

The resolvent identity

theorem LinearPMap.resolvent_sub_resolvent_apply {𝕜 : Type u_1} {X : Type u_2} [Ring 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 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 LinearPMap.resolvent_sub_resolvent {𝕜 : Type u_1} {X : Type u_2} [CommRing 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] [IsTopologicalAddGroup X] [ContinuousConstSMul 𝕜 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 continuous linear maps.

theorem LinearPMap.resolvent_comm {𝕜 : Type u_1} {X : Type u_2} [DivisionRing 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 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.

theorem LinearPMap.resolvent_apply_of_apply_eq_smul {𝕜 : Type u_1} {X : Type u_2} [DivisionRing 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] {A : X →ₗ.[𝕜] X} {lambda : 𝕜} (h : lambda ∈ A.resolventSet) {c : 𝕜} (x : ↥A.domain) (hx : ↑A x = c • ↑x) : (A.resolvent lambda) ↑x = (lambda - c)⁻¹ • ↑x

The resolvent acts on an eigenvector of A for the eigenvalue c as multiplication by (lambda - c)⁻¹. For c = lambda both sides vanish: a point of the resolvent set is not an eigenvalue, so the eigenvector is zero.

Invertible perturbations

theorem ContinuousLinearMap.isResolventAt_vadd_of_isUnit_one_sub_mul_resolvent {𝕜 : Type u_1} {X : Type u_2} [Ring 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] [IsTopologicalAddGroup 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.

The bridge to Mathlib's algebraic resolvent

A continuous linear operator T : X →L[𝕜] X becomes an everywhere defined partial linear map (T : X →ₗ[𝕜] X).toPMap ⊤. Its resolvent set and resolvent agree with Mathlib's resolventSet 𝕜 T and resolvent T, computed in the algebra X →L[𝕜] X.

theorem LinearPMap.IsResolventAt.isUnit_toPMap_top {𝕜 : Type u_1} {X : Type u_2} [CommRing 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] [IsTopologicalAddGroup X] [ContinuousConstSMul 𝕜 X] {T R : X →L[𝕜] X} {lambda : 𝕜} (h : ((↑T).toPMap ⊤).IsResolventAt lambda R) : IsUnit ((algebraMap 𝕜 (X →L[𝕜] X)) lambda - T)

An inverse of lambda • I - T in the partial-map 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} [CommRing 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] [IsTopologicalAddGroup X] [ContinuousConstSMul 𝕜 X] {T : X →L[𝕜] X} {lambda : 𝕜} (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 partial-map sense, with the algebra inverse as the resolvent.

@[simp]

theorem ContinuousLinearMap.mem_resolventSet_toPMap_top_iff {𝕜 : Type u_1} {X : Type u_2} [CommRing 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] [IsTopologicalAddGroup X] [ContinuousConstSMul 𝕜 X] (T : X →L[𝕜] X) (lambda : 𝕜) : lambda ∈ ((↑T).toPMap ⊤).resolventSet ↔ lambda ∈ resolventSet 𝕜 T

The continuous-operator bridge, membership half. For a continuous linear operator T, the partial-map resolvent set and Mathlib's algebraic resolvent set agree.

@[simp]

theorem ContinuousLinearMap.spectrum_toPMap_top {𝕜 : Type u_1} {X : Type u_2} [CommRing 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] [IsTopologicalAddGroup X] [ContinuousConstSMul 𝕜 X] (T : X →L[𝕜] X) : ((↑T).toPMap ⊤).spectrum = spectrum 𝕜 T

For a continuous linear operator on the full domain, the partial-operator spectrum agrees with Mathlib's algebraic spectrum in X →L[𝕜] X.

@[simp]

theorem ContinuousLinearMap.resolvent_toPMap_top {𝕜 : Type u_1} {X : Type u_2} [CommRing 𝕜] [AddCommGroup X] [TopologicalSpace X] [Module 𝕜 X] [IsTopologicalAddGroup X] [ContinuousConstSMul 𝕜 X] (T : X →L[𝕜] X) {lambda : 𝕜} (h : lambda ∈ resolventSet 𝕜 T) : ((↑T).toPMap ⊤).resolvent lambda = resolvent T lambda

The continuous-operator bridge, value half. For a continuous linear operator, the partial-map resolvent is Mathlib's algebraic resolvent.