The generator of a similar semigroup

The transported semigroup S.similar e of TauCeti.Analysis.Semigroups.Similarity has the transported generator: the domain is the image of D(A) under e, and the action is e ∘ A ∘ e⁻¹.

The first application is a commutation criterion. A semigroup whose generator commutes with an invertible operator J has J ∘ S t ∘ J⁻¹ with the same generator, so by uniqueness it agrees with S; this is how complex linearity of a semigroup is read off its generator.

Main definitions and results

• TauCeti.Semigroups.StronglyContinuousSemigroup.mem_similar_domain_iff: y is in the transported generator domain iff e⁻¹ y is in the original one.
• TauCeti.Semigroups.StronglyContinuousSemigroup.similar_generator_apply: the transported generator is e ∘ A ∘ e⁻¹.
• TauCeti.Semigroups.StronglyContinuousSemigroup.similar_eq_self_of_generator_comm and map_comm_of_generator_comm: the commutation criterion, S.similar e = S when e commutes with the generator, so S t commutes with e.

References

Engel--Nagel, One-Parameter Semigroups for Linear Evolution Equations, Section II.2.1.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.mem_similar_domain_iff {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (S : StronglyContinuousSemigroup X) (e : X ≃L[ℝ] Y) (y : Y) : y ∈ (S.similar e).domain ↔ e.symm y ∈ S.domain

y lies in the generator domain of the transported semigroup iff e⁻¹ y lies in the generator domain of S.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.similar_generator_apply {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (S : StronglyContinuousSemigroup X) (e : X ≃L[ℝ] Y) {y : Y} (hy : y ∈ (S.similar e).domain) : ↑(S.similar e).generator ⟨y, ⋯⟩ = e (↑S.generator ⟨e.symm y, ⋯⟩)

The generator of the transported semigroup is e ∘ A ∘ e⁻¹.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.similar_eq_self_of_generator_comm {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) (e : X ≃L[ℝ] X) (hdom : ∀ (x : X), e x ∈ S.domain ↔ x ∈ S.domain) (hcomm : ∀ (x : X) (hx : x ∈ S.generator.domain), ↑S.generator ⟨e x, ⋯⟩ = e (↑S.generator ⟨x, hx⟩)) : S.similar e = S

Commutation criterion. A C₀-semigroup whose generator commutes with an invertible operator e (in the sense that e maps the generator domain onto itself and intertwines the generator) is invariant under conjugation by e: S.similar e = S.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.map_comm_of_generator_comm {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) (e : X ≃L[ℝ] X) (hdom : ∀ (x : X), e x ∈ S.domain ↔ x ∈ S.domain) (hcomm : ∀ (x : X) (hx : x ∈ S.generator.domain), ↑S.generator ⟨e x, ⋯⟩ = e (↑S.generator ⟨x, hx⟩)) (t : NNReal) (x : X) : (S t) (e x) = e ((S t) x)

The operators of a C₀-semigroup commute with an invertible operator that commutes with the generator.