The identity strongly continuous semigroup

This file records the identity C₀-semigroup, equivalently the semigroup generated by the zero bounded operator. It supplies the smallest concrete example for the bounded-generator acceptance examples in the one-parameter-semigroups roadmap. Conversely, uniqueness of the semigroup generated by an operator identifies every C₀-semigroup with vanishing generator with this one (StronglyContinuousSemigroup.eq_id_of_generator_eq_zero).

References

This is the zero-generator case of the standard uniformly continuous semigroup S(t) = exp(tA).

def TauCeti.Semigroups.StronglyContinuousSemigroup.id (X : Type u_1) [NormedAddCommGroup X] [NormedSpace ℝ X] : StronglyContinuousSemigroup X

The identity C₀-semigroup S(t) = id, generated by the zero operator.

Equations

• TauCeti.Semigroups.StronglyContinuousSemigroup.id X = { toFun := fun (x : NNReal) => ContinuousLinearMap.id ℝ X, map_zero' := ⋯, map_add' := ⋯, continuousAt_zero' := ⋯ }

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.id_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (t : NNReal) : (id X) t = ContinuousLinearMap.id ℝ X

The identity C₀-semigroup is constantly the identity operator.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.id_apply_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (t : NNReal) (x : X) : ((id X) t) x = x

Pointwise form of StronglyContinuousSemigroup.id_apply.

def TauCeti.Semigroups.ContractionSemigroup.id (X : Type u_1) [NormedAddCommGroup X] [NormedSpace ℝ X] : ContractionSemigroup X

The identity contraction semigroup.

Equations

• TauCeti.Semigroups.ContractionSemigroup.id X = { toStronglyContinuousSemigroup := TauCeti.Semigroups.StronglyContinuousSemigroup.id X, contracting := ⋯ }

@[simp]

theorem TauCeti.Semigroups.ContractionSemigroup.id_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (t : NNReal) : (id X) t = ContinuousLinearMap.id ℝ X

The identity contraction semigroup is constantly the identity operator.

theorem TauCeti.Semigroups.ContractionSemigroup.id_apply_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (t : NNReal) (x : X) : ((id X) t) x = x

Pointwise form of ContractionSemigroup.id_apply.

@[simp]

theorem TauCeti.Semigroups.ContractionSemigroup.id_toStronglyContinuousSemigroup {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] : (id X).toStronglyContinuousSemigroup = StronglyContinuousSemigroup.id X

The C₀-semigroup underlying the identity contraction semigroup.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.id_hasGrowthBound {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] : (id X).HasGrowthBound 0 1

The identity semigroup has the contraction growth bound (0, 1).

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.mem_id_domain {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (x : X) : x ∈ (id X).domain

Every vector lies in the generator domain of the identity semigroup.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.id_domain_eq_top {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] : (id X).domain = ⊤

The generator domain of the identity semigroup is all of the space.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.id_generator_eq_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] : (id X).generator = 0

The generator of the identity semigroup is the zero operator.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.eq_id_of_generator_eq_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {S : StronglyContinuousSemigroup X} (h : S.generator = 0) : S = id X

A strongly continuous semigroup whose generator vanishes is the identity semigroup.