The generator determines the semigroup

Two strongly continuous semigroups on a real Banach space with the same infinitesimal generator coincide. The proof is the classical interpolation argument: for x in the common generator domain and a fixed time t, the orbit

u ↦ S (t - u) (T u x)

interpolates between S t x (at u = 0) and T t x (at u = t), and it is constant because its right derivative vanishes: the derivative of the inner factor contributes the vector S (t - u) (A (T u x)), and the derivative of the outer factor contributes its negative.

Differentiating the outer factor requires a two-sided derivative of a generator-domain orbit, which is available at positive times through TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_hasDerivWithinAt_Ici; both contributions are recombined using the joint strong continuity TauCeti.Semigroups.StronglyContinuousSemigroup.tendsto_realOperator_apply from TauCeti/Analysis/Semigroups/GrowthBound.lean.

The concrete identifications this makes available are recorded with the semigroups they identify: a semigroup with vanishing generator is the identity semigroup (TauCeti/Analysis/Semigroups/Identity.lean), and a semigroup whose generator is a bounded operator A is t ↦ exp (t • A) (TauCeti/Analysis/Semigroups/BoundedGenerator/Basic.lean).

Main results

• hasDerivWithinAt_realOperator_apply_realOperator (in the TauCeti.Semigroups.StronglyContinuousSemigroup namespace): the right derivative of a composite orbit u ↦ S (f u) (T u x) is the generator contribution of T, pushed through S (f s), plus the derivative of u ↦ S (f u) (T s x).
• realOperator_apply_eq_of_hasDerivWithinAt_zero (same namespace): a path u ↦ S (f u) (g u) with vanishing right derivative on [0, t) is constant on [0, t].
• TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_eq_of_generator_eq: two semigroups with the same generator agree on the generator domain.
• TauCeti.Semigroups.StronglyContinuousSemigroup.eq_of_generator_eq and TauCeti.Semigroups.StronglyContinuousSemigroup.generator_injective: the generator determines the semigroup.
• TauCeti.Semigroups.ContractionSemigroup.eq_of_generator_eq: the contraction-semigroup form.

References

• K.-J. Engel and R. Nagel, One-Parameter Semigroups for Linear Evolution Equations, Theorem II.1.4.
• A. Pazy, Semigroups of Linear Operators and Applications to Partial Differential Equations, Theorem 1.2.6.

Uniqueness of the semigroup generated by an operator

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.hasDerivWithinAt_realOperator_apply_realOperator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S T : StronglyContinuousSemigroup X) {f : ℝ → ℝ} {x a c : X} {s : ℝ} (hs : 0 ≤ s) (hf : Filter.Tendsto f (nhdsWithin s (Set.Ioi s)) (nhds (f s))) (hf0 : ∀ᶠ (u : ℝ) in nhdsWithin s (Set.Ioi s), 0 ≤ f u) (hquot : Filter.Tendsto (fun (u : ℝ) => (u - s)⁻¹ • ((T.realOperator (u - s)) ((T.realOperator s) x) - (T.realOperator s) x)) (nhdsWithin s (Set.Ioi s)) (nhds a)) (hslope : HasDerivWithinAt (fun (u : ℝ) => (S.realOperator (f u)) ((T.realOperator s) x)) c (Set.Ici s) s) : HasDerivWithinAt (fun (u : ℝ) => (S.realOperator (f u)) ((T.realOperator u) x)) ((S.realOperator (f s)) a + c) (Set.Ici s) s

Differentiating a composite orbit. Along a time reparametrisation f, right-continuous at s and nonnegative near s, if the rebased generator quotient of T at T s x converges to a and u ↦ S (f u) (T s x) has right derivative c at s, then the composite orbit u ↦ S (f u) (T u x) has right derivative S (f s) a + c at s: pushing the quotient through S (f u) produces S (f s) a.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_apply_eq_of_hasDerivWithinAt_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {f : ℝ → ℝ} {g : ℝ → X} {t : ℝ} (hf : ContinuousOn f (Set.Icc 0 t)) (hf0 : ∀ u ∈ Set.Icc 0 t, 0 ≤ f u) (hg : ContinuousOn g (Set.Icc 0 t)) (hderiv : ∀ u ∈ Set.Ico 0 t, HasDerivWithinAt (fun (v : ℝ) => (S.realOperator (f v)) (g v)) 0 (Set.Ici u) u) (u : ℝ) : u ∈ Set.Icc 0 t → (S.realOperator (f u)) (g u) = (S.realOperator (f 0)) (g 0)

A path with vanishing right derivative is constant. If u ↦ S (f u) (g u) has right derivative 0 on [0, t), with f continuous and nonnegative and g continuous on [0, t], then it is constant on [0, t], with value S (f 0) (g 0).

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_eq_of_generator_eq {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {S T : StronglyContinuousSemigroup X} (hgen : S.generator = T.generator) {t : ℝ} (ht : 0 ≤ t) {x : X} (hx : x ∈ T.domain) : (S.realOperator t) x = (T.realOperator t) x

Two strongly continuous semigroups with the same generator agree on the generator domain, at every nonnegative time.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.eq_of_generator_eq {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {S T : StronglyContinuousSemigroup X} (hgen : S.generator = T.generator) : S = T

The generator determines the semigroup: two strongly continuous semigroups on a real Banach space with the same infinitesimal generator are equal ([EN] Thm. II.1.4).

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.generator_injective {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] : Function.Injective generator

The infinitesimal generator is injective on strongly continuous semigroups.

theorem TauCeti.Semigroups.ContractionSemigroup.eq_of_generator_eq {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {S T : ContractionSemigroup X} (hgen : S.generator = T.generator) : S = T

Two contraction semigroups with the same generator are equal.