The iterated generator domains of a strongly continuous semigroup are dense

StronglyContinuousSemigroup.dense_domain says that the domain D(A) of the infinitesimal generator is dense. This file proves the same for every iterate: the domain D(Aⁿ) of the n-th iterate of the generator is dense as well, and is preserved by every semigroup operator.

The regularising maps are the powers of the resolvent. R(lambda)ⁿ lands in D(Aⁿ) (TauCeti.resolvent_pow_mem_domainPow), and lambdaⁿ R(lambda)ⁿ converges strongly to the identity as lambda → ∞, so every vector is a limit of vectors of D(Aⁿ). The convergence is proved here at a general growth exponent: the exponent-zero statement TauCeti.Semigroups.tendsto_smul_resolvent_apply_atTop asks for ‖R(lambda)‖ ≤ M / lambda, which a semigroup only satisfies once its growth exponent is at most 0.

Main results

• TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_mem_domainPow: every S t preserves D(Aⁿ).
• TauCeti.Semigroups.StronglyContinuousSemigroup.tendsto_smul_resolventFun_apply: lambda R(lambda) x → x as lambda → ∞.
• TauCeti.Semigroups.StronglyContinuousSemigroup.dense_domainPow: D(Aⁿ) is dense.

References

Engel--Nagel, One-Parameter Semigroups for Linear Evolution Equations, Lemma II.1.3 and Theorem II.1.10; Pazy, Semigroups of Linear Operators and Applications to Partial Differential Equations, Theorem 1.2.7.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_mem_domainPow {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {t : ℝ} (ht : 0 ≤ t) {n : ℕ} {x : X} (hx : x ∈ domainPow S.generator n) : (S.realOperator t) x ∈ domainPow S.generator n

Every semigroup operator preserves each iterated generator domain D(Aⁿ).

Strong convergence of the scaled resolvents

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.tendsto_smul_resolventFun_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {omega M : ℝ} (hb : S.HasGrowthBound omega M) (x : X) : Filter.Tendsto (fun (lambda : ℝ) => lambda • (S.resolventFun hb lambda) x) Filter.atTop (nhds x)

The scaled resolvents converge strongly to the identity. For a C₀-semigroup with growth bound (omega, M), lambda R(lambda) x → x as lambda → ∞, for every x.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.tendsto_pow_smul_resolventFun_pow_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {omega M : ℝ} (hb : S.HasGrowthBound omega M) (n : ℕ) (x : X) : Filter.Tendsto (fun (lambda : ℝ) => lambda ^ n • (S.resolventFun hb lambda ^ n) x) Filter.atTop (nhds x)

The iterated scaled resolvents converge strongly to the identity: lambdaⁿ R(lambda)ⁿ x → x as lambda → ∞.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.dense_domainPow {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) (n : ℕ) : Dense ↑(domainPow S.generator n)

The iterated generator domains are dense. For every n, the domain D(Aⁿ) of the n-th iterate of the infinitesimal generator of a C₀-semigroup is dense in the whole space.

For n = 1 this is StronglyContinuousSemigroup.dense_domain.