The Lumer--Phillips generation theorem

A densely defined m-dissipative operator A on a real Banach space generates a strongly continuous contraction semigroup. The semigroup itself is built in TauCeti/Analysis/Semigroups/Generation/LimitSemigroup.lean as the limit S(t) x = lim_{lambda -> ∞} exp (t A_lambda) x of the Yosida exponentials.

The reusable generator-identification argument lives in TauCeti/Analysis/Semigroups/Generation/Yosida/Generator.lean. This file supplies its hypotheses: the compact-time convergence defining yosidaLimitSemigroup, convergence of A_lambda x to A x on the dense domain, the contraction bound on the approximating semigroups, and the shared resolvent point 1. Thus the generator of the limit semigroup is A.

Main results

• TauCeti.Semigroups.IsMDissipative.yosidaLimitSemigroup_generator: the generator of the Yosida limit semigroup of a densely defined m-dissipative A is A.
• TauCeti.Semigroups.IsMDissipative.exists_contractionSemigroup_generator_eq: the Lumer--Phillips generation theorem.
• TauCeti.Semigroups.exists_contractionSemigroup_generator_eq_iff: an operator generates a contraction semigroup exactly when it is densely defined and m-dissipative.
• The duality-set characterization with a nonpositive witness for each x ∈ D(A).
• The equivalent universal sign condition for every member of each duality set.

References

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

@[simp]

theorem TauCeti.Semigroups.IsMDissipative.yosidaLimitSemigroup_generator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} (hA : IsMDissipative A) (hdense : Dense ↑A.domain) : (hA.yosidaLimitSemigroup hdense).generator = A

The generator of the Yosida limit semigroup is the operator it was built from. For a densely defined m-dissipative A, the semigroup yosidaLimitSemigroup has generator A.

theorem TauCeti.Semigroups.IsMDissipative.exists_contractionSemigroup_generator_eq {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} (hA : IsMDissipative A) (hdense : Dense ↑A.domain) : ∃ (S : ContractionSemigroup X), S.generator = A

The Lumer--Phillips generation theorem. A densely defined m-dissipative operator on a real Banach space generates a strongly continuous contraction semigroup.

Dissipativity plus the range condition packaged in IsMDissipative is exactly the hypothesis set of Lumer--Phillips; the semigroup produced is the strong limit of the semigroups generated by the Yosida approximations of A.

theorem TauCeti.Semigroups.exists_contractionSemigroup_generator_eq_iff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →ₗ.[ℝ] X) : (∃ (S : ContractionSemigroup X), S.generator = A) ↔ Dense ↑A.domain ∧ IsMDissipative A

Lumer--Phillips as a characterization. An unbounded operator on a real Banach space is the generator of a strongly continuous contraction semigroup if and only if it is densely defined and m-dissipative.

The forward direction is the density of a generator domain together with the converse of Lumer--Phillips; the backward direction is the generation theorem.

theorem TauCeti.Semigroups.exists_contractionSemigroup_generator_eq_iff_exists_mem_dualitySet_apply_nonpos {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →ₗ.[ℝ] X) : (∃ (S : ContractionSemigroup X), S.generator = A) ↔ Dense ↑A.domain ∧ (∀ (x : ↥A.domain), ∃ f ∈ dualitySet ℝ ↑x, f (↑A x) ≤ 0) ∧ ∃ (lambda : ℝ), 0 < lambda ∧ Function.Surjective fun (x : ↥A.domain) => lambda • ↑x - ↑A x

Lumer--Phillips in duality-map form. An unbounded operator on a real Banach space generates a contraction semigroup exactly when it is densely defined, each x ∈ D(A) has a duality-set member f with f (A x) ≤ 0, and lambda • I - A maps D(A) onto X for some lambda > 0.

theorem TauCeti.Semigroups.exists_contractionSemigroup_generator_eq_iff_forall_mem_dualitySet_apply_nonpos {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →ₗ.[ℝ] X) : (∃ (S : ContractionSemigroup X), S.generator = A) ↔ Dense ↑A.domain ∧ (∀ (x : ↥A.domain), ∀ f ∈ dualitySet ℝ ↑x, f (↑A x) ≤ 0) ∧ ∃ (lambda : ℝ), 0 < lambda ∧ Function.Surjective fun (x : ↥A.domain) => lambda • ↑x - ↑A x

Lumer--Phillips with the universal duality-set sign condition. A densely defined operator generates a contraction semigroup exactly when every member of the duality set of each x ∈ D(A) is nonpositive on A x, and the positive resolvent range condition holds.