Closedness of semigroup generators

This file proves that the infinitesimal generator of a strongly continuous semigroup on a real Banach space is a closed LinearPMap. The proof uses the Laplace-transform resolvent: for any parameter above a growth exponent, the generator graph is the equalizer

R(lambda) (lambda x - y) = x.

The forward implication is the resolvent left-inverse identity on the generator domain. The reverse implication uses that the resolvent maps into the domain and is a right inverse to lambda I - A. Since the resolvent is bounded, the equalizer is closed.

Main results

• TauCeti.Semigroups.StronglyContinuousSemigroup.mem_generator_graph_iff_resolvent_eq: membership in the generator graph is characterized by one resolvent equation.
• TauCeti.Semigroups.StronglyContinuousSemigroup.isClosed_generator: the generator of every strongly continuous semigroup is closed.

References

• K.-J. Engel and R. Nagel, One-Parameter Semigroups for Linear Evolution Equations, Proposition II.1.4.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.mem_generator_graph_iff_resolvent_eq {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {omega M : ℝ} (hb : S.HasGrowthBound omega M) (lambda : ℝ) (hlambda : omega < lambda) (p : X × X) : p ∈ S.generator.graph ↔ (S.resolvent hb lambda hlambda) (lambda • p.1 - p.2) = p.1

A pair (x, y) belongs to the graph of the generator precisely when applying an admissible resolvent to lambda x - y recovers x.

This characterization presents the graph as the equalizer of two continuous maps and is also a convenient elimination rule when a resolvent equation is easier to establish than domain membership directly.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.isClosed_generator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) : S.generator.IsClosed

The infinitesimal generator of a strongly continuous semigroup on a real Banach space is a closed linear partial map.