Dissipative operators

This file introduces dissipativity for a (possibly unbounded) operator A : X →ₗ.[ℝ] X on a real Banach space, in the resolvent-range form

lambda * ‖x‖ ≤ ‖lambda • x - A x‖ for all lambda > 0 and all x ∈ D(A),

which is the notion available in a general Banach space (the Hilbert-space characterization ⟪A x, x⟫ ≤ 0 is a specialization, proved in TauCeti/Analysis/Semigroups/Dissipative/Hilbert.lean).

The elementary API records what the inequality buys: an a priori estimate ‖x‖ ≤ ‖y‖ / lambda for solutions of lambda x - A x = y, injectivity of lambda • I - A on D(A), and stability under restriction and under nonnegative scalar multiples. Adding the range condition — lambda • I - A onto X for some lambda > 0 — gives m-dissipativity (IsMDissipative). On a Banach space that single point is enough: inverting lambda • I - A and expanding a Neumann series propagates the range condition from lambda to every mu ∈ (0, 2 lambda), and iterating that step along the geometric sequence (3/2)^n lambda covers all of (0, ∞), so mu • I - A : D(A) → X is bijective for every mu > 0. Equivalently, every positive mu belongs to the resolvent set, and the resolvent satisfies ‖R(mu, A)‖ ≤ 1 / mu.

The file then connects dissipativity to C₀-semigroups. For a semigroup with growth bound (ω, M) and lambda > ω, the Laplace-transform resolvent turns the bound ‖R(lambda)‖ ≤ M / (lambda - ω) into the resolvent-range inequality

‖x‖ ≤ M / (lambda - ω) * ‖lambda • x - A x‖ for x ∈ D(A),

so that lambda • I - A : D(A) → X is bijective for every lambda > ω — that is, (ω, ∞) lies in the resolvent set of the generator. Specializing to (ω, M) = (0, 1) gives the converse of the Lumer--Phillips theorem: the generator of a contraction semigroup is dissipative.

Main results

• TauCeti.Semigroups.IsDissipative, TauCeti.Semigroups.IsMDissipative: the dissipativity and m-dissipativity predicates.
• TauCeti.Semigroups.IsDissipative.smul_sub_surjective_of_lt_two_mul and TauCeti.Semigroups.IsMDissipative.smul_sub_surjective: on a Banach space the range condition at one positive lambda propagates to every positive lambda.
• TauCeti.Semigroups.IsMDissipative.mem_resolventSet and TauCeti.Semigroups.IsMDissipative.norm_resolvent_le: every positive real is a resolvent point, with the contraction bound ‖R(lambda, A)‖ ≤ 1 / lambda.
• TauCeti.Semigroups.StronglyContinuousSemigroup.norm_le_norm_smul_sub_generator: the resolvent-range inequality at a general growth bound (ω, M).
• TauCeti.Semigroups.StronglyContinuousSemigroup.smul_sub_generator_bijective: lambda • I - A is bijective from D(A) onto X for lambda > ω.
• TauCeti.Semigroups.ContractionSemigroup.isDissipative_generator and TauCeti.Semigroups.ContractionSemigroup.isMDissipative_generator: the generator of a contraction semigroup is dissipative, indeed m-dissipative.

References

Engel--Nagel, One-Parameter Semigroups for Linear Evolution Equations, Section II.3.b (dissipativity and the Lumer--Phillips theorem); Pazy, Semigroups of Linear Operators and Applications to Partial Differential Equations, Chapter 1, Theorem 4.3.

Dissipativity

def TauCeti.Semigroups.IsDissipative {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (A : X →ₗ.[ℝ] X) : Prop

An unbounded operator A : X →ₗ.[ℝ] X is dissipative when lambda * ‖x‖ ≤ ‖lambda • x - A x‖ for every lambda > 0 and every x in its domain.

This is the Banach-space form of the condition: it says exactly that lambda • I - A is injective on D(A) with ‖(lambda • I - A)⁻¹‖ ≤ 1 / lambda on its range, for every lambda > 0. In a Hilbert space it is equivalent to ⟪A x, x⟫ ≤ 0.

Equations

• TauCeti.Semigroups.IsDissipative A = ∀ (lambda : ℝ), 0 < lambda → ∀ (x : ↥A.domain), lambda * ‖↑x‖ ≤ ‖lambda • ↑x - ↑A x‖

theorem TauCeti.Semigroups.isDissipative_iff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} : IsDissipative A ↔ ∀ (lambda : ℝ), 0 < lambda → ∀ (x : ↥A.domain), lambda * ‖↑x‖ ≤ ‖lambda • ↑x - ↑A x‖

IsDissipative A unfolds to its defining inequality: lambda * ‖x‖ ≤ ‖lambda • x - A x‖ for every lambda > 0 and every x ∈ D(A).

theorem TauCeti.Semigroups.IsDissipative.norm_le_of_smul_sub_eq {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} (hA : IsDissipative A) {lambda : ℝ} (hlambda : 0 < lambda) {x : ↥A.domain} {y : X} (h : lambda • ↑x - ↑A x = y) : ‖↑x‖ ≤ ‖y‖ / lambda

The a priori estimate carried by dissipativity: a solution of lambda x - A x = y obeys ‖x‖ ≤ ‖y‖ / lambda.

theorem TauCeti.Semigroups.IsDissipative.smul_sub_injective {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} (hA : IsDissipative A) {lambda : ℝ} (hlambda : 0 < lambda) : Function.Injective fun (x : ↥A.domain) => lambda • ↑x - ↑A x

A dissipative operator has lambda • I - A injective on its domain, for every lambda > 0.

theorem TauCeti.Semigroups.IsDissipative.of_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A B : X →ₗ.[ℝ] X} (hB : IsDissipative B) (hAB : A ≤ B) : IsDissipative A

Dissipativity passes to restrictions: if A ≤ B as unbounded operators and B is dissipative, then so is A.

theorem TauCeti.Semigroups.isDissipative_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] : IsDissipative 0

The zero operator, defined on all of X, is dissipative.

theorem TauCeti.Semigroups.IsDissipative.smul {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} (hA : IsDissipative A) {c : ℝ} (hc : 0 ≤ c) : IsDissipative (c • A)

A nonnegative scalar multiple of a dissipative operator is dissipative.

Maximal dissipativity

def TauCeti.Semigroups.IsMDissipative {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (A : X →ₗ.[ℝ] X) : Prop

An unbounded operator is m-dissipative (maximally dissipative) when it is dissipative and lambda • I - A maps D(A) onto X for some lambda > 0.

The range condition is what upgrades the one-sided estimate of IsDissipative to a genuine resolvent, and one positive lambda already suffices: over a Banach space it propagates to every lambda > 0 (IsMDissipative.smul_sub_surjective), so that lambda • I - A : D(A) → X is bijective there (IsMDissipative.mem_resolventSet and LinearPMap.smul_sub_bijective), with inverse bounded by 1 / lambda through IsDissipative.norm_le_of_smul_sub_eq. Asking for a single lambda is the form the hypothesis takes in the Lumer--Phillips generation theorem — that a densely defined m-dissipative operator is the generator of a contraction semigroup — proved as IsMDissipative.exists_contractionSemigroup_generator_eq; its converse half is ContractionSemigroup.isMDissipative_generator below.

Equations

• TauCeti.Semigroups.IsMDissipative A = (TauCeti.Semigroups.IsDissipative A ∧ ∃ (lambda : ℝ), 0 < lambda ∧ Function.Surjective fun (x : ↥A.domain) => lambda • ↑x - ↑A x)

theorem TauCeti.Semigroups.isMDissipative_iff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} : IsMDissipative A ↔ IsDissipative A ∧ ∃ (lambda : ℝ), 0 < lambda ∧ Function.Surjective fun (x : ↥A.domain) => lambda • ↑x - ↑A x

IsMDissipative A unfolds to its defining conjunction: A is dissipative and lambda • I - A maps D(A) onto X for some lambda > 0.

theorem TauCeti.Semigroups.IsDissipative.isMDissipative {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} (hA : IsDissipative A) {lambda : ℝ} (hlambda : 0 < lambda) (hrange : Function.Surjective fun (x : ↥A.domain) => lambda • ↑x - ↑A x) : IsMDissipative A

A dissipative operator whose lambda • I - A maps D(A) onto X for a single lambda > 0 is m-dissipative.

theorem TauCeti.Semigroups.IsMDissipative.isDissipative {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} (hA : IsMDissipative A) : IsDissipative A

An m-dissipative operator is dissipative.

theorem TauCeti.Semigroups.IsMDissipative.exists_smul_sub_surjective {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} (hA : IsMDissipative A) : ∃ (lambda : ℝ), 0 < lambda ∧ Function.Surjective fun (x : ↥A.domain) => lambda • ↑x - ↑A x

The range condition of an m-dissipative operator: lambda • I - A maps D(A) onto X for at least one lambda > 0.

theorem TauCeti.Semigroups.IsDissipative.smul_sub_surjective_of_lt_two_mul {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} (hA : IsDissipative A) {lambda mu : ℝ} (hlambda : 0 < lambda) (hrange : Function.Surjective fun (x : ↥A.domain) => lambda • ↑x - ↑A x) (hmu : 0 < mu) (hmu' : mu < 2 * lambda) : Function.Surjective fun (x : ↥A.domain) => mu • ↑x - ↑A x

The range condition propagates along a Neumann series. If A is dissipative and lambda • I - A maps D(A) onto X, then so does mu • I - A for every mu in the interval (0, 2 lambda).

Dissipativity makes lambda • I - A : D(A) → X a bijection whose inverse J is bounded by 1 / lambda, and mu • I - A = (I - (lambda - mu) • J) ∘ (lambda • I - A). The first factor is invertible because ‖(lambda - mu) • J‖ ≤ |lambda - mu| / lambda < 1, which is exactly the constraint 0 < mu < 2 lambda.

theorem TauCeti.Semigroups.IsMDissipative.smul_sub_surjective {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} (hA : IsMDissipative A) {lambda : ℝ} (hlambda : 0 < lambda) : Function.Surjective fun (x : ↥A.domain) => lambda • ↑x - ↑A x

The range condition of an m-dissipative operator holds at every positive lambda, not just at the one its definition provides: propagate the given lambda₀ through IsDissipative.smul_sub_surjective_of_lt_two_mul along the geometric sequence (3/2)^n lambda₀, which passes every positive real.

theorem TauCeti.Semigroups.IsMDissipative.mem_resolventSet {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} (hA : IsMDissipative A) {lambda : ℝ} (hlambda : 0 < lambda) : lambda ∈ A.resolventSet

Every positive real lies in the resolvent set of an m-dissipative operator.

theorem TauCeti.Semigroups.IsMDissipative.norm_resolvent_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} (hA : IsMDissipative A) {lambda : ℝ} (hlambda : 0 < lambda) : ‖A.resolvent lambda‖ ≤ lambda⁻¹

The resolvent of an m-dissipative operator satisfies the contraction bound ‖R(lambda, A)‖ ≤ 1 / lambda at every lambda > 0.

theorem TauCeti.Semigroups.IsMDissipative.mul_norm_resolvent_le_one {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} (hA : IsMDissipative A) {lambda : ℝ} (hlambda : 0 < lambda) : lambda * ‖A.resolvent lambda‖ ≤ 1

The scalar form of the contraction bound for the resolvent of an m-dissipative operator: lambda * ‖R(lambda, A)‖ ≤ 1 for every lambda > 0.

The generator of a C₀-semigroup

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.norm_le_norm_smul_sub_generator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {ω M : ℝ} (hb : S.HasGrowthBound ω M) {lambda : ℝ} (hlambda : ω < lambda) (x : ↥S.generator.domain) : ‖↑x‖ ≤ M / (lambda - ω) * ‖lambda • ↑x - ↑S.generator x‖

Resolvent-range inequality. For a C₀-semigroup with growth bound (ω, M) and lambda > ω, every x ∈ D(A) satisfies ‖x‖ ≤ M / (lambda - ω) * ‖lambda x - A x‖.

This is the Hille--Yosida resolvent bound ‖R(lambda)‖ ≤ M / (lambda - ω) read backwards through the left-inverse identity R(lambda) (lambda x - A x) = x.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.smul_sub_generator_injective {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {ω M : ℝ} (hb : S.HasGrowthBound ω M) {lambda : ℝ} (hlambda : ω < lambda) : Function.Injective fun (x : ↥S.generator.domain) => lambda • ↑x - ↑S.generator x

For lambda beyond the growth exponent, lambda • I - A is injective on D(A): the resolvent is a left inverse of it.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.smul_sub_generator_surjective {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {ω M : ℝ} (hb : S.HasGrowthBound ω M) {lambda : ℝ} (hlambda : ω < lambda) : Function.Surjective fun (x : ↥S.generator.domain) => lambda • ↑x - ↑S.generator x

For lambda beyond the growth exponent, lambda • I - A maps D(A) onto X: the resolvent supplies the preimage.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.smul_sub_generator_bijective {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {ω M : ℝ} (hb : S.HasGrowthBound ω M) {lambda : ℝ} (hlambda : ω < lambda) : Function.Bijective fun (x : ↥S.generator.domain) => lambda • ↑x - ↑S.generator x

Every lambda beyond the growth exponent lies in the resolvent set of the generator: lambda • I - A : D(A) → X is bijective.

theorem TauCeti.Semigroups.ContractionSemigroup.isDissipative_generator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : ContractionSemigroup X) : IsDissipative S.generator

Converse of the Lumer--Phillips theorem: the generator of a contraction semigroup is dissipative.

It is the (ω, M) = (0, 1) case of the resolvent-range inequality StronglyContinuousSemigroup.norm_le_norm_smul_sub_generator. Together with StronglyContinuousSemigroup.smul_sub_generator_surjective and the density of the generator domain, it shows that the hypotheses of the Lumer--Phillips generation theorem are also necessary.

theorem TauCeti.Semigroups.ContractionSemigroup.isMDissipative_generator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : ContractionSemigroup X) : IsMDissipative S.generator

The generator of a contraction semigroup is m-dissipative. This is the full converse of the Lumer--Phillips theorem apart from the density of the domain (which is StronglyContinuousSemigroup.dense_domain): dissipativity is ContractionSemigroup.isDissipative_generator and the range condition is witnessed at lambda = 1 by the surjectivity of lambda • I - A that the resolvent supplies (indeed at every lambda > 0, by StronglyContinuousSemigroup.smul_sub_generator_surjective).

theorem TauCeti.Semigroups.ContractionSemigroup.norm_le_of_smul_sub_generator_eq {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : ContractionSemigroup X) {lambda : ℝ} (hlambda : 0 < lambda) {x : ↥S.generator.domain} {y : X} (h : lambda • ↑x - ↑S.generator x = y) : ‖↑x‖ ≤ ‖y‖ / lambda

The a priori estimate for the generator of a contraction semigroup: a solution of lambda x - A x = y has ‖x‖ ≤ ‖y‖ / lambda.