The Laplace-transform resolvent is the resolvent of the generator

This file proves that the Laplace-transform resolvent is also a left inverse of lambda • I - A on the generator domain. Together with the right-inverse identity from TauCeti/Analysis/Semigroups/Resolvent/Basic.lean that identifies it as the resolvent of the generator in the unbounded sense of TauCeti/Analysis/Normed/Operator/Resolvent/Unbounded.lean: StronglyContinuousSemigroup.generator_resolvent_eq says LinearPMap.resolvent S.generator lambda = S.resolvent hb lambda hlambda for lambda beyond the growth exponent.

Everything else here is read off that bridge. The resolvent identity R(lambda) - R(mu) = (mu - lambda) R(lambda) R(mu) and commutativity of resolvents are the abstract LinearPMap.resolvent_sub_resolvent and LinearPMap.resolvent_comm transported along it, rather than separate arguments; the identity is recorded both for resolvent and for resolventFun, the resolvent seen as a function of the spectral parameter alone. The bridge also transports the Laplace-transform norm estimate to the abstract resolvent: ‖R(lambda, A)‖ ≤ M / (lambda - omega). The sharp power estimate is proved from the integral power formula in TauCeti/Analysis/Semigroups/Resolvent/PowerBounds.lean.

References

The argument follows Engel--Nagel, One-Parameter Semigroups for Linear Evolution Equations, Theorem II.1.10: integration of the derivative of exp (-lambda * t) • S(t)x gives the left-inverse formula, from which the algebraic resolvent identity follows. The generation estimates are Theorem II.3.5 there.

@[simp]

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

The Laplace-transform resolvent is a left inverse to lambda • I - A on the generator domain: R(lambda) (lambda x - A x) = x.

The bridge to the resolvent of the generator

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.isResolventAt_generator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) [CompleteSpace X] {omega M : ℝ} (hb : S.HasGrowthBound omega M) {lambda : ℝ} (hlambda : omega < lambda) : S.generator.IsResolventAt lambda (S.resolvent hb lambda hlambda)

For a C₀-semigroup with growth bound (omega, M) and lambda > omega, the Laplace-transform resolvent R(lambda) x = ∫₀^∞ e^{-λt} S(t) x dt inverts lambda • I - A for the generator A: it lands in D(A) (StronglyContinuousSemigroup.resolvent_mem_domain) and is a two-sided inverse there (StronglyContinuousSemigroup.resolventRightInv, StronglyContinuousSemigroup.resolventLeftInv).

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.mem_resolventSet_generator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) [CompleteSpace X] {omega M : ℝ} (hb : S.HasGrowthBound omega M) {lambda : ℝ} (hlambda : omega < lambda) : lambda ∈ S.generator.resolventSet

Every lambda beyond the growth exponent lies in the resolvent set of the generator.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.Ioi_subset_resolventSet_generator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) [CompleteSpace X] {omega M : ℝ} (hb : S.HasGrowthBound omega M) : Set.Ioi omega ⊆ S.generator.resolventSet

The half-line (omega, ∞) lies in the resolvent set of the generator — the hypothesis hres of the Hille--Yosida generation theorem, here in its (already available) converse direction.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.generator_resolvent_eq {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) [CompleteSpace X] {omega M : ℝ} (hb : S.HasGrowthBound omega M) {lambda : ℝ} (hlambda : omega < lambda) : S.generator.resolvent lambda = S.resolvent hb lambda hlambda

The Laplace-transform bridge. The resolvent of the generator, in the unbounded sense, is the Laplace transform R(lambda) x = ∫₀^∞ e^{-λt} S(t) x dt.

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

Hille--Yosida resolvent bound for the resolvent of the generator: ‖R(lambda, A)‖ ≤ M / (lambda - omega).

The resolvent identity

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.resolvent_sub_resolvent_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {omegaLambda MLambda omegaMu MMu : ℝ} [CompleteSpace X] (hbLambda : S.HasGrowthBound omegaLambda MLambda) (hbMu : S.HasGrowthBound omegaMu MMu) (lambda mu : ℝ) (hlambda : omegaLambda < lambda) (hmu : omegaMu < mu) (x : X) : (S.resolvent hbLambda lambda hlambda) x - (S.resolvent hbMu mu hmu) x = (mu - lambda) • (S.resolvent hbLambda lambda hlambda) ((S.resolvent hbMu mu hmu) x)

Pointwise form of the resolvent identity R(lambda) - R(mu) = (mu - lambda) R(lambda) R(mu); the abstract TauCeti.LinearPMap.resolvent_sub_resolvent_apply read through the bridge.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.resolvent_sub_resolvent {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {omegaLambda MLambda omegaMu MMu : ℝ} [CompleteSpace X] (hbLambda : S.HasGrowthBound omegaLambda MLambda) (hbMu : S.HasGrowthBound omegaMu MMu) (lambda mu : ℝ) (hlambda : omegaLambda < lambda) (hmu : omegaMu < mu) : S.resolvent hbLambda lambda hlambda - S.resolvent hbMu mu hmu = (mu - lambda) • S.resolvent hbLambda lambda hlambda ∘SL S.resolvent hbMu mu hmu

The resolvent identity R(lambda) - R(mu) = (mu - lambda) R(lambda) R(mu) as an equality of continuous linear maps.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.resolventFun_sub_resolventFun {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {omega M : ℝ} [CompleteSpace X] (hb : S.HasGrowthBound omega M) {lambda mu : ℝ} (hl : omega < lambda) (hm : omega < mu) : S.resolventFun hb lambda - S.resolventFun hb mu = (mu - lambda) • (S.resolventFun hb lambda * S.resolventFun hb mu)

The resolvent identity for resolventFun, written in the ring X →L[ℝ] X.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.resolvent_comm {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {omegaLambda MLambda omegaMu MMu : ℝ} [CompleteSpace X] (hbLambda : S.HasGrowthBound omegaLambda MLambda) (hbMu : S.HasGrowthBound omegaMu MMu) (lambda mu : ℝ) (hlambda : omegaLambda < lambda) (hmu : omegaMu < mu) : S.resolvent hbLambda lambda hlambda ∘SL S.resolvent hbMu mu hmu = S.resolvent hbMu mu hmu ∘SL S.resolvent hbLambda lambda hlambda

Resolvents at two admissible parameters commute.

@[simp]

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

The contraction resolvent is a left inverse to lambda • I - A on the generator domain.

theorem TauCeti.Semigroups.ContractionSemigroup.resolvent_sub_resolvent {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : ContractionSemigroup X) [CompleteSpace X] (lambda mu : ℝ) (hlambda : 0 < lambda) (hmu : 0 < mu) : S.resolvent lambda hlambda - S.resolvent mu hmu = (mu - lambda) • S.resolvent lambda hlambda ∘SL S.resolvent mu hmu

The resolvent identity for a contraction semigroup.

theorem TauCeti.Semigroups.ContractionSemigroup.resolvent_sub_resolvent_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : ContractionSemigroup X) [CompleteSpace X] (lambda mu : ℝ) (hlambda : 0 < lambda) (hmu : 0 < mu) (x : X) : (S.resolvent lambda hlambda) x - (S.resolvent mu hmu) x = (mu - lambda) • (S.resolvent lambda hlambda) ((S.resolvent mu hmu) x)

Pointwise form of the resolvent identity for a contraction semigroup.

theorem TauCeti.Semigroups.ContractionSemigroup.resolvent_comm {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : ContractionSemigroup X) [CompleteSpace X] (lambda mu : ℝ) (hlambda : 0 < lambda) (hmu : 0 < mu) : S.resolvent lambda hlambda ∘SL S.resolvent mu hmu = S.resolvent mu hmu ∘SL S.resolvent lambda hlambda

Resolvents of a contraction semigroup commute.

theorem TauCeti.Semigroups.ContractionSemigroup.mem_resolventSet_generator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : ContractionSemigroup X) [CompleteSpace X] {lambda : ℝ} (hlambda : 0 < lambda) : lambda ∈ S.generator.resolventSet

Every lambda > 0 lies in the resolvent set of the generator of a contraction semigroup.

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

The resolvent of the generator of a contraction semigroup is its Laplace transform.