The exponent-zero Hille--Yosida limit semigroup

Let A be a densely defined operator on a real Banach space. Suppose every positive real number belongs to its resolvent set and, for some M ≥ 1,

‖R(lambda, A) ^ n‖ ≤ M / lambda ^ n

for every n ≥ 1 and lambda > 0. The Yosida exponentials exp (t A_lambda) x are uniformly Cauchy on compact nonnegative time intervals. This file turns their pointwise limits into a strongly continuous semigroup and proves its exponent-zero growth bound ‖S(t)‖ ≤ M.

The underlying limit is TauCeti.Semigroups.yosidaLimit, shared with the Lumer--Phillips construction. The semigroup packaging is obtained from the shared constructor TauCeti.Semigroups.yosidaLimitSemigroupOfTendsto in LimitSemigroup.lean.

This is the limit stage of the Hille--Yosida generation theorem. The generator identification and the scalar unshift are carried out in TauCeti/Analysis/Semigroups/Generation/HilleYosida/Generation.lean.

Main results

• TauCeti.Semigroups.tendsto_yosidaLimit_of_norm_resolvent_pow_le: the Yosida exponentials converge pointwise to yosidaLimit.
• TauCeti.Semigroups.tendstoUniformlyOn_exp_yosidaApproximation_of_norm_resolvent_pow_le: uniform convergence on compact nonnegative intervals.
• TauCeti.Semigroups.norm_yosidaLimit_le_of_norm_resolvent_pow_le: each limit vector satisfies ‖yosidaLimit A t x‖ ≤ M * ‖x‖.
• TauCeti.Semigroups.hilleYosidaLimitSemigroup: the resulting strongly continuous semigroup.
• TauCeti.Semigroups.hilleYosidaLimitSemigroup_apply: evaluating the limit semigroup.
• TauCeti.Semigroups.hilleYosidaLimitSemigroup_realOperator_apply_of_nonneg: evaluating the real-time operator at nonnegative times.
• TauCeti.Semigroups.hasGrowthBound_hilleYosidaLimitSemigroup: its growth bound (0, M).
• TauCeti.Semigroups.tendsto_hilleYosidaLimitSemigroup: convergence of approximating orbits to the semigroup orbits.

References

• K.-J. Engel and R. Nagel, One-Parameter Semigroups for Linear Evolution Equations, Theorem II.3.8.
• A. Pazy, Semigroups of Linear Operators and Applications to Partial Differential Equations, Chapter 1, Theorem 5.3.

Convergence of the approximating exponentials

theorem TauCeti.Semigroups.tendsto_yosidaLimit_of_norm_resolvent_pow_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {M : ℝ} (hM : 1 ≤ M) (hres : ∀ (lambda : ℝ), 0 < lambda → lambda ∈ A.resolventSet) (hpow : ∀ (n : ℕ), 1 ≤ n → ∀ (lambda : ℝ), 0 < lambda → ‖A.resolvent lambda ^ n‖ ≤ M / lambda ^ n) (hdense : Dense ↑A.domain) {t : ℝ} (ht : 0 ≤ t) (x : X) : Filter.Tendsto (fun (lambda : ℝ) => (NormedSpace.exp (t • yosidaApproximation A lambda)) x) Filter.atTop (nhds (yosidaLimit A t x))

Under the exponent-zero Hille--Yosida bounds, the Yosida exponentials converge to the chosen Yosida limit at every nonnegative time.

theorem TauCeti.Semigroups.tendstoUniformlyOn_exp_yosidaApproximation_of_norm_resolvent_pow_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {M : ℝ} (hM : 1 ≤ M) (hres : ∀ (lambda : ℝ), 0 < lambda → lambda ∈ A.resolventSet) (hpow : ∀ (n : ℕ), 1 ≤ n → ∀ (lambda : ℝ), 0 < lambda → ‖A.resolvent lambda ^ n‖ ≤ M / lambda ^ n) (hdense : Dense ↑A.domain) (x : X) {T : ℝ} (hT : 0 ≤ T) : TendstoUniformlyOn (fun (lambda t : ℝ) => (NormedSpace.exp (t • yosidaApproximation A lambda)) x) (fun (t : ℝ) => yosidaLimit A t x) Filter.atTop (Set.Icc 0 T)

Convergence of the Hille--Yosida approximations is uniform on every compact nonnegative time interval.

theorem TauCeti.Semigroups.norm_yosidaLimit_le_of_norm_resolvent_pow_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {M : ℝ} (hM : 1 ≤ M) (hres : ∀ (lambda : ℝ), 0 < lambda → lambda ∈ A.resolventSet) (hpow : ∀ (n : ℕ), 1 ≤ n → ∀ (lambda : ℝ), 0 < lambda → ‖A.resolvent lambda ^ n‖ ≤ M / lambda ^ n) (hdense : Dense ↑A.domain) {t : ℝ} (ht : 0 ≤ t) (x : X) : ‖yosidaLimit A t x‖ ≤ M * ‖x‖

Under the exponent-zero Hille--Yosida bounds, each limit vector satisfies ‖yosidaLimit A t x‖ ≤ M * ‖x‖ at nonnegative times.

The limit semigroup

noncomputable def TauCeti.Semigroups.hilleYosidaLimitSemigroup {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {M : ℝ} (hM : 1 ≤ M) (hres : ∀ (lambda : ℝ), 0 < lambda → lambda ∈ A.resolventSet) (hpow : ∀ (n : ℕ), 1 ≤ n → ∀ (lambda : ℝ), 0 < lambda → ‖A.resolvent lambda ^ n‖ ≤ M / lambda ^ n) (hdense : Dense ↑A.domain) : StronglyContinuousSemigroup X

The strongly continuous semigroup obtained as the strong limit of the exponent-zero Hille--Yosida approximating semigroups.

Equations

• TauCeti.Semigroups.hilleYosidaLimitSemigroup hM hres hpow hdense = TauCeti.Semigroups.yosidaLimitSemigroupOfTendsto ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.Semigroups.hilleYosidaLimitSemigroup_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {M : ℝ} (hM : 1 ≤ M) (hres : ∀ (lambda : ℝ), 0 < lambda → lambda ∈ A.resolventSet) (hpow : ∀ (n : ℕ), 1 ≤ n → ∀ (lambda : ℝ), 0 < lambda → ‖A.resolvent lambda ^ n‖ ≤ M / lambda ^ n) (hdense : Dense ↑A.domain) (t : NNReal) (x : X) : ((hilleYosidaLimitSemigroup hM hres hpow hdense) t) x = yosidaLimit A (↑t) x

Evaluating the exponent-zero Hille--Yosida limit semigroup at t on x yields yosidaLimit A t x.

@[simp]

theorem TauCeti.Semigroups.hilleYosidaLimitSemigroup_realOperator_apply_of_nonneg {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {M : ℝ} (hM : 1 ≤ M) (hres : ∀ (lambda : ℝ), 0 < lambda → lambda ∈ A.resolventSet) (hpow : ∀ (n : ℕ), 1 ≤ n → ∀ (lambda : ℝ), 0 < lambda → ‖A.resolvent lambda ^ n‖ ≤ M / lambda ^ n) (hdense : Dense ↑A.domain) {t : ℝ} (ht : 0 ≤ t) (x : X) : ((hilleYosidaLimitSemigroup hM hres hpow hdense).realOperator t) x = yosidaLimit A t x

Evaluating the real-time operator of the exponent-zero Hille--Yosida limit semigroup at a nonnegative time t yields yosidaLimit A t x.

theorem TauCeti.Semigroups.hasGrowthBound_hilleYosidaLimitSemigroup {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {M : ℝ} (hM : 1 ≤ M) (hres : ∀ (lambda : ℝ), 0 < lambda → lambda ∈ A.resolventSet) (hpow : ∀ (n : ℕ), 1 ≤ n → ∀ (lambda : ℝ), 0 < lambda → ‖A.resolvent lambda ^ n‖ ≤ M / lambda ^ n) (hdense : Dense ↑A.domain) : (hilleYosidaLimitSemigroup hM hres hpow hdense).HasGrowthBound 0 M

The exponent-zero Hille--Yosida limit semigroup has growth bound (0, M).

theorem TauCeti.Semigroups.tendsto_hilleYosidaLimitSemigroup {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {M : ℝ} (hM : 1 ≤ M) (hres : ∀ (lambda : ℝ), 0 < lambda → lambda ∈ A.resolventSet) (hpow : ∀ (n : ℕ), 1 ≤ n → ∀ (lambda : ℝ), 0 < lambda → ‖A.resolvent lambda ^ n‖ ≤ M / lambda ^ n) (hdense : Dense ↑A.domain) (t : NNReal) (x : X) : Filter.Tendsto (fun (lambda : ℝ) => (NormedSpace.exp (↑t • yosidaApproximation A lambda)) x) Filter.atTop (nhds (((hilleYosidaLimitSemigroup hM hres hpow hdense) t) x))

The orbits of the exponent-zero Hille--Yosida limit semigroup are the limits of the Yosida exponentials.