Generators of exponentially shifted semigroups

The exponentially shifted semigroup t ↦ exp (-omega t) S(t) has the same generator domain as S, and its generator is A - omega I. This identifies the shift used to move semigroup growth bounds with the scalar shift used in unbounded-resolvent hypotheses.

Main result

• TauCeti.Semigroups.StronglyContinuousSemigroup.generator_expShift: the generator of exp (-omega t) S(t) is A - omega I.

References

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

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.generator_expShift {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (omega : ℝ) : (S.expShift omega).generator = LinearPMap.subScalar S.generator omega

The generator of the exponentially shifted semigroup exp (-omega t) S(t) is A - omega I, where A is the generator of S.