Limits of Yosida semigroups

For an unbounded operator A on a real Banach space whose Yosida approximations A_lambda = lambda ^ 2 R(lambda, A) - lambda I generate approximating exponentials exp (t A_lambda) x that form a Cauchy family as lambda -> +∞, this file defines the chosen candidate limit vector yosidaLimit A t x and provides the shared scaffolding for assembling such limits into strongly continuous semigroups.

Completeness of the Banach space turns the Cauchy estimate into a limit vector yosidaLimit A t x. The definition is the chosen value limUnder atTop of exp (t A_lambda) x, so it makes sense for every real t, but it is only proved to be the limit when A is m-dissipative with dense domain (or satisfies the Hille--Yosida bounds) and t ≥ 0. For the densely defined m-dissipative case, convergence is established below in TauCeti.Semigroups.IsMDissipative.tendsto_yosidaLimit; for the general-M Hille--Yosida case, convergence is proved in TauCeti.Semigroups.tendsto_yosidaLimit_of_norm_resolvent_pow_le in TauCeti/Analysis/Semigroups/Generation/HilleYosida/Limit.lean.

On the range t ≥ 0, the limit is linear in x, satisfies S(0) = I and S(s + t) = S(s) S(t), and — because the convergence is uniform on compact time intervals — depends continuously on t. Under m-dissipativity it is contractive and yields a genuine contraction semigroup yosidaLimitSemigroup, while under general Hille--Yosida bounds with parameter M ≥ 1 it satisfies ‖yosidaLimit A t x‖ ≤ M * ‖x‖.

This file also provides the general limit-semigroup constructor yosidaLimitSemigroupOfTendsto parameterized by pointwise and uniform convergence and an eventual norm bound, shared between the Lumer--Phillips and Hille--Yosida constructions.

Main definitions

• TauCeti.Semigroups.yosidaLimit: the value chosen from the family exp (t A_lambda) x as lambda -> ∞, which is its limit at nonnegative times.
• TauCeti.Semigroups.yosidaLimitSemigroupOfTendsto: the strongly continuous semigroup obtained from pointwise and uniform convergence and an eventual norm bound M.
• TauCeti.Semigroups.IsMDissipative.yosidaLimitSemigroup: the resulting contraction semigroup.

Main results

• TauCeti.Semigroups.norm_yosidaLimit_le_of_tendsto_of_norm_le: passing an operator bound to the limit.
• TauCeti.Semigroups.yosidaLimitSemigroupOfTendsto_apply: evaluating the limit semigroup.
• TauCeti.Semigroups.yosidaLimitSemigroupOfTendsto_realOperator_apply_of_nonneg: evaluating the real-time operator at nonnegative times.
• TauCeti.Semigroups.hasGrowthBound_yosidaLimitSemigroupOfTendsto: growth bound (0, M) of the limit semigroup.
• TauCeti.Semigroups.tendsto_yosidaLimitSemigroupOfTendsto: convergence of approximating orbits.
• TauCeti.Semigroups.IsMDissipative.tendsto_yosidaLimit: the defining convergence exp (t A_lambda) x -> yosidaLimit A t x.
• TauCeti.Semigroups.IsMDissipative.tendstoUniformlyOn_exp_yosidaApproximation: that convergence is uniform on compact time intervals.
• TauCeti.Semigroups.IsMDissipative.yosidaLimit_time_add: the semigroup law yosidaLimit A (s + t) = yosidaLimit A s ∘ yosidaLimit A t at nonnegative times.
• TauCeti.Semigroups.IsMDissipative.exists_contractionSemigroup: a densely defined m-dissipative operator gives rise to a contraction semigroup whose orbits are the limits of the Yosida exponentials.

This is the limit stage of the Yosida construction; the generator of yosidaLimitSemigroup is identified with A — the Lumer--Phillips generation theorem — in TauCeti/Analysis/Semigroups/Generation/LumerPhillips.lean.

References

• Engel--Nagel, One-Parameter Semigroups for Linear Evolution Equations, Sections II.3.5 and II.3.8;
• Pazy, Semigroups of Linear Operators and Applications to Partial Differential Equations, Chapter 1, Theorems 4.3 and 5.3.

noncomputable def TauCeti.Semigroups.yosidaLimit {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (A : X →ₗ.[ℝ] X) (t : ℝ) (x : X) : X

The Yosida limit of an unbounded operator A at time t, applied to x: the value limUnder atTop chooses from the family exp (t A_lambda) x.

Being a limUnder, this is a total definition: it names a candidate value for every operator A and every real t, but it is a junk value unless that family actually converges. It is proved to be the limit at nonnegative times in the two supported cases: when A is m-dissipative with dense domain (established below in TauCeti.Semigroups.IsMDissipative.tendsto_yosidaLimit), or when A has dense domain and satisfies the Hille--Yosida resolvent-power bounds (proved in TauCeti.Semigroups.tendsto_yosidaLimit_of_norm_resolvent_pow_le in TauCeti/Analysis/Semigroups/Generation/HilleYosida/Limit.lean). In both cases the compact-time Cauchy estimate gives convergence. Every lemma below that appeals to the limit property carries the relevant hypotheses explicitly.

Equations

• TauCeti.Semigroups.yosidaLimit A t x = Filter.atTop.limUnder fun (lambda : ℝ) => (NormedSpace.exp (t • TauCeti.Semigroups.yosidaApproximation A lambda)) x

theorem TauCeti.Semigroups.tendsto_yosidaLimit_of_cauchySeq {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →ₗ.[ℝ] X) (t : ℝ) (x : X) (h : CauchySeq fun (lambda : ℝ) => (NormedSpace.exp (t • yosidaApproximation A lambda)) x) : Filter.Tendsto (fun (lambda : ℝ) => (NormedSpace.exp (t • yosidaApproximation A lambda)) x) Filter.atTop (nhds (yosidaLimit A t x))

A Cauchy family of Yosida exponentials converges to yosidaLimit, its chosen limUnder value. This exposes the convergence property to downstream modules while keeping the implementation of yosidaLimit hidden.

@[simp]

theorem TauCeti.Semigroups.yosidaLimit_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (A : X →ₗ.[ℝ] X) (x : X) : yosidaLimit A 0 x = x

At time 0 every Yosida exponential is the identity, so the limit is too.

Shared limit-semigroup scaffolding

theorem TauCeti.Semigroups.norm_yosidaLimit_le_of_tendsto_of_norm_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} {t M : ℝ} {x : X} (htend : Filter.Tendsto (fun (lambda : ℝ) => (NormedSpace.exp (t • yosidaApproximation A lambda)) x) Filter.atTop (nhds (yosidaLimit A t x))) (hbound : ∀ᶠ (lambda : ℝ) in Filter.atTop, ‖NormedSpace.exp (t • yosidaApproximation A lambda)‖ ≤ M) : ‖yosidaLimit A t x‖ ≤ M * ‖x‖

An eventual operator bound on the Yosida exponentials passes to the limit.

Shared limit-semigroup constructor

noncomputable def TauCeti.Semigroups.yosidaLimitSemigroupOfTendsto {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {M : ℝ} (htend : ∀ (t : ℝ), 0 ≤ t → ∀ (x : X), Filter.Tendsto (fun (lambda : ℝ) => (NormedSpace.exp (t • yosidaApproximation A lambda)) x) Filter.atTop (nhds (yosidaLimit A t x))) (hunif : ∀ (x : X) (T : ℝ), 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)) (hbound : ∀ (t : ℝ), 0 ≤ t → ∀ᶠ (lambda : ℝ) in Filter.atTop, ‖NormedSpace.exp (t • yosidaApproximation A lambda)‖ ≤ M) : StronglyContinuousSemigroup X

The strongly continuous semigroup obtained from pointwise and uniform convergence of the approximating Yosida semigroups together with an eventual norm bound M.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Semigroups.yosidaLimitSemigroupOfTendsto_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {M : ℝ} (htend : ∀ (t : ℝ), 0 ≤ t → ∀ (x : X), Filter.Tendsto (fun (lambda : ℝ) => (NormedSpace.exp (t • yosidaApproximation A lambda)) x) Filter.atTop (nhds (yosidaLimit A t x))) (hunif : ∀ (x : X) (T : ℝ), 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)) (hbound : ∀ (t : ℝ), 0 ≤ t → ∀ᶠ (lambda : ℝ) in Filter.atTop, ‖NormedSpace.exp (t • yosidaApproximation A lambda)‖ ≤ M) (t : NNReal) (x : X) : ((yosidaLimitSemigroupOfTendsto htend hunif hbound) t) x = yosidaLimit A (↑t) x

Evaluating the limit semigroup at t on x yields yosidaLimit A t x.

@[simp]

theorem TauCeti.Semigroups.yosidaLimitSemigroupOfTendsto_realOperator_apply_of_nonneg {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {M : ℝ} (htend : ∀ (t : ℝ), 0 ≤ t → ∀ (x : X), Filter.Tendsto (fun (lambda : ℝ) => (NormedSpace.exp (t • yosidaApproximation A lambda)) x) Filter.atTop (nhds (yosidaLimit A t x))) (hunif : ∀ (x : X) (T : ℝ), 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)) (hbound : ∀ (t : ℝ), 0 ≤ t → ∀ᶠ (lambda : ℝ) in Filter.atTop, ‖NormedSpace.exp (t • yosidaApproximation A lambda)‖ ≤ M) {t : ℝ} (ht : 0 ≤ t) (x : X) : ((yosidaLimitSemigroupOfTendsto htend hunif hbound).realOperator t) x = yosidaLimit A t x

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

theorem TauCeti.Semigroups.hasGrowthBound_yosidaLimitSemigroupOfTendsto {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {M : ℝ} (hM : 1 ≤ M) (htend : ∀ (t : ℝ), 0 ≤ t → ∀ (x : X), Filter.Tendsto (fun (lambda : ℝ) => (NormedSpace.exp (t • yosidaApproximation A lambda)) x) Filter.atTop (nhds (yosidaLimit A t x))) (hunif : ∀ (x : X) (T : ℝ), 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)) (hbound : ∀ (t : ℝ), 0 ≤ t → ∀ᶠ (lambda : ℝ) in Filter.atTop, ‖NormedSpace.exp (t • yosidaApproximation A lambda)‖ ≤ M) : (yosidaLimitSemigroupOfTendsto htend hunif hbound).HasGrowthBound 0 M

The limit semigroup has growth bound (0, M).

theorem TauCeti.Semigroups.tendsto_yosidaLimitSemigroupOfTendsto {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {M : ℝ} (htend : ∀ (t : ℝ), 0 ≤ t → ∀ (x : X), Filter.Tendsto (fun (lambda : ℝ) => (NormedSpace.exp (t • yosidaApproximation A lambda)) x) Filter.atTop (nhds (yosidaLimit A t x))) (hunif : ∀ (x : X) (T : ℝ), 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)) (hbound : ∀ (t : ℝ), 0 ≤ t → ∀ᶠ (lambda : ℝ) in Filter.atTop, ‖NormedSpace.exp (t • yosidaApproximation A lambda)‖ ≤ M) (t : NNReal) (x : X) : Filter.Tendsto (fun (lambda : ℝ) => (NormedSpace.exp (↑t • yosidaApproximation A lambda)) x) Filter.atTop (nhds (((yosidaLimitSemigroupOfTendsto htend hunif hbound) t) x))

The orbits of the limit semigroup are the limits of the Yosida exponentials.

Existence of the limit

theorem TauCeti.Semigroups.IsMDissipative.tendsto_yosidaLimit {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} (hA : IsMDissipative A) (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))

The defining convergence of the Yosida limit: exp (t A_lambda) x -> yosidaLimit A t x as lambda -> +∞, for every nonnegative time t.

Completeness turns the compact-time Cauchy estimate into convergence to the chosen value limUnder atTop, which is yosidaLimit A t x by definition.

theorem TauCeti.Semigroups.IsMDissipative.tendstoUniformlyOn_exp_yosidaApproximation {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} (hA : IsMDissipative A) (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)

The convergence to the Yosida limit is uniform on every compact time interval.

Linearity and contractivity in the vector variable

theorem TauCeti.Semigroups.IsMDissipative.yosidaLimit_add {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} (hA : IsMDissipative A) (hdense : Dense ↑A.domain) {t : ℝ} (ht : 0 ≤ t) (x y : X) : yosidaLimit A t (x + y) = yosidaLimit A t x + yosidaLimit A t y

The Yosida limit is additive in the vector variable.

theorem TauCeti.Semigroups.IsMDissipative.yosidaLimit_smul {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} (hA : IsMDissipative A) (hdense : Dense ↑A.domain) {t : ℝ} (ht : 0 ≤ t) (c : ℝ) (x : X) : yosidaLimit A t (c • x) = c • yosidaLimit A t x

The Yosida limit is homogeneous in the vector variable.

theorem TauCeti.Semigroups.IsMDissipative.norm_yosidaLimit_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} (hA : IsMDissipative A) (hdense : Dense ↑A.domain) {t : ℝ} (ht : 0 ≤ t) (x : X) : ‖yosidaLimit A t x‖ ≤ ‖x‖

The Yosida limit is contractive: ‖yosidaLimit A t x‖ ≤ ‖x‖ at every nonnegative time.

Each Yosida exponential is a contraction, and the bound passes to the limit.

The semigroup law and continuity in time

theorem TauCeti.Semigroups.IsMDissipative.yosidaLimit_time_add {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} (hA : IsMDissipative A) (hdense : Dense ↑A.domain) {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (x : X) : yosidaLimit A (s + t) x = yosidaLimit A s (yosidaLimit A t x)

The semigroup law for the Yosida limit. At nonnegative times, yosidaLimit A (s + t) x = yosidaLimit A s (yosidaLimit A t x).

The corresponding identity for the approximations is exact; the two error terms it produces are controlled by the contractivity of exp (s A_lambda) and by the two defining convergences.

theorem TauCeti.Semigroups.IsMDissipative.continuousOn_yosidaLimit_Icc {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} (hA : IsMDissipative A) (hdense : Dense ↑A.domain) (x : X) {T : ℝ} (hT : 0 ≤ T) : ContinuousOn (fun (t : ℝ) => yosidaLimit A t x) (Set.Icc 0 T)

The Yosida limit is continuous in time on every compact interval [0, T]: it is a uniform limit there of the continuous orbits of the bounded approximations.

theorem TauCeti.Semigroups.IsMDissipative.continuousOn_yosidaLimit {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} (hA : IsMDissipative A) (hdense : Dense ↑A.domain) (x : X) : ContinuousOn (fun (t : ℝ) => yosidaLimit A t x) (Set.Ici 0)

The Yosida limit is continuous in time on the whole nonnegative half-line.

The contraction semigroup

noncomputable def TauCeti.Semigroups.IsMDissipative.yosidaLimitSemigroup {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} (hA : IsMDissipative A) (hdense : Dense ↑A.domain) : ContractionSemigroup X

The contraction semigroup produced by the Yosida construction. For a densely defined m-dissipative operator A on a real Banach space, the limits of the Yosida exponentials form a strongly continuous contraction semigroup.

Equations

• hA.yosidaLimitSemigroup hdense = { toStronglyContinuousSemigroup := TauCeti.Semigroups.yosidaLimitSemigroupOfTendsto ⋯ ⋯ ⋯, contracting := ⋯ }

@[simp]

theorem TauCeti.Semigroups.IsMDissipative.yosidaLimitSemigroup_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} (hA : IsMDissipative A) (hdense : Dense ↑A.domain) (t : NNReal) (x : X) : ((hA.yosidaLimitSemigroup hdense) t) x = yosidaLimit A (↑t) x

@[simp]

theorem TauCeti.Semigroups.IsMDissipative.yosidaLimitSemigroup_realOperator_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} (hA : IsMDissipative A) (hdense : Dense ↑A.domain) {t : ℝ} (ht : 0 ≤ t) (x : X) : ((hA.yosidaLimitSemigroup hdense).realOperator t) x = yosidaLimit A t x

The real-time orbit of yosidaLimitSemigroup is the Yosida limit at nonnegative times.

theorem TauCeti.Semigroups.IsMDissipative.tendsto_yosidaLimitSemigroup {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} (hA : IsMDissipative A) (hdense : Dense ↑A.domain) (t : NNReal) (x : X) : Filter.Tendsto (fun (lambda : ℝ) => (NormedSpace.exp (↑t • yosidaApproximation A lambda)) x) Filter.atTop (nhds (((hA.yosidaLimitSemigroup hdense) t) x))

The orbits of yosidaLimitSemigroup are exactly the limits of the Yosida exponentials.

theorem TauCeti.Semigroups.IsMDissipative.exists_contractionSemigroup {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} (hA : IsMDissipative A) (hdense : Dense ↑A.domain) : ∃ (S : ContractionSemigroup X), ∀ (t : NNReal) (x : X), Filter.Tendsto (fun (lambda : ℝ) => (NormedSpace.exp (↑t • yosidaApproximation A lambda)) x) Filter.atTop (nhds ((S t) x))

A densely defined m-dissipative operator gives rise to a contraction semigroup, obtained as the strong limit of the semigroups generated by its Yosida approximations.

This is the existence half of the Lumer--Phillips generation theorem; the generator of the resulting semigroup is identified with A in TauCeti/Analysis/Semigroups/Generation/LumerPhillips.lean.