Power bounds for contraction-semigroup resolvents

This file proves the contraction case of the iterated Hille--Yosida estimate. If S is a contraction semigroup and lambda > 0, then every natural power of its Laplace-transform resolvent satisfies

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

The corresponding pointwise estimate and the equivalent bound for the scaled resolvent lambda R(lambda) are also recorded. These estimates are the contraction specialization of the power bounds used in the Hille--Yosida generation theorem.

References

The estimates are the contraction case of Engel--Nagel, One-Parameter Semigroups for Linear Evolution Equations, Theorem II.3.5.

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_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.