The complex resolvent of a strongly continuous semigroup

A C₀-semigroup acting by complex-linear operators on a complex Banach space X has a complex generator A (TauCeti.Semigroups.StronglyContinuousSemigroup.complexGenerator), an unbounded operator over ℂ. This file locates the open half-plane {lambda | omega < re lambda} of a growth bound (omega, M) inside the complex resolvent set of A, identifies the resolvent there with the Laplace transform

R(lambda, A) x = ∫₀^∞ exp (-lambda t) S(t) x dt,

bounds it by M / (re lambda - omega), and concludes that lambda ↦ R(lambda, A) is holomorphic on that half-plane.

The Laplace-transform resolvent of TauCeti/Analysis/Semigroups/Resolvent/Basic.lean is a real-variable construction: the semigroup is indexed by nonnegative reals and acts by real bounded operators, so it only produces real points of the resolvent set. Two bridges cross to the complex picture. Moving parallel to the imaginary axis is the phase shift t ↦ exp (-i b t) S(t), whose generator is A - i b (TauCeti.Semigroups.StronglyContinuousSemigroup.complexGenerator_phaseShift) and whose growth bound is that of S; moving from a real to a complex scalar field is TauCeti.LinearPMap.mem_resolventSet_restrictScalars_iff, which upgrades a bounded real-linear inverse of mu • I - A to the complex resolvent. Holomorphy is then the abstract LinearPMap.analyticOnNhd_resolvent restricted to the half-plane.

Main results

• TauCeti.Semigroups.StronglyContinuousSemigroup.mem_resolventSet_complexGenerator and TauCeti.Semigroups.StronglyContinuousSemigroup.setOf_lt_re_subset_resolventSet_complexGenerator: the half-plane omega < re lambda lies in the complex resolvent set.
• TauCeti.Semigroups.StronglyContinuousSemigroup.resolvent_complexGenerator_apply: the complex resolvent is the Laplace transform of the semigroup.
• TauCeti.Semigroups.StronglyContinuousSemigroup.norm_resolvent_complexGenerator_le and TauCeti.Semigroups.StronglyContinuousSemigroup.norm_resolvent_complexGenerator_pow_le: the Hille--Yosida bounds ‖R(lambda, A)ⁿ‖ ≤ M / (re lambda - omega)ⁿ.
• TauCeti.Semigroups.StronglyContinuousSemigroup.analyticOnNhd_resolvent_complexGenerator: the complex resolvent is holomorphic on the half-plane.

References

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

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.mem_resolventSet_complexGenerator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] [CompleteSpace X] {omega M : ℝ} {lambda : ℂ} (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) (hb : S.HasGrowthBound omega M) (hlambda : omega < lambda.re) : lambda ∈ (S.complexGenerator hS).resolventSet

The complex resolvent set of the generator contains the half-plane of the growth bound. Every lambda with omega < re lambda is a resolvent point of the complex generator.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.restrictScalars_resolvent_complexGenerator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] [CompleteSpace X] {omega M : ℝ} {lambda : ℂ} (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) (hb : S.HasGrowthBound omega M) (hlambda : omega < lambda.re) : ContinuousLinearMap.restrictScalars ℝ ((S.complexGenerator hS).resolvent lambda) = (S.phaseShift hS lambda.im).resolvent ⋯ lambda.re hlambda

The resolvent of the complex generator at a point of the open half-plane omega < re lambda, read over the reals, is the Laplace-transform resolvent of the phase-shifted semigroup t ↦ exp (-i (im lambda) t) S(t) at the real point re lambda.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.setOf_lt_re_subset_resolventSet_complexGenerator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] [CompleteSpace X] {omega M : ℝ} (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) (hb : S.HasGrowthBound omega M) : {z : ℂ | omega < z.re} ⊆ (S.complexGenerator hS).resolventSet

The open half-plane omega < re lambda of a growth bound (omega, M) lies in the complex resolvent set of the generator.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.resolvent_complexGenerator_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] [CompleteSpace X] {omega M : ℝ} {lambda : ℂ} (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) (hb : S.HasGrowthBound omega M) (hlambda : omega < lambda.re) (x : X) : ((S.complexGenerator hS).resolvent lambda) x = ∫ (t : ℝ) in Set.Ioi 0, Complex.exp (-(lambda * ↑t)) • (S.realOperator t) x

The complex Laplace-transform bridge. On the half-plane omega < re lambda the resolvent of the complex generator is the pointwise Bochner integral R(lambda, A) x = ∫₀^∞ exp (-lambda t) S(t) x dt.

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

The Hille--Yosida bound at a complex spectral parameter: on the half-plane of a growth bound (omega, M), ‖R(lambda, A)‖ ≤ M / (re lambda - omega).

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.norm_resolvent_complexGenerator_pow_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] [CompleteSpace X] {omega M : ℝ} {lambda : ℂ} (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) (hb : S.HasGrowthBound omega M) (hlambda : omega < lambda.re) (n : ℕ) : ‖(S.complexGenerator hS).resolvent lambda ^ n‖ ≤ M / (lambda.re - omega) ^ n

The Hille--Yosida power bounds at a complex spectral parameter: on the half-plane of a growth bound (omega, M), ‖R(lambda, A)ⁿ‖ ≤ M / (re lambda - omega)ⁿ for every n.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.analyticOnNhd_resolvent_complexGenerator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] [CompleteSpace X] {omega M : ℝ} (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) (hb : S.HasGrowthBound omega M) : AnalyticOnNhd ℂ (S.complexGenerator hS).resolvent {z : ℂ | omega < z.re}

The resolvent of a C₀-semigroup is holomorphic. On the half-plane omega < re lambda of a growth bound (omega, M), the resolvent of the complex generator is analytic in operator norm.