The shift reduction for the Hille--Yosida theorem

The Hille--Yosida generation theorem is proved first at growth exponent zero. For an operator A with resolvent bounds on (omega, infinity), the shifted operator A - omega I has the corresponding bounds on (0, infinity). This file packages that reduction using the exact resolvent translation

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

Together with StronglyContinuousSemigroup.generator_expShift, this is the shift step that reduces the general (M, omega) generation problem to the exponent-zero construction.

Main result

• TauCeti.LinearPMap.hilleYosida_zero_of: reduction of the general Hille--Yosida resolvent hypotheses to growth exponent zero.

References

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

theorem TauCeti.LinearPMap.hilleYosida_zero_of {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} {M omega : ℝ} (hres : ∀ (lambda : ℝ), omega < lambda → lambda ∈ A.resolventSet) (hbound : ∀ (n : ℕ), 1 ≤ n → ∀ (lambda : ℝ), omega < lambda → ‖A.resolvent lambda ^ n‖ ≤ M / (lambda - omega) ^ n) : (∀ (lambda : ℝ), 0 < lambda → lambda ∈ (subScalar A omega).resolventSet) ∧ ∀ (n : ℕ), 1 ≤ n → ∀ (lambda : ℝ), 0 < lambda → ‖(subScalar A omega).resolvent lambda ^ n‖ ≤ M / lambda ^ n

The general (M, omega) Hille--Yosida resolvent hypotheses become the exponent-zero hypotheses for A - omega I.

This packages exactly the two facts consumed by the zero-exponent Yosida construction: every positive lambda is a resolvent point, and every positive power satisfies the sharp M / lambda ^ n estimate.