Similar semigroups

Transporting a C₀-semigroup S on X along a continuous linear equivalence e : X ≃L[ℝ] Y gives the C₀-semigroup t ↦ e ∘ S t ∘ e⁻¹ on Y, whose operators are the conjugates e.conjContinuousAlgEquiv (S t). Its generator is described in TauCeti.Analysis.Semigroups.Generator.Similarity.

Main definitions and results

• TauCeti.Semigroups.StronglyContinuousSemigroup.similar: the transported semigroup.
• TauCeti.Semigroups.StronglyContinuousSemigroup.similar_apply_apply and similar_realOperator_apply: its operators act by y ↦ e (S t (e⁻¹ y)).

References

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

noncomputable def TauCeti.Semigroups.StronglyContinuousSemigroup.similar {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (S : StronglyContinuousSemigroup X) (e : X ≃L[ℝ] Y) : StronglyContinuousSemigroup Y

The C₀-semigroup t ↦ e ∘ S t ∘ e⁻¹ on Y obtained by transporting S along the continuous linear equivalence e : X ≃L[ℝ] Y.

Equations

• S.similar e = { toFun := fun (t : NNReal) => e.conjContinuousAlgEquiv (S t), map_zero' := ⋯, map_add' := ⋯, continuousAt_zero' := ⋯ }

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.similar_apply_apply {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (S : StronglyContinuousSemigroup X) (e : X ≃L[ℝ] Y) (t : NNReal) (y : Y) : ((S.similar e) t) y = e ((S t) (e.symm y))

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.similar_realOperator_apply {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (S : StronglyContinuousSemigroup X) (e : X ≃L[ℝ] Y) (t : ℝ) (y : Y) : ((S.similar e).realOperator t) y = e ((S.realOperator t) (e.symm y))

The real-time operator of the transported semigroup is the conjugate e ∘ S.realOperator t ∘ e.symm.