Resolvent of a bounded generator

This file identifies the Laplace-transform resolvent of the uniformly continuous semigroup t ↦ exp (tA) with the Neumann series for λI - A. For ‖A‖ < λ, the series

λ⁻¹ ∑' n, (λ⁻¹ A)ⁿ

converges in the Banach algebra of bounded operators and is a two-sided inverse of λI - A. The general semigroup resolvent is already a right inverse, so the two operators agree. This is the bounded-generator resolvent acceptance example in the one-parameter-semigroups roadmap.

The geometric-series argument uses Mathlib's summable_geometric_of_norm_lt_one and its two multiplication identities for the sum.

References

See Engel--Nagel, One-Parameter Semigroups for Linear Evolution Equations, Section I.3.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofBounded_resolvent_eq_inv_smul_tsum_pow {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →L[ℝ] X) {lambda : ℝ} (hlambda : ‖A‖ < lambda) : (ofBounded A).resolvent ⋯ lambda hlambda = lambda⁻¹ • ∑' (n : ℕ), (lambda⁻¹ • A) ^ n

For λ > ‖A‖, the Laplace-transform resolvent of t ↦ exp (tA) is the Neumann series λ⁻¹ ∑' n, (λ⁻¹ A)ⁿ.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofBounded_resolvent_eq_resolvent {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →L[ℝ] X) {lambda : ℝ} (hlambda : ‖A‖ < lambda) : (ofBounded A).resolvent ⋯ lambda hlambda = _root_.resolvent A lambda

For λ > ‖A‖, the Laplace-transform resolvent of t ↦ exp (tA) agrees with Mathlib's Banach-algebra resolvent of A.