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. 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, and the fact that an operator has no proper extension sharing a resolvent point. On normed spaces the continuous linear inverse is bounded; the normed resolvent theory and its bridge to Mathlib's Banach-algebra resolvent 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 Banach-algebra 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 bounded operator read as an everywhere defined LinearPMap; the bridge is developed in TauCeti.Analysis.Normed.Operator.Resolvent.Unbounded.

• 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.

Equations

• A.resolventSet = {lambda : 𝕜 | ∃ (R : X →L[𝕜] X), A.IsResolventAt lambda R}

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.

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.

Equations

• A.resolvent lambda = ⋯.choose

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_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).