Bounded approximations for the Hille--Yosida theorem

This file establishes the bounded stage of the exponent-zero, general-M Hille--Yosida construction. Suppose that the powers of an unbounded operator's resolvent at lambda > 0 satisfy

‖R(lambda, A) ^ n‖ ≤ M / lambda ^ n for every n ≥ 1, with 1 ≤ M.

Then every power of the scaled resolvent lambda R(lambda, A) has norm at most M. Expanding the resolvent factor in

exp (t A_lambda) = exp (-t lambda I) exp (t lambda² R(lambda, A))

as a power series gives the uniform estimate ‖exp (t A_lambda)‖ ≤ M for t ≥ 0. Consequently, the bounded-generator semigroup associated to every Yosida approximation has growth bound (0,M). Unlike the contraction estimate in TauCeti.Analysis.Semigroups.Generation.Yosida.Basic, this argument uses the bounds on all resolvent powers; that distinction is exactly why the exponent-zero Hille--Yosida hypothesis for general M is stronger than a bound on the resolvent alone.

For the general Hille--Yosida generation theorem, these estimates must be combined with reduction from (M, omega) to exponent zero by shifting the operator, compact-time Cauchy convergence of the approximating semigroups, construction of their strong limit, and identification of its generator.

Main results

• TauCeti.Semigroups.norm_smul_resolvent_pow_le: the scaled resolvent powers are bounded by M.
• TauCeti.Semigroups.norm_exp_smul_yosidaApproximation_le: every positive-time Yosida exponential has norm at most M.
• TauCeti.Semigroups.ofBounded_yosidaApproximation_hasGrowthBound: the corresponding bounded semigroup has growth bound (0,M).

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.Semigroups.norm_smul_resolvent_pow_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} {lambda M : ℝ} (hM : 1 ≤ M) (hlambda : 0 < lambda) (hpow : ∀ (n : ℕ), 1 ≤ n → ‖A.resolvent lambda ^ n‖ ≤ M / lambda ^ n) (n : ℕ) : ‖(lambda • A.resolvent lambda) ^ n‖ ≤ M

The exponent-zero Hille--Yosida bounds on the powers of R(lambda, A) imply the uniform bound ‖(lambda R(lambda, A)) ^ n‖ ≤ M, including at n = 0 when 1 ≤ M.

theorem TauCeti.Semigroups.norm_exp_smul_yosidaApproximation_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {lambda M t : ℝ} (hM : 1 ≤ M) (hlambda : 0 < lambda) (ht : 0 ≤ t) (hpow : ∀ (n : ℕ), 1 ≤ n → ‖A.resolvent lambda ^ n‖ ≤ M / lambda ^ n) : ‖NormedSpace.exp (t • yosidaApproximation A lambda)‖ ≤ M

Under the exponent-zero Hille--Yosida power bounds for general M, every positive-time Yosida approximation has norm at most M.

theorem TauCeti.Semigroups.ofBounded_yosidaApproximation_hasGrowthBound {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {lambda M : ℝ} (hM : 1 ≤ M) (hlambda : 0 < lambda) (hpow : ∀ (n : ℕ), 1 ≤ n → ‖A.resolvent lambda ^ n‖ ≤ M / lambda ^ n) : (StronglyContinuousSemigroup.ofBounded (yosidaApproximation A lambda)).HasGrowthBound 0 M

The bounded-generator semigroup associated to an exponent-zero Hille--Yosida approximation has the uniform growth bound (0, M).