Smooth vectors of a strongly continuous semigroup

A vector is smooth when it belongs to every iterated domain of the infinitesimal generator. Its semigroup orbit is then smooth on the closed nonnegative half-line, including right derivatives at the origin. More generally, membership in D(Aⁿ) gives Cⁿ regularity. The semigroup preserves smooth vectors, and the generator maps them to smooth vectors.

These facts connect the iterated-domain construction to regularity of the abstract Cauchy problem. The orbit characterization can identify time-smoothed approximants as members of smoothVectors once their orbits are shown to be smooth.

References

Engel--Nagel, One-Parameter Semigroups for Linear Evolution Equations, Lemma II.1.3.

def TauCeti.Semigroups.StronglyContinuousSemigroup.IsSmoothVector {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (x : X) : Prop

A smooth vector belongs to the domain of every power of the generator.

Equations

• S.IsSmoothVector x = ∀ (n : ℕ), x ∈ TauCeti.domainPow S.generator n

noncomputable def TauCeti.Semigroups.StronglyContinuousSemigroup.smoothVectors {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) : Submodule ℝ X

The linear subspace of vectors in every iterated generator domain.

Equations

• S.smoothVectors = ⨅ (n : ℕ), TauCeti.domainPow S.generator n

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.mem_smoothVectors {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {x : X} : x ∈ S.smoothVectors ↔ S.IsSmoothVector x

Membership in the smooth-vector submodule is smoothness of the vector.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.IsSmoothVector.mem_domain {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {x : X} (hx : S.IsSmoothVector x) : x ∈ S.domain

Every smooth vector belongs to the generator domain.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.IsSmoothVector.generator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {x : X} (hx : S.IsSmoothVector x) : S.IsSmoothVector (↑S.generator ⟨x, ⋯⟩)

The generator sends a smooth vector to another smooth vector.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.IsSmoothVector.realOperator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {x : X} (hx : S.IsSmoothVector x) {t : ℝ} (ht : 0 ≤ t) : S.IsSmoothVector ((S.realOperator t) x)

Every semigroup operator preserves smooth vectors.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.contDiffOn_realOperator_of_mem_domainPow {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) (n : ℕ) {x : X} (hx : x ∈ domainPow S.generator n) : ContDiffOn ℝ (↑n) (fun (t : ℝ) => (S.realOperator t) x) (Set.Ici 0)

Membership in D(Aⁿ) gives Cⁿ regularity of the orbit on the nonnegative half-line.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.mem_domainPow_iff_contDiffOn_realOperator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) (n : ℕ) (x : X) : x ∈ domainPow S.generator n ↔ ContDiffOn ℝ (↑n) (fun (t : ℝ) => (S.realOperator t) x) (Set.Ici 0)

The orbit is Cⁿ on the nonnegative half-line exactly when its initial vector belongs to the domain D(Aⁿ). At the boundary, differentiability is understood from the right.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.IsSmoothVector.contDiffOn_realOperator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {x : X} (hx : S.IsSmoothVector x) : ContDiffOn ℝ (↑⊤) (fun (t : ℝ) => (S.realOperator t) x) (Set.Ici 0)

The orbit of a smooth vector is infinitely differentiable on the nonnegative half-line, with one-sided derivatives at time zero.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.isSmoothVector_iff_contDiffOn_realOperator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) (x : X) : S.IsSmoothVector x ↔ ContDiffOn ℝ (↑⊤) (fun (t : ℝ) => (S.realOperator t) x) (Set.Ici 0)

Smooth vectors are precisely those with a smooth orbit on the nonnegative half-line.