Generators of strongly continuous semigroups

This file defines the infinitesimal generator as a LinearPMap, exposes domain membership through the explicit right-difference-quotient limit, and proves the local orbit-integral lemmas giving density of the generator domain.

References

Ported and adapted (Apache 2.0) from mrdouglasny/hille-yosida; references include Engel--Nagel, Linares, Pazy, Hille, and Yosida.

The Infinitesimal Generator

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

The domain D(A) of the generator, as a ℝ-submodule of X.

Equations

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

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

The infinitesimal generator A as an unbounded operator (LinearPMap), A x = lim_{t→0⁺} (S t x - x)/t on the domain D(A) where the limit exists ([EN] Def. II.1.2). Modelled as X →ₗ.[ℝ] X so it composes with Mathlib's unbounded-operator API.

Equations

• S.generator = { domain := S.domain, toFun := { toFun := fun (x : ↥S.domain) => Classical.choose ⋯, map_add' := ⋯, map_smul' := ⋯ } }

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.generator_domain {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) : S.generator.domain = S.domain

S.generator.domain is the generator domain submodule.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.mem_domain_iff_tendsto {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (x : X) : x ∈ S.domain ↔ ∃ (y : X), Filter.Tendsto (fun (t : ℝ) => (1 / t) • ((S.realOperator t) x - x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds y)

A vector lies in the generator domain iff its difference quotient (S t x - x)/t converges as t → 0⁺ ([EN] Def. II.1.2).

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.generator_tendsto {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (x : ↥S.domain) : Filter.Tendsto (fun (t : ℝ) => (1 / t) • ((S.realOperator t) ↑x - ↑x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (↑S.generator ⟨↑x, ⋯⟩))

Characteristic property of the generator: for x in the domain, the difference quotient (S t x - x)/t converges to S.generator x as t → 0⁺ ([EN] Def. II.1.2).

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.generator_tendsto_comp_sub_const {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (x : ↥S.domain) (s : ℝ) : Filter.Tendsto (fun (u : ℝ) => (u - s)⁻¹ • ((S.realOperator (u - s)) ↑x - ↑x)) (nhdsWithin s (Set.Ioi s)) (nhds (↑S.generator ⟨↑x, ⋯⟩))

The generator difference quotient, rebased at s: the defining quotient of S.generator at x (generator_tendsto), precomposed with u ↦ u - s so that it approaches s from the right rather than 0.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.generator_eq_of_tendsto {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {x : X} (hx : x ∈ S.domain) {y : X} (h : Filter.Tendsto (fun (t : ℝ) => (1 / t) • ((S.realOperator t) x - x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds y)) : ↑S.generator ⟨x, ⋯⟩ = y

Eliminator for the generator: if the difference quotient (S t x - x)/t of an x ∈ D(A) converges to y, then A x = y.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.le_generator_of_forall_tendsto {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {A : X →ₗ.[ℝ] X} (h : ∀ (x : ↥A.domain), Filter.Tendsto (fun (t : ℝ) => (1 / t) • ((S.realOperator t) ↑x - ↑x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (↑A x))) : A ≤ S.generator

If the generator difference quotient of every vector of A.domain converges to A x, then A is a restriction of the generator.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.generator_eq_toPMap_top_of_forall_tendsto {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (L : X →ₗ[ℝ] X) (h : ∀ (x : X), Filter.Tendsto (fun (t : ℝ) => (1 / t) • ((S.realOperator t) x - x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (L x))) : S.domain = ⊤ ∧ S.generator = L.toPMap ⊤

If every generator difference quotient converges to L x for a linear operator L, then the generator domain is the whole space and the generator is L as a total LinearPMap.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.tendsto_average_orbit_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) (x : X) : Filter.Tendsto (fun (t : ℝ) => (1 / t) • ∫ (u : ℝ) in Set.Ioc 0 t, (S.realOperator u) x) (nhdsWithin 0 (Set.Ioi 0)) (nhds x)

The integral average (1/t) • ∫_{(0,t]} S(u)x du of the orbit tends to x as t → 0⁺.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.integral_orbit_mem_domain {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) (x : X) {t : ℝ} (ht : 0 < t) : ∫ (u : ℝ) in Set.Ioc 0 t, (S.realOperator u) x ∈ S.domain

The local orbit integral ∫₀ᵗ S(u)x du lies in the generator domain D(A) ([EN] Lemma II.1.3).

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.generator_integral_orbit {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) (x : X) {t : ℝ} (ht : 0 < t) : ↑S.generator ⟨∫ (u : ℝ) in Set.Ioc 0 t, (S.realOperator u) x, ⋯⟩ = (S.realOperator t) x - x

The generator value on the local orbit integral: A (∫₀ᵗ S(u)x du) = S t x - x ([EN] Lemma II.1.3).

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.dense_domain {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) : Dense ↑S.domain

The generator domain of a strongly continuous semigroup is dense ([EN] Lemma II.1.3 and its density corollary).

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.continuousLinearMap_ext_of_eqOn_domain {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {f g : X →L[ℝ] X} (h : ∀ x ∈ S.domain, f x = g x) : f = g

Two continuous linear maps that agree on the (dense) generator domain are equal.