Identifying the generator of a Yosida limit semigroup

This file isolates the final, common step in generation theorems proved by Yosida approximation. Let A be an unbounded operator and suppose that the bounded semigroups

exp (t A_lambda), where A_lambda = lambda ^ 2 R(lambda, A) - lambda I,

converge to a strongly continuous semigroup S: at each nonnegative time on a vector x of D(A), and uniformly on compact time intervals on the orbit of its image A x. If the operators A_lambda converge to A on D(A) and the approximating semigroups are norm bounded on each compact time interval, then A is a restriction of the generator of S.

The proof passes the bounded Duhamel identity

exp (t A_lambda) x - x = integral_0^t exp (u A_lambda) (A_lambda x) du

to the limit. For x in D(A), the integrands converge uniformly to S(u) (A x): one error is the compact-time convergence of the orbit of A x, and the other is controlled by the time-local operator bound and A_lambda x -> A x. Only the integrand needs uniform convergence; the left side of the identity passes to the limit at the single time t. The resulting integrated identity makes the generator difference quotients converge to A x. A shared resolvent point of A and the generator then upgrades the restriction to equality.

This is the generator-identification rung that follows the construction of the limit semigroup in a generation theorem. The Lumer--Phillips theorem in TauCeti/Analysis/Semigroups/Generation/LumerPhillips.lean supplies the hypotheses with the contraction bound 1; TauCeti/Analysis/Semigroups/Generation/HilleYosida/Generation.lean supplies them with the general Hille--Yosida growth constant M.

Main results

• TauCeti.Semigroups.StronglyContinuousSemigroup.le_generator_of_yosidaApproximation: the original operator is a restriction of the generator of the compact-time limit semigroup.
• TauCeti.Semigroups.StronglyContinuousSemigroup.generator_eq_of_yosidaApproximation: a shared resolvent point identifies the generator with the original operator.

References

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

Convergence of the Duhamel integrands

The integrated Cauchy problem

Identification of the generator

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.le_generator_of_yosidaApproximation {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {A : X →ₗ.[ℝ] X} (happrox : ∀ (x : ↥A.domain), Filter.Tendsto (fun (lambda : ℝ) => (yosidaApproximation A lambda) ↑x) Filter.atTop (nhds (↑A x))) (hpoint : ∀ (x : ↥A.domain) {t : ℝ}, 0 ≤ t → Filter.Tendsto (fun (lambda : ℝ) => (NormedSpace.exp (t • yosidaApproximation A lambda)) ↑x) Filter.atTop (nhds ((S.realOperator t) ↑x))) (huniform : ∀ (x : ↥A.domain) {T : ℝ}, 0 ≤ T → TendstoUniformlyOn (fun (lambda u : ℝ) => (NormedSpace.exp (u • yosidaApproximation A lambda)) (↑A x)) (fun (u : ℝ) => (S.realOperator u) (↑A x)) Filter.atTop (Set.Icc 0 T)) (hbound : ∀ {T : ℝ}, 0 < T → ∃ (K : ℝ), ∀ᶠ (lambda : ℝ) in Filter.atTop, ∀ u ∈ Set.Icc 0 T, ‖NormedSpace.exp (u • yosidaApproximation A lambda)‖ ≤ K) : A ≤ S.generator

If Yosida exponentials converge to S — at each nonnegative time on the orbit of a domain vector, and uniformly on compact time intervals on the orbit of its image — the approximating generators converge to A on its domain, and the exponentials are bounded in operator norm on each compact time interval, then A is a restriction of the generator of S.

The hypotheses are stated independently so the theorem applies both to the contraction estimates in Lumer--Phillips and to the general power estimates in Hille--Yosida.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.generator_eq_of_yosidaApproximation {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {A : X →ₗ.[ℝ] X} {lambda : ℝ} (hres : lambda ∈ A.resolventSet) (hgenres : lambda ∈ S.generator.resolventSet) (happrox : ∀ (x : ↥A.domain), Filter.Tendsto (fun (mu : ℝ) => (yosidaApproximation A mu) ↑x) Filter.atTop (nhds (↑A x))) (hpoint : ∀ (x : ↥A.domain) {t : ℝ}, 0 ≤ t → Filter.Tendsto (fun (mu : ℝ) => (NormedSpace.exp (t • yosidaApproximation A mu)) ↑x) Filter.atTop (nhds ((S.realOperator t) ↑x))) (huniform : ∀ (x : ↥A.domain) {T : ℝ}, 0 ≤ T → TendstoUniformlyOn (fun (mu u : ℝ) => (NormedSpace.exp (u • yosidaApproximation A mu)) (↑A x)) (fun (u : ℝ) => (S.realOperator u) (↑A x)) Filter.atTop (Set.Icc 0 T)) (hbound : ∀ {T : ℝ}, 0 < T → ∃ (K : ℝ), ∀ᶠ (mu : ℝ) in Filter.atTop, ∀ u ∈ Set.Icc 0 T, ‖NormedSpace.exp (u • yosidaApproximation A mu)‖ ≤ K) : S.generator = A

A compact-time Yosida limit semigroup has generator A. In addition to the convergence and boundedness hypotheses giving A ≤ generator S, it suffices that A and the generator have one shared resolvent point.

This is the reusable generator-identification step of a Yosida-approximation generation theorem; IsMDissipative.yosidaLimitSemigroup_generator is the Lumer--Phillips instance.