The resolvent of a complexified strongly continuous semigroup

Let S be a C₀-semigroup on a real Banach space X with generator A, and let S_ℂ be its componentwise complexification on X_ℂ (StronglyContinuousSemigroup.complexify), a complex-linear semigroup whose complex generator A_ℂ acts by A_ℂ (x + i y) = A x + i A y.

This file shows that the resolvent commutes with complexification at real spectral parameters: every real point lambda of the resolvent set of A is a point of the complex resolvent set of A_ℂ, and there

R(lambda, A_ℂ) = R(lambda, A)_ℂ.

No growth bound is needed; the proof goes through the componentwise description of the generator graph and the graph form of LinearPMap.IsResolventAt.

Together with the complex half-plane theory of TauCeti/Analysis/Semigroups/Resolvent/Complex.lean, applied to S_ℂ with the growth bound HasGrowthBound.complexify, this realizes the complex resolvent of a real semigroup: the half-plane omega < re lambda lies in the resolvent set of A_ℂ, the resolvent is holomorphic there and satisfies ‖R(lambda, A_ℂ)ⁿ‖ ≤ M / (re lambda - omega)ⁿ, and on the real axis it is the complexification of the real resolvent of A, with the same norm.

Main results

• StronglyContinuousSemigroup.isResolventAt_complexify_generator: a real inverse of lambda • I - A complexifies to an inverse of lambda • I - A_ℂ over the reals.
• StronglyContinuousSemigroup.resolvent_complexify_generator: the real resolvent of the generator of S_ℂ is the complexified resolvent.
• StronglyContinuousSemigroup.ofReal_mem_resolventSet_complexify_complexGenerator and StronglyContinuousSemigroup.resolvent_complexify_complexGenerator_ofReal: the same statements for the complex generator A_ℂ at the real point (lambda : ℂ).

References

• K.-J. Engel and R. Nagel, One-Parameter Semigroups for Linear Evolution Equations, Sections II.2.1 and IV.1.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.isResolventAt_complexify_generator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {lambda : ℝ} {R : X →L[ℝ] X} (h : S.generator.IsResolventAt lambda R) : S.complexify.generator.IsResolventAt lambda (ContinuousLinearMap.restrictScalars ℝ R.complexify)

A real inverse R of lambda • I - A, with A the generator of S, complexifies to an inverse of lambda • I - A_ℂ for the generator A_ℂ of the complexified semigroup.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.mem_resolventSet_complexify_generator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {lambda : ℝ} (h : lambda ∈ S.generator.resolventSet) : lambda ∈ S.complexify.generator.resolventSet

Every real point of the resolvent set of the generator of S lies in the resolvent set of the generator of the complexified semigroup.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.resolvent_complexify_generator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {lambda : ℝ} (h : lambda ∈ S.generator.resolventSet) : S.complexify.generator.resolvent lambda = ContinuousLinearMap.restrictScalars ℝ (S.generator.resolvent lambda).complexify

The resolvent commutes with complexification, read over the reals: at a point lambda of the resolvent set of A, the resolvent of the generator of S_ℂ is the complexification of R(lambda, A).

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ofReal_mem_resolventSet_complexify_complexGenerator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {lambda : ℝ} (h : lambda ∈ S.generator.resolventSet) : ↑lambda ∈ (S.complexify.complexGenerator ⋯).resolventSet

Every real point lambda of the resolvent set of A gives the point (lambda : ℂ) of the complex resolvent set of the complex generator A_ℂ of the complexified semigroup.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.resolvent_complexify_complexGenerator_ofReal {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {lambda : ℝ} (h : lambda ∈ S.generator.resolventSet) : (S.complexify.complexGenerator ⋯).resolvent ↑lambda = (S.generator.resolvent lambda).complexify

The complex resolvent on the real axis. At a real point lambda of the resolvent set of A, the resolvent of the complex generator A_ℂ of the complexified semigroup is the complexification of R(lambda, A).