Invariance of the generator domain

This file proves that every operator of a strongly continuous semigroup preserves the domain of its infinitesimal generator and commutes with the generator there. The mechanism is StronglyContinuousSemigroup.tendsto_genQuot_map_of_commute: a bounded operator commuting with the semigroup pushes the generator difference quotient through, so it maps the generator domain to itself and commutes with the generator.

References

The argument follows Engel--Nagel, One-Parameter Semigroups for Linear Evolution Equations, Lemma II.1.3(ii): apply the bounded semigroup operator to the defining difference-quotient limit.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.tendsto_genQuot_map_of_commute {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (T : X →L[ℝ] X) (hT : ∀ (s : NNReal) (x : X), (S s) (T x) = T ((S s) x)) {x y : X} (h : Filter.Tendsto (fun (t : ℝ) => (1 / t) • ((S.realOperator t) x - x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds y)) : Filter.Tendsto (fun (t : ℝ) => (1 / t) • ((S.realOperator t) (T x) - T x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (T y))

A bounded operator commuting with the semigroup pushes the generator difference quotient through: the quotient based at T x is T applied to the quotient based at x.

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

Every semigroup operator preserves the domain of the infinitesimal generator.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.generator_map {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (s : NNReal) (x : ↥S.domain) : ↑S.generator ⟨(S s) ↑x, ⋯⟩ = (S s) (↑S.generator ⟨↑x, ⋯⟩)

The infinitesimal generator commutes with every semigroup operator on its domain.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_mem_domain {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {s : ℝ} (hs : 0 ≤ s) {x : X} (hx : x ∈ S.domain) : (S.realOperator s) x ∈ S.domain

Real-time form of domain invariance at nonnegative times.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_generator_map {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {s : ℝ} (hs : 0 ≤ s) (x : ↥S.domain) : ↑S.generator ⟨(S.realOperator s) ↑x, ⋯⟩ = (S.realOperator s) (↑S.generator ⟨↑x, ⋯⟩)

Real-time form of generator commutation at nonnegative times.