Complex-linear operators from real strongly continuous semigroups

A strongly continuous semigroup in Tau Ceti acts by real continuous linear maps, including on a complex Banach space regarded as a real Banach space. This file records the additional hypothesis that each operator commutes with complex scalar multiplication and bundles each operator as a complex continuous linear map. It does not introduce a parallel complex semigroup.

Main definitions and results

• StronglyContinuousSemigroup.IsComplexLinear: every semigroup operator is complex linear.
• StronglyContinuousSemigroup.isComplexLinear_iff, IsComplexLinear.map_smul and IsComplexLinear.realOperator_map_smul: its characterisation and accessors.
• StronglyContinuousSemigroup.complexLinearOperator: the operator at a fixed time, bundled over ℂ.
• StronglyContinuousSemigroup.complexLinearOperator_apply: the complex bundle has the same action.
• StronglyContinuousSemigroup.complexLinearOperator_restrictScalars: restriction to ℝ recovers the original semigroup operator.
• StronglyContinuousSemigroup.complexLinearOperator_zero and complexLinearOperator_add: the semigroup law for the bundle.
• StronglyContinuousSemigroup.complexDomain: the generator domain as a complex submodule.
• StronglyContinuousSemigroup.mem_complexDomain_iff: membership agrees with the real domain.
• StronglyContinuousSemigroup.complexGenerator: the real generator bundled as a complex LinearPMap on the same domain.
• StronglyContinuousSemigroup.dense_complexDomain: the complex generator domain is dense.
• StronglyContinuousSemigroup.isClosed_complexGenerator: the complex generator is closed.
• StronglyContinuousSemigroup.complexGenerator_restrictScalars: restricting the complex generator to real scalars recovers the real generator.
• StronglyContinuousSemigroup.isComplexLinear_of_I_smul: commuting with multiplication by i suffices for complex linearity.
• StronglyContinuousSemigroup.mem_domain_iff_of_generator_eq_restrictScalars: the generator domain is the domain of the complex-linear partial map the generator restricts.
• StronglyContinuousSemigroup.isComplexLinear_of_generator_eq_restrictScalars: a semigroup whose generator is the real restriction of a complex-linear partial map is complex linear.
• StronglyContinuousSemigroup.complexGenerator_eq_of_generator_eq_restrictScalars: the complex generator of such a semigroup is that complex-linear partial map.

References

• K.-J. Engel and R. Nagel, One-Parameter Semigroups for Linear Evolution Equations, Section II.2.1 (similar semigroups) and Theorem II.1.4 (the generator determines the semigroup).
• A. Pazy, Semigroups of Linear Operators and Applications to Partial Differential Equations, Theorem 1.2.6.

def TauCeti.Semigroups.StronglyContinuousSemigroup.IsComplexLinear {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) : Prop

A real C₀-semigroup on a complex normed space is complex linear when every operator commutes with complex scalar multiplication.

Equations

• S.IsComplexLinear = ∀ (t : NNReal) (z : ℂ) (x : X), (S t) (z • x) = z • (S t) x

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.isComplexLinear_iff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) : S.IsComplexLinear ↔ ∀ (t : NNReal) (z : ℂ) (x : X), (S t) (z • x) = z • (S t) x

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.IsComplexLinear.map_smul {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] {S : StronglyContinuousSemigroup X} (hS : S.IsComplexLinear) (t : NNReal) (z : ℂ) (x : X) : (S t) (z • x) = z • (S t) x

The operators of a complex-linear semigroup commute with complex scalars.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.IsComplexLinear.realOperator_map_smul {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] {S : StronglyContinuousSemigroup X} (hS : S.IsComplexLinear) (t : ℝ) (z : ℂ) (x : X) : (S.realOperator t) (z • x) = z • (S.realOperator t) x

The real-time operators of a complex-linear semigroup commute with complex scalars.

noncomputable def TauCeti.Semigroups.StronglyContinuousSemigroup.complexLinearOperator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) (t : NNReal) : X →L[ℂ] X

A complex-linear semigroup operator, bundled as a complex continuous linear map.

Equations

• S.complexLinearOperator hS t = { toFun := ⇑(S t), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.complexLinearOperator_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) (t : NNReal) (x : X) : (S.complexLinearOperator hS t) x = (S t) x

The complex-linear bundle has the same pointwise action as the underlying real operator.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.complexLinearOperator_restrictScalars {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) (t : NNReal) : ContinuousLinearMap.restrictScalars ℝ (S.complexLinearOperator hS t) = S t

Restricting the complex-linear bundle to real scalars recovers the semigroup operator.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.complexLinearOperator_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) : S.complexLinearOperator hS 0 = ContinuousLinearMap.id ℂ X

The complex-linear bundle at time 0 is the identity.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.complexLinearOperator_add {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) (s t : NNReal) : S.complexLinearOperator hS (s + t) = S.complexLinearOperator hS s ∘SL S.complexLinearOperator hS t

The semigroup law for the complex-linear bundle.

def TauCeti.Semigroups.StronglyContinuousSemigroup.complexDomain {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) : Submodule ℂ X

The generator domain of a complex-linear semigroup, as a complex submodule.

Equations

• S.complexDomain hS = { carrier := ↑S.domain, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.mem_complexDomain_iff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) (x : X) : x ∈ S.complexDomain hS ↔ x ∈ S.domain

Membership in the complex generator domain is membership in the underlying real domain.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.coe_complexDomain {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) : ↑(S.complexDomain hS) = ↑S.domain

The complex generator domain has the real generator domain as its underlying set.

noncomputable def TauCeti.Semigroups.StronglyContinuousSemigroup.complexGenerator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) : X →ₗ.[ℂ] X

The infinitesimal generator, bundled as a complex linear partial map.

Equations

• S.complexGenerator hS = { domain := S.complexDomain hS, toFun := { toFun := fun (x : ↥(S.complexDomain hS)) => ↑S.generator ⟨↑x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } }

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.complexGenerator_domain {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) : (S.complexGenerator hS).domain = S.complexDomain hS

The complex generator has the complex generator domain.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.complexGenerator_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) (x : ↥(S.complexGenerator hS).domain) : ↑(S.complexGenerator hS) x = ↑S.generator ⟨↑x, ⋯⟩

The complex generator agrees pointwise with the underlying real generator.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.dense_complexDomain {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) : Dense ↑(S.complexDomain hS)

The domain of the complex generator is dense.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.complexGenerator_restrictScalars {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) : LinearPMap.restrictScalars ℝ (S.complexGenerator hS) = S.generator

The real restriction of the complex generator is the real generator.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.isClosed_complexGenerator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) : (S.complexGenerator hS).IsClosed

The complex generator is closed: its graph is that of the real generator.

Complex linearity from the generator

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.isComplexLinear_of_I_smul {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) (h : ∀ (t : NNReal) (x : X), (S t) (Complex.I • x) = Complex.I • (S t) x) : S.IsComplexLinear

A real-linear semigroup commuting with multiplication by i is complex linear.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.mem_domain_iff_of_generator_eq_restrictScalars {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) {A : X →ₗ.[ℂ] X} (hA : S.generator = LinearPMap.restrictScalars ℝ A) {y : X} : y ∈ S.domain ↔ y ∈ A.domain

The generator domain of S is the domain of A when S.generator = A.restrictScalars ℝ.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.isComplexLinear_of_generator_eq_restrictScalars {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) {A : X →ₗ.[ℂ] X} (hA : S.generator = LinearPMap.restrictScalars ℝ A) : S.IsComplexLinear

Complex linearity is read off the generator. A real C₀-semigroup on a complex Banach space whose generator is the real restriction of a complex-linear partial map is complex linear.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.complexGenerator_eq_of_generator_eq_restrictScalars {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℂ X] (S : StronglyContinuousSemigroup X) (hS : S.IsComplexLinear) {A : X →ₗ.[ℂ] X} (hA : S.generator = LinearPMap.restrictScalars ℝ A) : S.complexGenerator hS = A

The complex generator of a complex-linear semigroup whose real generator is the real restriction of A is A itself.