Integral formulas and power bounds for semigroup resolvents

This file proves the integral formula for powers of a Laplace-transform resolvent,

R(lambda)^(n+1) x = 1 / n! * integral t in (0, infinity), t^n exp (-lambda t) S(t)x dt,

and derives the sharp iterated Hille--Yosida estimate for a semigroup with growth bound (omega, M) (norm (S(t)) <= M exp (omega t) with M >= 1):

norm (R(lambda)^n) <= M / (lambda - omega)^n for n >= 1.

Only one factor of M occurs because R(lambda)^(n+1) is itself a single weighted orbit integral, so the growth bound is applied once. This is sharper than applying submultiplicativity to the first-resolvent bound, which would give M^n / (lambda - omega)^n.

For a contraction semigroup, this specializes to

‖R(lambda)^n‖ ≤ lambda⁻ⁿ.

Using generator_resolvent_eq, the sharp bound is also transported to the generator resolvent,

‖R(lambda, generator S)^n‖ ≤ M / (lambda - omega)^n,

with the corresponding contraction-semigroup specialization.

The corresponding pointwise estimates and the bound for the scaled contraction resolvent lambda R(lambda) are also recorded. This is the necessity half of the Hille--Yosida generation theorem: every C₀-semigroup's Laplace-transform resolvent, and hence its generator resolvent, satisfies the sharp power bound used by the generation theorem.

The sharp derivative bound obtained from the power formula is recorded here in both the general growth-bound and contraction cases.

References

Engel--Nagel, One-Parameter Semigroups for Linear Evolution Equations, Theorem II.1.10 and Corollary II.1.11 for the power formula and bound; Theorems II.3.5--II.3.8 for the generation theorems they support.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.resolvent_pow_succ_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {omega M : ℝ} (hb : S.HasGrowthBound omega M) (n : ℕ) {lambda : ℝ} (hlambda : omega < lambda) (x : X) : (S.resolvent hb lambda hlambda ^ (n + 1)) x = (1 / ↑n.factorial) • ∫ (t : ℝ) in Set.Ioi 0, (t ^ n * Real.exp (-(lambda * t))) • (S.realOperator t) x

The pointwise power formula for a semigroup resolvent: R(lambda)^(n+1)x = 1/n! integral t^n exp(-lambda t) S(t)x dt.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.norm_resolvent_pow_succ_apply_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {omega M : ℝ} (hb : S.HasGrowthBound omega M) (n : ℕ) {lambda : ℝ} (hlambda : omega < lambda) (x : X) : ‖(S.resolvent hb lambda hlambda ^ (n + 1)) x‖ ≤ M / (lambda - omega) ^ (n + 1) * ‖x‖

Pointwise form of the sharp Hille--Yosida power bound.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.resolvent_pow_norm_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {omega M : ℝ} (hb : S.HasGrowthBound omega M) (n : ℕ) {lambda : ℝ} (hlambda : omega < lambda) : ‖S.resolvent hb lambda hlambda ^ n‖ ≤ M / (lambda - omega) ^ n

The sharp iterated Hille--Yosida estimate for a semigroup with growth bound (omega, M): norm (R(lambda)^n) <= M / (lambda - omega)^n.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.norm_generator_resolvent_pow_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {omega M : ℝ} (hb : S.HasGrowthBound omega M) {lambda : ℝ} (hlambda : omega < lambda) (n : ℕ) : ‖LinearPMap.resolvent S.generator lambda ^ n‖ ≤ M / (lambda - omega) ^ n

Sharp Hille--Yosida power bound for the generator resolvent. For a C₀-semigroup with growth bound (omega, M) and lambda > omega, ‖R(lambda, generator S) ^ n‖ ≤ M / (lambda - omega) ^ n.

This is the necessity estimate in exactly the form consumed by the Hille--Yosida generation theorem.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.norm_iteratedDeriv_resolventFun_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {omega M : ℝ} (hb : S.HasGrowthBound omega M) (n : ℕ) {lambda : ℝ} (hlambda : omega < lambda) : ‖iteratedDeriv n (S.resolventFun hb) lambda‖ ≤ ↑n.factorial * M / (lambda - omega) ^ (n + 1)

The sharp Hille--Yosida derivative bound obtained from the resolvent power formula.

theorem TauCeti.Semigroups.ContractionSemigroup.resolvent_pow_succ_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : ContractionSemigroup X) (n : ℕ) {lambda : ℝ} (hlambda : 0 < lambda) (x : X) : (S.resolvent lambda hlambda ^ (n + 1)) x = (1 / ↑n.factorial) • ∫ (t : ℝ) in Set.Ioi 0, (t ^ n * Real.exp (-(lambda * t))) • (S.realOperator t) x

The pointwise power formula for a contraction-semigroup resolvent: R(lambda)^(n+1)x = 1/n! integral t^n exp(-lambda t) S(t)x dt.

theorem TauCeti.Semigroups.ContractionSemigroup.resolvent_pow_norm_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : ContractionSemigroup X) (lambda : ℝ) (hlambda : 0 < lambda) (n : ℕ) : ‖S.resolvent lambda hlambda ^ n‖ ≤ (1 / lambda) ^ n

The iterated Hille--Yosida bound for a contraction semigroup: ‖R(lambda)^n‖ ≤ lambda⁻ⁿ.

theorem TauCeti.Semigroups.ContractionSemigroup.norm_generator_resolvent_pow_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : ContractionSemigroup X) {lambda : ℝ} (hlambda : 0 < lambda) (n : ℕ) : ‖LinearPMap.resolvent S.generator lambda ^ n‖ ≤ (1 / lambda) ^ n

The sharp Hille--Yosida power bound for the generator of a contraction semigroup: ‖R(lambda, generator S) ^ n‖ ≤ lambda⁻ⁿ for lambda > 0.

theorem TauCeti.Semigroups.ContractionSemigroup.norm_iteratedDeriv_resolventFun_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : ContractionSemigroup X) (n : ℕ) {lambda : ℝ} (hlambda : 0 < lambda) : ‖iteratedDeriv n S.resolventFun lambda‖ ≤ ↑n.factorial * (1 / lambda) ^ (n + 1)

The Hille--Yosida derivative bound in the contraction case.

theorem TauCeti.Semigroups.ContractionSemigroup.norm_resolvent_pow_apply_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : ContractionSemigroup X) (lambda : ℝ) (hlambda : 0 < lambda) (n : ℕ) (x : X) : ‖(S.resolvent lambda hlambda ^ n) x‖ ≤ (1 / lambda) ^ n * ‖x‖

Pointwise form of the iterated contraction resolvent bound.

theorem TauCeti.Semigroups.ContractionSemigroup.norm_smul_resolvent_pow_le_one {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : ContractionSemigroup X) (lambda : ℝ) (hlambda : 0 < lambda) (n : ℕ) : ‖(lambda • S.resolvent lambda hlambda) ^ n‖ ≤ 1

Every power of the scaled contraction resolvent lambda R(lambda) has norm at most one.

theorem TauCeti.Semigroups.ContractionSemigroup.norm_smul_resolvent_pow_apply_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : ContractionSemigroup X) (lambda : ℝ) (hlambda : 0 < lambda) (n : ℕ) (x : X) : ‖((lambda • S.resolvent lambda hlambda) ^ n) x‖ ≤ ‖x‖

Pointwise form of the power bound for the scaled contraction resolvent.