Growth bounds for strongly continuous semigroups

This file contains exponential growth bounds for C₀-semigroups, including the contraction case and the existence of a finite exponential type.

The uniform operator bound this provides also yields strong continuity of (u, x) ↦ S u x in both arguments at once (StronglyContinuousSemigroup.tendsto_realOperator_apply and its ContinuousOn form StronglyContinuousSemigroup.continuousOn_realOperator_apply), which does not follow from continuity of u ↦ S u alone.

References

Ported and adapted (Apache 2.0) from mrdouglasny/hille-yosida; references include Engel--Nagel, Linares, Pazy, Hille, and Yosida.

Exponential growth bounds

def TauCeti.Semigroups.StronglyContinuousSemigroup.HasGrowthBound {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (ω M : ℝ) : Prop

A C₀-semigroup has exponential growth bound (ω, M), with M ≥ 1.

Equations

• S.HasGrowthBound ω M = (1 ≤ M ∧ ∀ (t : ℝ), 0 ≤ t → ‖S.realOperator t‖ ≤ M * Real.exp (ω * t))

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.HasGrowthBound.one_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {S : StronglyContinuousSemigroup X} {ω M : ℝ} (hb : S.HasGrowthBound ω M) : 1 ≤ M

The multiplicative constant in a growth bound is at least one.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.HasGrowthBound.bound {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {S : StronglyContinuousSemigroup X} {ω M : ℝ} (hb : S.HasGrowthBound ω M) (t : ℝ) (ht : 0 ≤ t) : ‖S.realOperator t‖ ≤ M * Real.exp (ω * t)

The operator-norm estimate supplied by a growth bound.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.hasGrowthBound_of_bound {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {S : StronglyContinuousSemigroup X} {ω M : ℝ} (hM : 1 ≤ M) (hbound : ∀ (t : ℝ), 0 ≤ t → ‖S.realOperator t‖ ≤ M * Real.exp (ω * t)) : S.HasGrowthBound ω M

Constructor for a growth bound from the multiplicative lower bound and operator-norm estimate.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.HasGrowthBound.mono {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {S : StronglyContinuousSemigroup X} {ω M ω' M' : ℝ} (hb : S.HasGrowthBound ω M) (hω : ω ≤ ω') (hM : M ≤ M') : S.HasGrowthBound ω' M'

A growth bound can be weakened by increasing both the exponential rate and the multiplicative constant.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.HasGrowthBound.mono_omega {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {S : StronglyContinuousSemigroup X} {ω M ω' : ℝ} (hb : S.HasGrowthBound ω M) (hω : ω ≤ ω') : S.HasGrowthBound ω' M

A growth bound can be weakened by increasing the exponential rate.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.HasGrowthBound.norm_le_mul_exp_max_zero_mul_of_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {S : StronglyContinuousSemigroup X} {ω M : ℝ} (hb : S.HasGrowthBound ω M) {t t₀ : ℝ} (ht : 0 ≤ t) (htt₀ : t ≤ t₀) : ‖S.realOperator t‖ ≤ M * Real.exp (max ω 0 * t₀)

A growth bound controls the semigroup on [0, t₀] by the envelope M * exp (max ω 0 * t₀). Replacing the signed rate ω by max ω 0 makes the envelope nondecreasing in the time, so the bound at t₀ covers every earlier nonnegative t.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.HasGrowthBound.mono_const {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {S : StronglyContinuousSemigroup X} {ω M M' : ℝ} (hb : S.HasGrowthBound ω M) (hM : M ≤ M') : S.HasGrowthBound ω M'

A growth bound can be weakened by increasing the multiplicative constant.

theorem TauCeti.Semigroups.ContractionSemigroup.hasGrowthBound {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : ContractionSemigroup X) : S.HasGrowthBound 0 1

A contraction semigroup has growth bound (0, 1).

theorem TauCeti.Semigroups.ContractionSemigroup.hasGrowthBound_of_nonneg_omega {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : ContractionSemigroup X) {ω : ℝ} (hω : 0 ≤ ω) : S.HasGrowthBound ω 1

A contraction semigroup has every nonnegative exponential growth rate with constant 1.

theorem TauCeti.Semigroups.ContractionSemigroup.hasGrowthBound_of_one_le_const {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : ContractionSemigroup X) {M : ℝ} (hM : 1 ≤ M) : S.HasGrowthBound 0 M

A contraction semigroup has growth bound (0, M) for every M ≥ 1.

theorem TauCeti.Semigroups.ContractionSemigroup.hasGrowthBound_of_nonneg_omega_of_one_le_const {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : ContractionSemigroup X) {ω M : ℝ} (hω : 0 ≤ ω) (hM : 1 ≤ M) : S.HasGrowthBound ω M

A contraction semigroup has growth bound (ω, M) whenever 0 ≤ ω and 1 ≤ M.

Growth Bounds and Exponential Type

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.existsGrowthBound {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) : ∃ (ω : ℝ) (M : ℝ), S.HasGrowthBound ω M

Every C₀-semigroup has a finite exponential growth bound ([EN] Prop. I.5.5, [Linares] Thm. 1).

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.existsGrowthBound_ge_omega {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) (ω₀ : ℝ) : ∃ (ω : ℝ) (M : ℝ), ω₀ ≤ ω ∧ S.HasGrowthBound ω M

A C₀-semigroup admits a growth bound with exponent at least any prescribed real number.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.existsGrowthBound_ge_const {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) (M₀ : ℝ) : ∃ (ω : ℝ) (M : ℝ), M₀ ≤ M ∧ S.HasGrowthBound ω M

A C₀-semigroup admits a growth bound with multiplicative constant at least any prescribed real number.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.existsGrowthBound_ge {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) (ω₀ M₀ : ℝ) : ∃ (ω : ℝ) (M : ℝ), ω₀ ≤ ω ∧ M₀ ≤ M ∧ S.HasGrowthBound ω M

A C₀-semigroup admits a growth bound whose exponent and multiplicative constant are both at least prescribed lower bounds.

Joint strong continuity

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.tendsto_realOperator_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {ι : Type u_2} {l : Filter ι} (S : StronglyContinuousSemigroup X) {f : ι → ℝ} {g : ι → X} {r : ℝ} {z : X} (hf : Filter.Tendsto f l (nhds r)) (hf0 : ∀ᶠ (i : ι) in l, 0 ≤ f i) (hr : 0 ≤ r) (hg : Filter.Tendsto g l (nhds z)) : Filter.Tendsto (fun (i : ι) => (S.realOperator (f i)) (g i)) l (nhds ((S.realOperator r) z))

Joint strong continuity: if f i → r through nonnegative values and g i → z, then S (f i) (g i) → S r z.

A C₀-semigroup is strongly, not uniformly, continuous, so this does not follow from continuity of u ↦ S.realOperator u alone; the proof combines strong continuity at r with the uniform operator bound supplied by a growth bound.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.continuousOn_realOperator_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {Y : Type u_2} [TopologicalSpace Y] {s : Set Y} {f : Y → ℝ} {g : Y → X} (hf : ContinuousOn f s) (hf0 : ∀ u ∈ s, 0 ≤ f u) (hg : ContinuousOn g s) : ContinuousOn (fun (u : Y) => (S.realOperator (f u)) (g u)) s

The ContinuousOn form of joint strong continuity: a continuous nonnegative time reparametrization applied to a continuous vector-valued map gives a continuous orbit.