Scalar shifts of unbounded operators

For an unbounded operator A, subtracting the scalar operator omega I leaves its domain unchanged and translates its resolvent:

R(lambda, A - omega I) = R(lambda + omega, A).

This file develops the characteristic resolvent API of the generic scalar shift from TauCeti.LinearAlgebra.LinearPMap.Shift. The results here are stated over an arbitrary nontrivially normed field, so a complex shift of a complex unbounded operator is covered. The continuous-inverse foundation itself applies to modules over a ring equipped with a topology. The construction is independent of semigroups; in particular, it can be used for an operator not yet known to generate one.

Main results

• TauCeti.LinearPMap.mem_resolventSet_subScalar_iff: translation of the resolvent set.
• TauCeti.LinearPMap.resolvent_subScalar: translation of the resolvent itself.

@[simp]

theorem TauCeti.LinearPMap.isResolventAt_subScalar_iff {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {A : X →ₗ.[𝕜] X} {omega lambda : 𝕜} {R : X →L[𝕜] X} : (subScalar A omega).IsResolventAt lambda R ↔ A.IsResolventAt (lambda + omega) R

An inverse for lambda I - (A - omega I) is the same as an inverse for (lambda + omega) I - A.

@[simp]

theorem TauCeti.LinearPMap.mem_resolventSet_subScalar_iff {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {A : X →ₗ.[𝕜] X} {omega lambda : 𝕜} : lambda ∈ (subScalar A omega).resolventSet ↔ lambda + omega ∈ A.resolventSet

Translation of the resolvent set under the scalar shift A ↦ A - omega I.

@[simp]

theorem TauCeti.LinearPMap.resolvent_subScalar {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] {A : X →ₗ.[𝕜] X} {omega lambda : 𝕜} (hlambda : lambda + omega ∈ A.resolventSet) : (subScalar A omega).resolvent lambda = A.resolvent (lambda + omega)

Exact translation of the resolvent under the scalar shift A ↦ A - omega I.