Semigroups whose generators are negatives of one another are mutually inverse

Two C₀-semigroups whose generators are negatives of one another have mutually inverse operators at equal nonnegative times. No group structure is assumed: these identities are exactly the hypotheses of the gluing construction TauCeti.Semigroups.StronglyContinuousSemigroup.toGroupOfInverse, so together they produce the C₀-group generated by an operator whose positive and negative multiples both generate semigroups; Stone's theorem uses this with the contraction semigroups generated by i • A and -i • A for a self-adjoint A.

Main results

• TauCeti.Semigroups.StronglyContinuousSemigroup.comp_eq_id_of_generator_eq_neg: (S t).comp (T t) = id, and the primed version (T t).comp (S t) = id.
• TauCeti.Semigroups.StronglyContinuousSemigroup.apply_apply_eq_self_of_generator_eq_neg: S t (T t x) = x, and the primed version T t (S t x) = x. (Neither is a simp lemma: the hypothesis on the generators is not something simp can discharge on its own.)

Attribution

The argument adapts the generator-uniqueness proof of TauCeti.Analysis.Semigroups.Generator.Uniqueness.

References

Engel--Nagel, One-Parameter Semigroups for Linear Evolution Equations, Section II.3.11; Pazy, Semigroups of Linear Operators and Applications to Partial Differential Equations, Section 1.6.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.comp_eq_id_of_generator_eq_neg {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {S T : StronglyContinuousSemigroup X} (hgen : T.generator = -S.generator) (t : NNReal) : S t ∘SL T t = ContinuousLinearMap.id ℝ X

S t is a left inverse of T t: if T.generator = -S.generator then (S t).comp (T t) = id for every t : ℝ≥0. Together with comp_eq_id_of_generator_eq_neg' the two operators are mutually inverse.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.comp_eq_id_of_generator_eq_neg' {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {S T : StronglyContinuousSemigroup X} (hgen : T.generator = -S.generator) (t : NNReal) : T t ∘SL S t = ContinuousLinearMap.id ℝ X

T t is a left inverse of S t: if T.generator = -S.generator then (T t).comp (S t) = id for every t : ℝ≥0.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.apply_apply_eq_self_of_generator_eq_neg {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {S T : StronglyContinuousSemigroup X} (hgen : T.generator = -S.generator) (t : NNReal) (x : X) : (S t) ((T t) x) = x

S t undoes T t: if T.generator = -S.generator then S t (T t x) = x.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.apply_apply_eq_self_of_generator_eq_neg' {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {S T : StronglyContinuousSemigroup X} (hgen : T.generator = -S.generator) (t : NNReal) (x : X) : (T t) ((S t) x) = x

T t undoes S t: if T.generator = -S.generator then T t (S t x) = x.