Uniformly continuous semigroups

This file proves the bounded-generator characterization of uniformly continuous semigroups. In the standard semigroup terminology, "uniformly continuous" means that the semigroup is continuous in operator norm (it does not mean uniform continuity on the unbounded time interval).

For the nontrivial direction, operator-norm continuity makes the normalized local orbit average

B_t = t⁻¹ ∫₀ᵗ S(s) ds

arbitrarily close to the identity for small positive t. Hence B_t is invertible. Its range is contained in the generator domain by the local-orbit integral identity, so that domain is all of the Banach space. Conversely, a full-domain generator is bounded by the closed graph theorem, and generator uniqueness identifies the semigroup with its operator exponential.

Main results

• StronglyContinuousSemigroup.domain_eq_top_of_continuousAt_zero: operator-norm continuity at zero implies that the generator has full domain.
• StronglyContinuousSemigroup.continuousAt_zero_iff_domain_eq_top: operator-norm continuity at zero is equivalent to boundedness of the generator.
• StronglyContinuousSemigroup.continuous_iff_domain_eq_top: operator-norm continuity is equivalent to boundedness of the generator.

References

• K.-J. Engel and R. Nagel, One-Parameter Semigroups for Linear Evolution Equations, Theorem I.3.7.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.domain_eq_top_of_continuousAt_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) (hS : ContinuousAt (fun (t : NNReal) => S t) 0) : S.domain = ⊤

If a strongly continuous semigroup is continuous in operator norm at zero, then every vector lies in the domain of its generator.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.domain_eq_top_of_continuous {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) (hS : Continuous fun (t : NNReal) => S t) : S.domain = ⊤

If a strongly continuous semigroup is continuous in operator norm, then every vector lies in the domain of its generator.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.continuousAt_zero_iff_domain_eq_top {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) : ContinuousAt (fun (t : NNReal) => S t) 0 ↔ S.domain = ⊤

A strongly continuous semigroup is continuous in operator norm at zero if and only if its generator has full domain. Equivalently, the generator is a bounded operator and the semigroup is its operator exponential.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.continuous_iff_domain_eq_top {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) : (Continuous fun (t : NNReal) => S t) ↔ S.domain = ⊤

A strongly continuous semigroup is continuous in operator norm if and only if its generator has full domain. Equivalently, the generator is a bounded operator and the semigroup is its operator exponential.