Complexification of strongly continuous semigroups

A strongly continuous semigroup on a real Banach space extends componentwise to the normed complexification of that space. The resulting semigroup is complex linear. Because the Taylor norm makes complexification isometric on bounded operators, this extension preserves every operator norm and hence every exponential growth bound without changing its constants.

This construction is the real-to-complex bridge for applying complex spectral theory to a real semigroup. In particular, it allows complex resolvent results for complex-linear semigroups to be transported back to real Banach spaces without weakening Hille--Yosida estimates.

Main declarations

• StronglyContinuousSemigroup.complexify: the componentwise complexification of a real strongly continuous semigroup.
• StronglyContinuousSemigroup.isComplexLinear_complexify: the complexified semigroup is complex linear.
• StronglyContinuousSemigroup.hasGrowthBound_complexify_iff: complexification preserves a growth bound with exactly the same constants.
• StronglyContinuousSemigroup.mem_complexify_domain_iff: the generator domain is described componentwise.
• StronglyContinuousSemigroup.complexify_generator_apply: the generator acts componentwise.
• StronglyContinuousSemigroup.mem_complexify_generator_graph_iff: the generator graph is the componentwise complexification of the original graph.
• ContractionSemigroup.complexify: complexification of a contraction semigroup.

References

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

noncomputable def TauCeti.Semigroups.StronglyContinuousSemigroup.complexify {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) : StronglyContinuousSemigroup (Complexification X)

The componentwise complexification of a strongly continuous semigroup on a real Banach space. At time t, its complex-linear operator is the complexification of S t.

Equations

• S.complexify = { toFun := fun (t : NNReal) => ContinuousLinearMap.restrictScalars ℝ (S t).complexify, map_zero' := ⋯, map_add' := ⋯, continuousAt_zero' := ⋯ }

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.complexify_apply_re {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (t : NNReal) (z : Complexification X) : ((S.complexify t) z).re = (S t) z.re

The real part of the complexified orbit is the original orbit of the real part.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.complexify_apply_im {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (t : NNReal) (z : Complexification X) : ((S.complexify t) z).im = (S t) z.im

The imaginary part of the complexified orbit is the original orbit of the imaginary part.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.complexify_apply_ofReal {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (t : NNReal) (x : X) : (S.complexify t) (Complexification.ofReal x) = Complexification.ofReal ((S t) x)

The complexified semigroup extends the original semigroup along the real embedding.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.norm_complexify_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (t : NNReal) : ‖S.complexify t‖ = ‖S t‖

The operator norm at each time is unchanged by complexification.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.complexify_realOperator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (t : ℝ) : S.complexify.realOperator t = ContinuousLinearMap.restrictScalars ℝ (S.realOperator t).complexify

The complexification commutes with the real-time operator shim.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.norm_complexify_realOperator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (t : ℝ) : ‖S.complexify.realOperator t‖ = ‖S.realOperator t‖

The real-time operator norm is unchanged by complexification.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.isComplexLinear_complexify {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) : S.complexify.IsComplexLinear

The complexified semigroup is complex linear.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.complexLinearOperator_complexify {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (t : NNReal) : S.complexify.complexLinearOperator ⋯ t = (S t).complexify

Bundling an operator of the complexified semigroup as complex linear recovers the complexification of the corresponding original operator.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.hasGrowthBound_complexify_iff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (ω M : ℝ) : S.complexify.HasGrowthBound ω M ↔ S.HasGrowthBound ω M

Complexification preserves exponential growth bounds, with exactly the same exponent and multiplicative constant.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.HasGrowthBound.complexify {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {S : StronglyContinuousSemigroup X} {ω M : ℝ} (h : S.HasGrowthBound ω M) : S.complexify.HasGrowthBound ω M

Every growth bound of a real semigroup is a growth bound of its complexification.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.mem_complexify_domain_iff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (z : Complexification X) : z ∈ S.complexify.domain ↔ z.re ∈ S.domain ∧ z.im ∈ S.domain

Membership in the generator domain of the complexified semigroup is componentwise membership in the original generator domain.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.complexify_generator_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {z : Complexification X} (hz : z ∈ S.complexify.domain) : ↑S.complexify.generator ⟨z, ⋯⟩ = { re := ↑S.generator ⟨z.re, ⋯⟩, im := ↑S.generator ⟨z.im, ⋯⟩ }

The generator of the complexified semigroup acts componentwise on its domain.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.complexify_generator_apply_re {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {z : Complexification X} (hz : z ∈ S.complexify.domain) : (↑S.complexify.generator ⟨z, ⋯⟩).re = ↑S.generator ⟨z.re, ⋯⟩

The real part of the complexified generator is the original generator on the real part.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.complexify_generator_apply_im {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {z : Complexification X} (hz : z ∈ S.complexify.domain) : (↑S.complexify.generator ⟨z, ⋯⟩).im = ↑S.generator ⟨z.im, ⋯⟩

The imaginary part of the complexified generator is the original generator on the imaginary part.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.mem_complexify_generator_graph_iff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (z w : Complexification X) : (z, w) ∈ S.complexify.generator.graph ↔ (z.re, w.re) ∈ S.generator.graph ∧ (z.im, w.im) ∈ S.generator.graph

The graph of the generator of the complexified semigroup is obtained by complexifying the graph of the original generator componentwise. Thus Aℂ (x + i y) = A x + i A y, with the domain condition on both components included in the statement.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.mem_complexify_complexGenerator_graph_iff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (z w : Complexification X) : (z, w) ∈ (S.complexify.complexGenerator ⋯).graph ↔ (z.re, w.re) ∈ S.generator.graph ∧ (z.im, w.im) ∈ S.generator.graph

The graph of the complex-linear generator is the componentwise complexification of the original real generator graph. This is the complex-linear form of mem_complexify_generator_graph_iff.

noncomputable def TauCeti.Semigroups.ContractionSemigroup.complexify {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : ContractionSemigroup X) : ContractionSemigroup (Complexification X)

The componentwise complexification of a contraction semigroup.

Equations

• S.complexify = { toStronglyContinuousSemigroup := S.complexify, contracting := ⋯ }

@[simp]

theorem TauCeti.Semigroups.ContractionSemigroup.complexify_toStronglyContinuousSemigroup {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : ContractionSemigroup X) : S.complexify.toStronglyContinuousSemigroup = S.complexify

The underlying C₀-semigroup of a complexified contraction semigroup is the complexification of the underlying C₀-semigroup.

@[simp]

theorem TauCeti.Semigroups.ContractionSemigroup.complexify_apply_re {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : ContractionSemigroup X) (t : NNReal) (z : Complexification X) : ((S.complexify t) z).re = (S t) z.re

The real part of a complexified contraction-semigroup orbit is the original orbit of the real part.

@[simp]

theorem TauCeti.Semigroups.ContractionSemigroup.complexify_apply_im {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : ContractionSemigroup X) (t : NNReal) (z : Complexification X) : ((S.complexify t) z).im = (S t) z.im

The imaginary part of a complexified contraction-semigroup orbit is the original orbit of the imaginary part.

@[simp]

theorem TauCeti.Semigroups.ContractionSemigroup.complexify_apply_ofReal {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : ContractionSemigroup X) (t : NNReal) (x : X) : (S.complexify t) (Complexification.ofReal x) = Complexification.ofReal ((S t) x)

The complexified contraction semigroup extends the original one along the real embedding.

theorem TauCeti.Semigroups.ContractionSemigroup.isComplexLinear_complexify {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : ContractionSemigroup X) : S.complexify.IsComplexLinear

The underlying C₀-semigroup of a complexified contraction semigroup is complex linear.

@[simp]

theorem TauCeti.Semigroups.ContractionSemigroup.norm_complexify_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : ContractionSemigroup X) (t : NNReal) : ‖S.complexify t‖ = ‖S t‖

Complexification preserves the operator norm of a contraction semigroup at every time.