Strongly continuous semigroups (Proposition 1.2)

• C0Semigroup 𝕜 X : strongly continuous semigroups T on X (first item of Definition 1.1): T 0 = Id, T (t + s) = T t ∘ T s for t, s ≥ 0, and T t y → y as t → 0⁺ for every y.
• C0Semigroup.exists_exp_bound : ‖T t‖ ≤ M exp(ω t) for t ≥ 0 ([Pazy 1983, Chapter 1, Theorem 2.2], used in the proofs of Theorem 1.5 and Proposition 1.3); proved with the Banach–Steinhaus theorem.
• C0Semigroup.continuousOn_orbit : Proposition 1.2 (prop:pazy-semigroup-solution-continuous), t ↦ T t x° is continuous on ℝ₊.

T is a function ℝ → (X →L[𝕜] X); all axioms only involve nonnegative times, so the values of T t for t < 0 play no role. Completeness of X is assumed where needed.

structure AbstractLinearControl.C0Semigroup (𝕜 : Type u_3) (X : Type u_4) [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] : Type u_4

A strongly continuous semigroup on X (first item of Definition 1.1).

• T : ℝ → X →L[𝕜] X

  the operators T t

• T_zero : self.T 0 = ContinuousLinearMap.id 𝕜 X

  T 0 = Id

• T_add (t s : ℝ) : 0 ≤ t → 0 ≤ s → self.T (t + s) = self.T t ∘SL self.T s

  T (t + s) = T t ∘ T s for t, s ≥ 0

• T_cont (y : X) : Filter.Tendsto (fun (t : ℝ) => (self.T t) y) (nhdsWithin 0 (Set.Ici 0)) (nhds y)

  T t y → y as t → 0⁺, for every y

Exponential bound

theorem AbstractLinearControl.C0Semigroup.exists_bound_near_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (S : C0Semigroup 𝕜 X) [CompleteSpace X] : ∃ τ > 0, ∃ M ≥ 1, ∀ (t : ℝ), 0 ≤ t → t ≤ τ → ‖S.T t‖ ≤ M

First step: ‖T t‖ ≤ M on some interval [0, τ] (Banach–Steinhaus).

theorem AbstractLinearControl.C0Semigroup.exists_exp_bound {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (S : C0Semigroup 𝕜 X) [CompleteSpace X] : ∃ ω ≥ 0, ∃ M ≥ 1, ∀ (t : ℝ), 0 ≤ t → ‖S.T t‖ ≤ M * Real.exp (ω * t)

Exponential bound: ‖T t‖ ≤ M * exp (ω * t) for all t ≥ 0, with ω ≥ 0, M ≥ 1.

Proposition 1.2: continuity of the orbits

theorem AbstractLinearControl.C0Semigroup.orbit_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (S : C0Semigroup 𝕜 X) (y : X) (a h : ℝ) (ha : 0 ≤ a) (hh : 0 ≤ h) : (S.T (a + h)) y - (S.T a) y = (S.T a) ((S.T h) y - y)

T (a + h) y - T a y = T a (T h y - y)

theorem AbstractLinearControl.C0Semigroup.norm_orbit_sub_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (S : C0Semigroup 𝕜 X) (y : X) (a h : ℝ) (ha : 0 ≤ a) (hh : 0 ≤ h) : ‖(S.T (a + h)) y - (S.T a) y‖ ≤ ‖S.T a‖ * ‖(S.T h) y - y‖

‖T (a + h) y - T a y‖ ≤ ‖T a‖ ‖T h y - y‖

theorem AbstractLinearControl.C0Semigroup.continuousOn_orbit {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] (S : C0Semigroup 𝕜 X) [CompleteSpace X] (y : X) : ContinuousOn (fun (t : ℝ) => (S.T t) y) (Set.Ici 0)

Proposition 1.2 (prop:pazy-semigroup-solution-continuous). For every y, t ↦ T t y is continuous on ℝ₊ = [0, ∞).