Yosida approximations

This file constructs the bounded approximations used in the generation theorems for strongly continuous semigroups. For an operator A whose resolvent at lambda > 0 satisfies the contraction bound, its Yosida approximation is

A_lambda = lambda ^ 2 R(lambda, A) - lambda I = lambda A R(lambda, A).

The resolvent estimate lambda ‖R(lambda, A)‖ ≤ 1 makes lambda R(lambda, A) a contraction. Splitting the exponential of t A_lambda into the commuting scalar and resolvent parts then proves that exp (t A_lambda) is a contraction for every t ≥ 0. Thus each approximation generates a uniformly continuous contraction semigroup. This is the bounded stage of the Yosida construction.

The convergence stage follows. It is stated against a resolvent bound ‖R(lambda, A)‖ ≤ M / lambda rather than against dissipativity, because the Hille--Yosida generation theorem needs the same estimates at a growth constant larger than one: for a densely defined operator with that bound, lambda R(lambda, A) converges strongly to the identity, hence A_lambda x converges to A x on D(A).

The compact-time Cauchy property of the associated semigroups needs a second, independent hypothesis: a uniform bound ‖exp (s A_lambda)‖ ≤ M on the Yosida exponentials, which the Duhamel comparison contributes squared, as the factor M ^ 2. Those two statements therefore carry two constants, the resolvent constant, written K there, and the exponential constant M. An m-dissipative operator supplies both hypotheses with K = M = 1, its exponential bound being the contraction estimate TauCeti.Semigroups.norm_exp_smul_yosidaApproximation_le_one; under the Hille--Yosida bounds on all resolvent powers the exponential bound is instead TauCeti.Semigroups.norm_exp_smul_yosidaApproximation_le. The later generation argument defines the limit of the approximating semigroups.

Main results

• TauCeti.Semigroups.yosidaApproximation: the bounded operator A_lambda.
• TauCeti.Semigroups.yosidaApproximation_apply_eq_smul_apply_resolvent: the identity A_lambda x = lambda A R(lambda, A) x.
• TauCeti.Semigroups.yosidaSemigroup: the uniformly continuous contraction semigroup generated by A_lambda.
• TauCeti.Semigroups.tendsto_smul_resolvent_apply_atTop: the strong convergence lambda R(lambda, A) x -> x for a densely defined operator obeying the resolvent bound.
• TauCeti.Semigroups.tendsto_yosidaApproximation_apply_atTop: the convergence A_lambda x -> A x on the domain of A.
• TauCeti.Semigroups.exp_yosidaApproximation_uniformCauchySeqOn_compact and TauCeti.Semigroups.exp_yosidaApproximation_uniformCauchySeqOn_compact_of_mem: the Yosida semigroups are uniformly Cauchy on compact time intervals, on every vector and on domain vectors.
• TauCeti.Semigroups.IsMDissipative.tendsto_smul_resolvent_apply_atTop, TauCeti.Semigroups.IsMDissipative.tendsto_yosidaApproximation_apply_atTop and TauCeti.Semigroups.IsMDissipative.exp_yosidaApproximation_uniformCauchySeqOn_compact: the three convergence statements for an m-dissipative operator, the case K = M = 1.

References

Engel--Nagel, One-Parameter Semigroups for Linear Evolution Equations, Section II.3.5; Pazy, Semigroups of Linear Operators and Applications to Partial Differential Equations, Chapter 1.

noncomputable def TauCeti.Semigroups.yosidaApproximation {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (A : X →ₗ.[ℝ] X) (lambda : ℝ) : X →L[ℝ] X

The Yosida approximation of an unbounded operator A at lambda: A_lambda = lambda ^ 2 R(lambda, A) - lambda I.

The definition is meaningful when lambda belongs to the resolvent set of A; its algebraic API carries that membership explicitly, while the norm estimates carry the resolvent bound they use.

Equations

• TauCeti.Semigroups.yosidaApproximation A lambda = lambda ^ 2 • A.resolvent lambda - lambda • 1

@[simp]

theorem TauCeti.Semigroups.yosidaApproximation_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (A : X →ₗ.[ℝ] X) (lambda : ℝ) (x : X) : (yosidaApproximation A lambda) x = lambda ^ 2 • (A.resolvent lambda) x - lambda • x

Pointwise form of the definition of the Yosida approximation.

theorem TauCeti.Semigroups.yosidaApproximation_apply_eq_smul_apply_resolvent {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} {lambda : ℝ} (hlambda : lambda ∈ A.resolventSet) (x : X) : (yosidaApproximation A lambda) x = lambda • ↑A ⟨(A.resolvent lambda) x, ⋯⟩

At a point of the resolvent set, the Yosida approximation is lambda A R(lambda, A) pointwise.

theorem TauCeti.Semigroups.yosidaApproximation_comm {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} {lambda mu : ℝ} (hlambda : lambda ∈ A.resolventSet) (hmu : mu ∈ A.resolventSet) : Commute (yosidaApproximation A lambda) (yosidaApproximation A mu)

Yosida approximations at two resolvent points commute.

theorem TauCeti.Semigroups.norm_yosidaApproximation_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} {lambda : ℝ} (hres : lambda * ‖A.resolvent lambda‖ ≤ 1) (hlambda : 0 < lambda) : ‖yosidaApproximation A lambda‖ ≤ 2 * lambda

The Yosida approximation has the elementary bound ‖A_lambda‖ ≤ 2 lambda.

theorem TauCeti.Semigroups.exp_yosidaApproximation {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} (lambda t : ℝ) : NormedSpace.exp (t • yosidaApproximation A lambda) = NormedSpace.exp (-(t * lambda) • 1) * NormedSpace.exp ((t * lambda ^ 2) • A.resolvent lambda)

Split the exponential of a Yosida approximation into its commuting scalar and resolvent factors: exp (t A_lambda) = exp (-t lambda I) exp (t lambda² R(lambda, A)).

theorem TauCeti.Semigroups.norm_exp_smul_yosidaApproximation_le_one {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {lambda t : ℝ} (hres : lambda * ‖A.resolvent lambda‖ ≤ 1) (hlambda : 0 < lambda) (ht : 0 ≤ t) : ‖NormedSpace.exp (t • yosidaApproximation A lambda)‖ ≤ 1

The exponential of a positive-time multiple of a Yosida approximation is contractive.

noncomputable def TauCeti.Semigroups.yosidaSemigroup {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →ₗ.[ℝ] X) (lambda : ℝ) (hres : lambda * ‖A.resolvent lambda‖ ≤ 1) (hlambda : 0 < lambda) : ContractionSemigroup X

The uniformly continuous contraction semigroup generated by the Yosida approximation.

Equations

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

@[simp]

theorem TauCeti.Semigroups.yosidaSemigroup_toStronglyContinuousSemigroup {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →ₗ.[ℝ] X) (lambda : ℝ) (hres : lambda * ‖A.resolvent lambda‖ ≤ 1) (hlambda : 0 < lambda) : (yosidaSemigroup A lambda hres hlambda).toStronglyContinuousSemigroup = StronglyContinuousSemigroup.ofBounded (yosidaApproximation A lambda)

The C₀-semigroup underlying the Yosida semigroup is the bounded-generator semigroup of the Yosida approximation.

@[simp]

theorem TauCeti.Semigroups.yosidaSemigroup_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →ₗ.[ℝ] X) (lambda : ℝ) (hres : lambda * ‖A.resolvent lambda‖ ≤ 1) (hlambda : 0 < lambda) (t : NNReal) : (yosidaSemigroup A lambda hres hlambda) t = NormedSpace.exp (↑t • yosidaApproximation A lambda)

The Yosida semigroup is the exponential of the Yosida approximation.

theorem TauCeti.Semigroups.continuous_yosidaSemigroup {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →ₗ.[ℝ] X) (lambda : ℝ) (hres : lambda * ‖A.resolvent lambda‖ ≤ 1) (hlambda : 0 < lambda) : Continuous fun (t : NNReal) => (yosidaSemigroup A lambda hres hlambda) t

The Yosida semigroup is continuous in operator norm, not merely strongly continuous.

theorem TauCeti.Semigroups.yosidaSemigroup_generator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →ₗ.[ℝ] X) (lambda : ℝ) (hres : lambda * ‖A.resolvent lambda‖ ≤ 1) (hlambda : 0 < lambda) : (yosidaSemigroup A lambda hres hlambda).generator = (↑(yosidaApproximation A lambda)).toPMap ⊤

The generator of the Yosida semigroup is the everywhere-defined Yosida approximation.

Strong convergence of the approximations

The estimates of this section carry the resolvent bound ‖R(lambda, A)‖ ≤ M / lambda as an explicit hypothesis rather than assuming dissipativity, since the Hille--Yosida generation theorem needs them at a growth constant M larger than one. An m-dissipative operator is the case M = 1, recorded by the IsMDissipative specializations at the end of the file.

theorem TauCeti.Semigroups.norm_smul_resolvent_apply_sub_self_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} {lambda M : ℝ} (hlambda : lambda ∈ A.resolventSet) (hbound : ‖A.resolvent lambda‖ ≤ M / lambda) (x : ↥A.domain) : ‖lambda • (A.resolvent lambda) ↑x - ↑x‖ ≤ M * ‖↑A x‖ / lambda

On the domain of A, the scaled resolvent differs from the identity by at most M ‖A x‖ / lambda:

‖lambda R(lambda, A) x - x‖ ≤ M ‖A x‖ / lambda,

whenever lambda is a resolvent point with ‖R(lambda, A)‖ ≤ M / lambda. This is the quantitative core of the strong convergence lambda R(lambda, A) -> I.

theorem TauCeti.Semigroups.tendsto_smul_resolvent_apply_atTop_of_mem {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} {M : ℝ} (hres : ∀ (lambda : ℝ), 0 < lambda → lambda ∈ A.resolventSet) (hbound : ∀ (lambda : ℝ), 0 < lambda → ‖A.resolvent lambda‖ ≤ M / lambda) (x : ↥A.domain) : Filter.Tendsto (fun (lambda : ℝ) => lambda • (A.resolvent lambda) ↑x) Filter.atTop (nhds ↑x)

On D(A), lambda R(lambda, A) x tends to x as lambda -> +∞ under the resolvent bound ‖R(lambda, A)‖ ≤ M / lambda. Density of the domain is not needed for this domain-restricted form.

theorem TauCeti.Semigroups.norm_smul_resolvent_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} {lambda M : ℝ} (hlambda : 0 < lambda) (hbound : ‖A.resolvent lambda‖ ≤ M / lambda) : ‖lambda • A.resolvent lambda‖ ≤ M

Under the resolvent bound ‖R(lambda, A)‖ ≤ M / lambda at a positive lambda, the scaled resolvent lambda R(lambda, A) has norm at most M.

theorem TauCeti.Semigroups.tendsto_smul_resolvent_apply_atTop {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} {M : ℝ} (hres : ∀ (lambda : ℝ), 0 < lambda → lambda ∈ A.resolventSet) (hbound : ∀ (lambda : ℝ), 0 < lambda → ‖A.resolvent lambda‖ ≤ M / lambda) (hdense : Dense ↑A.domain) (x : X) : Filter.Tendsto (fun (lambda : ℝ) => lambda • (A.resolvent lambda) x) Filter.atTop (nhds x)

For a densely defined operator obeying the resolvent bound ‖R(lambda, A)‖ ≤ M / lambda, the scaled resolvents converge strongly to the identity on the whole Banach space:

lambda R(lambda, A) x -> x as lambda -> +∞.

The uniform bound ‖lambda R(lambda, A)‖ ≤ M extends the domain estimate to all vectors by density.

theorem TauCeti.Semigroups.yosidaApproximation_apply_eq_smul_resolvent_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} {lambda : ℝ} (hlambda : lambda ∈ A.resolventSet) (x : ↥A.domain) : (yosidaApproximation A lambda) ↑x = lambda • (A.resolvent lambda) (↑A x)

At a resolvent point, the Yosida approximation acts on x ∈ D(A) as A_lambda x = lambda R(lambda, A) (A x).

theorem TauCeti.Semigroups.tendsto_yosidaApproximation_apply_atTop {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} {M : ℝ} (hres : ∀ (lambda : ℝ), 0 < lambda → lambda ∈ A.resolventSet) (hbound : ∀ (lambda : ℝ), 0 < lambda → ‖A.resolvent lambda‖ ≤ M / lambda) (hdense : Dense ↑A.domain) (x : ↥A.domain) : Filter.Tendsto (fun (lambda : ℝ) => (yosidaApproximation A lambda) ↑x) Filter.atTop (nhds (↑A x))

Under the resolvent bound ‖R(lambda, A)‖ ≤ M / lambda and density of the domain, the Yosida approximations converge strongly to the original operator on its domain: A_lambda x -> A x for every x ∈ D(A).

Compact-time Cauchy convergence of the approximating semigroups

The two statements below take independent resolvent and exponential bounds, with constants K and M respectively. For a dissipative operator the exponential bound is the contraction estimate TauCeti.Semigroups.norm_exp_smul_yosidaApproximation_le_one; under the Hille--Yosida resolvent power bounds for a general growth constant it is TauCeti.Semigroups.norm_exp_smul_yosidaApproximation_le.

theorem TauCeti.Semigroups.exp_yosidaApproximation_uniformCauchySeqOn_compact_of_mem {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {K M : ℝ} (hres : ∀ (lambda : ℝ), 0 < lambda → lambda ∈ A.resolventSet) (hbound : ∀ (lambda : ℝ), 0 < lambda → ‖A.resolvent lambda‖ ≤ K / lambda) (hexp : ∀ (lambda : ℝ), 0 < lambda → ∀ (s : ℝ), 0 ≤ s → ‖NormedSpace.exp (s • yosidaApproximation A lambda)‖ ≤ M) (hdense : Dense ↑A.domain) (x : ↥A.domain) {T : ℝ} (hT : 0 ≤ T) : UniformCauchySeqOn (fun (lambda t : ℝ) => (NormedSpace.exp (t • yosidaApproximation A lambda)) ↑x) Filter.atTop (Set.Icc 0 T)

The bounded Yosida semigroups are Cauchy on domain vectors, uniformly on every compact time interval. Explicitly, for T ≥ 0, the vectors exp (t A_lambda) x are uniformly Cauchy for 0 ≤ t ≤ T as lambda -> +∞, whenever x ∈ D(A).

The resolvent bound has constant K, while the independent exponential bound has constant M. The comparison estimate reduces the result to the convergence A_lambda x -> A x proved above, at the cost of the factor M ^ 2 from the two exponential factors of the Duhamel formula.

theorem TauCeti.Semigroups.exp_yosidaApproximation_uniformCauchySeqOn_compact {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {K M : ℝ} (hres : ∀ (lambda : ℝ), 0 < lambda → lambda ∈ A.resolventSet) (hbound : ∀ (lambda : ℝ), 0 < lambda → ‖A.resolvent lambda‖ ≤ K / lambda) (hexp : ∀ (lambda : ℝ), 0 < lambda → ∀ (s : ℝ), 0 ≤ s → ‖NormedSpace.exp (s • yosidaApproximation A lambda)‖ ≤ M) (hdense : Dense ↑A.domain) (x : X) {T : ℝ} (hT : 0 ≤ T) : UniformCauchySeqOn (fun (lambda t : ℝ) => (NormedSpace.exp (t • yosidaApproximation A lambda)) x) Filter.atTop (Set.Icc 0 T)

The bounded Yosida semigroups are Cauchy uniformly on every compact time interval, on every vector of the Banach space.

This is the compact-time Cauchy estimate from which a candidate pointwise limit family is defined; later arguments establish its semigroup structure and identify its generator as A. The domain case is TauCeti.Semigroups.exp_yosidaApproximation_uniformCauchySeqOn_compact_of_mem; the uniform bound ‖exp (s A_lambda)‖ ≤ M extends it to the whole space by density of D(A), independently of the resolvent-bound constant K.

The m-dissipative case

An m-dissipative operator has every positive lambda in its resolvent set with ‖R(lambda, A)‖ ≤ 1 / lambda, and its Yosida exponentials are contractions, so it supplies the hypotheses of the results above with both constants equal to one.

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

For a densely defined m-dissipative operator, the scaled resolvents converge strongly to the identity on the whole Banach space: lambda R(lambda, A) x -> x as lambda -> +∞.

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

For a densely defined m-dissipative operator, the Yosida approximations converge strongly to the original operator on its domain: A_lambda x -> A x for every x ∈ D(A).

theorem TauCeti.Semigroups.IsMDissipative.exp_yosidaApproximation_uniformCauchySeqOn_compact {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) : UniformCauchySeqOn (fun (lambda t : ℝ) => (NormedSpace.exp (t • yosidaApproximation A lambda)) x) Filter.atTop (Set.Icc 0 T)

For a densely defined m-dissipative operator, the bounded Yosida semigroups are Cauchy uniformly on every compact time interval, on every vector of the Banach space. This is the compact-time Cauchy estimate from which the contraction semigroup generated by A is built.