Laplace-transform resolvents of strongly continuous semigroups

This file develops the pointwise Bochner-integral resolvent for a C₀-semigroup with a growth bound, proves that it maps into the generator domain, and establishes the right-inverse identity and norm estimate. It also packages the resolvent as a function of the spectral parameter alone (resolventFun, extended by the junk value 0 below the growth exponent), the form in which it is differentiated in TauCeti/Analysis/Semigroups/Resolvent/Deriv.lean.

References

Ported and adapted (Apache 2.0) from mrdouglasny/hille-yosida; references include Engel--Nagel, Linares, Pazy, Hille, and Yosida.

The Resolvent (general growth bound)

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.norm_pow_mul_resolvent_integrand_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {ω M : ℝ} (hb : S.HasGrowthBound ω M) (n : ℕ) (lambda : ℝ) (x : X) {t : ℝ} (ht : 0 ≤ t) : ‖(t ^ n * Real.exp (-(lambda * t))) • (S.realOperator t) x‖ ≤ M * ‖x‖ * (t ^ n * Real.exp (-((lambda - ω) * t)))

The growth-bound estimate for a polynomially weighted Laplace-transform integrand: ‖t^n e^{-λt} S(t) x‖ ≤ M ‖x‖ t^n e^{-(λ-ω)t} for t ≥ 0.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.norm_resolvent_integrand_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {ω M : ℝ} (hb : S.HasGrowthBound ω M) (lambda : ℝ) (x : X) {t : ℝ} (ht : 0 ≤ t) : ‖Real.exp (-(lambda * t)) • (S.realOperator t) x‖ ≤ M * ‖x‖ * Real.exp (-(lambda - ω) * t)

The growth-bound estimate for the integrand in the defining resolvent integral.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.integrableOn_pow_mul_resolvent_integrand {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {ω M : ℝ} (hb : S.HasGrowthBound ω M) (n : ℕ) (lambda : ℝ) (hlam : ω < lambda) (x : X) : MeasureTheory.IntegrableOn (fun (t : ℝ) => (t ^ n * Real.exp (-(lambda * t))) • (S.realOperator t) x) (Set.Ioi 0) MeasureTheory.volume

The polynomially weighted Laplace-transform integrand t^n e^{-λt} S(t) x is integrable on (0, ∞) for ω < λ.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.integrableOn_resolvent_integrand {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {ω M : ℝ} (hb : S.HasGrowthBound ω M) (lambda : ℝ) (hlam : ω < lambda) (x : X) : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.exp (-(lambda * t)) • (S.realOperator t) x) (Set.Ioi 0) MeasureTheory.volume

The integrand in the defining resolvent integral is integrable on (0, ∞) for ω < λ.

noncomputable def TauCeti.Semigroups.StronglyContinuousSemigroup.resolvent {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {ω M : ℝ} (hb : S.HasGrowthBound ω M) (lambda : ℝ) (hlam : ω < lambda) : X →L[ℝ] X

The resolvent R(λ) x = ∫₀^∞ e^{-λt} S(t)x dt of a C₀-semigroup with growth bound (ω, M), for λ > ω. A pointwise X-valued Bochner integral (so it is well-defined for the merely strongly continuous t ↦ S t), with built-in norm bound ‖R λ‖ ≤ M/(λ-ω).

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.resolvent_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {ω M : ℝ} (hb : S.HasGrowthBound ω M) (lambda : ℝ) (hlam : ω < lambda) (x : X) : (S.resolvent hb lambda hlam) x = ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-(lambda * t)) • (S.realOperator t) x

The resolvent in integral form (characteristic lemma).

Resolvent-Generator Interface

The resolvent maps into the generator domain and satisfies the right-inverse identity from [EN] Thm. II.1.10(i) / [Linares] eq. 0.15.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.resolvent_mem_domain {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {ω M : ℝ} (hb : S.HasGrowthBound ω M) (lambda : ℝ) (hlam : ω < lambda) (x : X) : (S.resolvent hb lambda hlam) x ∈ S.domain

The resolvent maps all of X into the domain of the generator ([EN] Thm. II.1.10(i), [Linares] eq. 0.15).

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.resolventRightInv {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {ω M : ℝ} (hb : S.HasGrowthBound ω M) (lambda : ℝ) (hlam : ω < lambda) (x : X) : lambda • (S.resolvent hb lambda hlam) x - ↑S.generator ⟨(S.resolvent hb lambda hlam) x, ⋯⟩ = x

The fundamental resolvent identity: (λI - A) R(λ) x = x.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.resolvent_norm_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {ω M : ℝ} (hb : S.HasGrowthBound ω M) (lambda : ℝ) (hlam : ω < lambda) : ‖S.resolvent hb lambda hlam‖ ≤ M / (lambda - ω)

Hille–Yosida resolvent bound: ‖R λ‖ ≤ M/(λ-ω) for a C₀ semigroup with growth bound (ω, M) and λ > ω (Hille 1948, Yosida 1948; Engel–Nagel Ch. II).

The resolvent as a function of the spectral parameter

StronglyContinuousSemigroup.resolvent carries the proof ω < λ as an argument, so it is not a function of λ alone. The variant below drops that argument, extending the resolvent by the junk value 0 on λ ≤ ω, which is what lets one speak of its limits, derivatives and integrals in λ.

noncomputable def TauCeti.Semigroups.StronglyContinuousSemigroup.resolventFun {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {ω M : ℝ} (hb : S.HasGrowthBound ω M) (lambda : ℝ) : X →L[ℝ] X

The Laplace-transform resolvent of S as a function of the spectral parameter alone, extended by the junk value 0 on λ ≤ ω. Unlike StronglyContinuousSemigroup.resolvent it does not carry the proof ω < λ, so it can be differentiated in λ.

Equations

• S.resolventFun hb lambda = if h : ω < lambda then S.resolvent hb lambda h else 0

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.resolventFun_of_lt {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {ω M : ℝ} (hb : S.HasGrowthBound ω M) {lambda : ℝ} (h : ω < lambda) : S.resolventFun hb lambda = S.resolvent hb lambda h

Above the growth exponent, resolventFun is the Laplace-transform resolvent.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.resolventFun_of_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {ω M : ℝ} (hb : S.HasGrowthBound ω M) {lambda : ℝ} (h : lambda ≤ ω) : S.resolventFun hb lambda = 0

Below the growth exponent, resolventFun takes its junk value 0.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.resolventFun_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {ω M : ℝ} (hb : S.HasGrowthBound ω M) {lambda : ℝ} (h : ω < lambda) (x : X) : (S.resolventFun hb lambda) x = ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-(lambda * t)) • (S.realOperator t) x

resolventFun in integral form.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.resolventFun_norm_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {ω M : ℝ} (hb : S.HasGrowthBound ω M) {lambda : ℝ} (h : ω < lambda) : ‖S.resolventFun hb lambda‖ ≤ M / (lambda - ω)

The Hille--Yosida bound ‖R λ‖ ≤ M/(λ-ω) for resolventFun.

Contraction-semigroup specializations (M = 1, ω = 0)

noncomputable def TauCeti.Semigroups.ContractionSemigroup.resolvent {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : ContractionSemigroup X) (lambda : ℝ) (hlam : 0 < lambda) : X →L[ℝ] X

The resolvent of a contraction semigroup, the (0, 1) case.

Equations

• S.resolvent lambda hlam = S.resolvent ⋯ lambda hlam

theorem TauCeti.Semigroups.ContractionSemigroup.resolvent_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : ContractionSemigroup X) (lambda : ℝ) (hlam : 0 < lambda) (x : X) : (S.resolvent lambda hlam) x = ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-(lambda * t)) • (S.realOperator t) x

The contraction resolvent unfolds to the Laplace-transform integral R(λ) x = ∫₀^∞ e^{-λt} S(t)x dt, the (0, 1) case.

theorem TauCeti.Semigroups.ContractionSemigroup.resolvent_eq_stronglyContinuousSemigroup_resolvent {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : ContractionSemigroup X) (lambda : ℝ) (hlambda : 0 < lambda) : S.resolvent lambda hlambda = S.resolvent ⋯ lambda hlambda

The contraction resolvent is the (0, 1) case of the general semigroup resolvent.

theorem TauCeti.Semigroups.ContractionSemigroup.resolvent_mem_domain {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : ContractionSemigroup X) (lambda : ℝ) (hlam : 0 < lambda) (x : X) : (S.resolvent lambda hlam) x ∈ S.domain

The contraction resolvent maps into the generator domain.

theorem TauCeti.Semigroups.ContractionSemigroup.resolventRightInv {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : ContractionSemigroup X) (lambda : ℝ) (hlam : 0 < lambda) (x : X) : lambda • (S.resolvent lambda hlam) x - ↑S.generator ⟨(S.resolvent lambda hlam) x, ⋯⟩ = x

The contraction resolvent right-inverse identity (λI - A) R(λ) x = x, the (0, 1) case (cf. StronglyContinuousSemigroup.resolventRightInv).

theorem TauCeti.Semigroups.ContractionSemigroup.resolvent_norm_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : ContractionSemigroup X) (lambda : ℝ) (hlam : 0 < lambda) : ‖S.resolvent lambda hlam‖ ≤ 1 / lambda

The contraction resolvent bound ‖R λ‖ ≤ 1/λ, the (0, 1) case.

noncomputable def TauCeti.Semigroups.ContractionSemigroup.resolventFun {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : ContractionSemigroup X) (lambda : ℝ) : X →L[ℝ] X

The resolvent of a contraction semigroup as a function of the spectral parameter alone, the (ω, M) = (0, 1) case of StronglyContinuousSemigroup.resolventFun.

Equations

• S.resolventFun lambda = S.resolventFun ⋯ lambda

theorem TauCeti.Semigroups.ContractionSemigroup.resolventFun_eq {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : ContractionSemigroup X) : S.resolventFun = S.resolventFun ⋯

The contraction resolvent function is the (ω, M) = (0, 1) case of StronglyContinuousSemigroup.resolventFun.

@[simp]

theorem TauCeti.Semigroups.ContractionSemigroup.resolventFun_of_pos {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : ContractionSemigroup X) {lambda : ℝ} (h : 0 < lambda) : S.resolventFun lambda = S.resolvent lambda h

For a positive parameter, resolventFun is the contraction resolvent.

@[simp]

theorem TauCeti.Semigroups.ContractionSemigroup.resolventFun_of_nonpos {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : ContractionSemigroup X) {lambda : ℝ} (h : lambda ≤ 0) : S.resolventFun lambda = 0

For a nonpositive parameter, resolventFun takes its junk value 0.