Analyticity of an unbounded operator's resolvent

The resolvent of a LinearPMap on a complete normed space over a nontrivially normed field is analytic on its resolvent set. Locally at a resolvent point lambda, the Neumann formula identifies it with

R(mu) = R(lambda) * (1 - (lambda - mu) R(lambda))⁻¹.

The second factor is analytic near lambda because inversion in a complete normed algebra is analytic at every unit. This gives analyticity in operator norm, rather than merely pointwise analyticity after applying the resolvent to a vector.

Main results

• TauCeti.LinearPMap.analyticAt_resolvent: the resolvent is analytic at each point of its resolvent set.
• LinearPMap.analyticOnNhd_resolvent: the resolvent is analytic throughout its resolvent set.

References

• K.-J. Engel and R. Nagel, One-Parameter Semigroups for Linear Evolution Equations, Section IV.1.
• A. Pazy, Semigroups of Linear Operators and Applications to Partial Differential Equations, Chapter 1, Section 1.3.

theorem TauCeti.LinearPMap.analyticAt_resolvent {𝕜 : Type u_1} {X : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] [CompleteSpace X] {A : X →ₗ.[𝕜] X} {lambda : 𝕜} (h : lambda ∈ A.resolventSet) : AnalyticAt 𝕜 A.resolvent lambda

The resolvent of a LinearPMap is analytic at every point of its resolvent set.

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

The resolvent of a LinearPMap is analytic in operator norm on its resolvent set.