Strongly continuous semigroups

This file contains the foundational C₀-semigroup structures, the nonnegative-time API (map_zero, map_add, continuousAt_zero, and their pointwise/tendsto forms), the realOperator real-time shim, operator-norm local boundedness, and strong continuity within the nonnegative half-line.

References

Ported and adapted (Apache 2.0) from mrdouglasny/hille-yosida; references include Engel--Nagel, Linares, Pazy, Hille, and Yosida.

Strongly Continuous Semigroups

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

A strongly continuous one-parameter semigroup (C₀-semigroup) on a normed space X.

The semigroup is indexed by nonnegative real time. The axioms are S 0 = Id, S (s + t) = S s ∘ S t, and strong continuity at 0. Note that the C₀-semigroup theory proper (uniform boundedness, continuity of orbits at positive times) additionally needs X complete.

• toFun : NNReal → X →L[ℝ] X

  The semigroup operator at time t : ℝ≥0.

• map_zero' : self.toFun 0 = ContinuousLinearMap.id ℝ X

  S 0 = Id.

• map_add' (s t : NNReal) : self.toFun (s + t) = self.toFun s ∘SL self.toFun t

  S (s + t) = S s ∘ S t.

• continuousAt_zero' (x : X) : ContinuousAt (fun (t : NNReal) => (self.toFun t) x) 0

  Strong continuity at 0.

@[instance_reducible]

instance TauCeti.Semigroups.StronglyContinuousSemigroup.instFunLike {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] : FunLike (StronglyContinuousSemigroup X) NNReal (X →L[ℝ] X)

Equations

• TauCeti.Semigroups.StronglyContinuousSemigroup.instFunLike = { coe := TauCeti.Semigroups.StronglyContinuousSemigroup.toFun, coe_injective := ⋯ }

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ext {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {S T : StronglyContinuousSemigroup X} (h : ∀ (t : NNReal), S t = T t) : S = T

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.ext_iff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {S T : StronglyContinuousSemigroup X} : S = T ↔ ∀ (t : NNReal), S t = T t

@[simp]

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

The native nonnegative-time operator at zero is the identity.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.map_zero_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (x : X) : (S 0) x = x

Pointwise form of StronglyContinuousSemigroup.map_zero.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.map_add {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (s t : NNReal) : S (s + t) = S s ∘SL S t

The native nonnegative-time semigroup law.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.map_nsmul {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (t : NNReal) (k : ℕ) : S (k • t) = S t ^ k

The operator at a natural multiple of a time is a power. S (k • t) = (S t) ^ k.

Not a simp lemma: nsmul_eq_mul rewrites the left-hand side to S (↑k * t), so tagging this would put it out of simp normal form (simpNF).

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.map_natCast_mul {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (t : NNReal) (k : ℕ) : S (↑k * t) = S t ^ k

The power identity in simp normal form. S (↑k * t) = (S t) ^ k.

This is map_nsmul with the left-hand side normalised: nsmul_eq_mul rewrites k • t to ↑k * t, so this spelling is the one simp can reach.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.norm_map_nsmul_le_pow {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (t : NNReal) {M : ℝ} (hMt : ‖S t‖ ≤ M) (k : ℕ) : ‖S (k • t)‖ ≤ M ^ k

The multi-step operator-norm bound. If ‖S t‖ ≤ M, then ‖S (k • t)‖ ≤ M ^ k at every natural multiple of t.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.map_add_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (s t : NNReal) (x : X) : (S (s + t)) x = (S s) ((S t) x)

Pointwise form of StronglyContinuousSemigroup.map_add.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.sub_eq_comp_sub_one_of_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {a b : NNReal} (hab : a ≤ b) : S b - S a = S a ∘SL (S (b - a) - 1)

The increment of a semigroup over [a, b] factors through its value at a.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.norm_map_add_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (s t : NNReal) : ‖S (s + t)‖ ≤ ‖S s‖ * ‖S t‖

Submultiplicativity of the native nonnegative-time operator norm.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.continuousAt_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (x : X) : ContinuousAt (fun (t : NNReal) => (S t) x) 0

Strong continuity at zero for the native nonnegative-time action.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.continuousAt_zero_tendsto {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (x : X) : Filter.Tendsto (fun (t : NNReal) => (S t) x) (nhds 0) (nhds x)

Tendsto form of StronglyContinuousSemigroup.continuousAt_zero.

noncomputable def TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (t : ℝ) : X →L[ℝ] X

The semigroup as a function of real time, extended by id for t < 0.

Equations

• S.realOperator t = S t.toNNReal

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_def {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (t : ℝ) : S.realOperator t = S t.toNNReal

The real-time operator is the native semigroup operator at the nonnegative part of t.

This is not a simp lemma: the simp normal form keeps realOperator folded, so that the more specific lemmas realOperator_coe, realOperator_zero and realOperator_derivWithin_zero fire.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_coe {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (t : NNReal) : S.realOperator ↑t = S t

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) : S.realOperator 0 = ContinuousLinearMap.id ℝ X

The real-time operator at zero is the identity: S.realOperator 0 = id.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_add {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (s t : ℝ) (hs : 0 ≤ s) (ht : 0 ≤ t) : S.realOperator (s + t) = S.realOperator s ∘SL S.realOperator t

The real-time shim satisfies the semigroup law at nonnegative real times.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_add_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (s t : ℝ) (hs : 0 ≤ s) (ht : 0 ≤ t) (x : X) : (S.realOperator (s + t)) x = (S.realOperator s) ((S.realOperator t) x)

The semigroup law at nonnegative real times, applied to a vector.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.norm_realOperator_add_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (s t : ℝ) (hs : 0 ≤ s) (ht : 0 ≤ t) : ‖S.realOperator (s + t)‖ ≤ ‖S.realOperator s‖ * ‖S.realOperator t‖

Submultiplicativity of the real-time operator norm at nonnegative times: the semigroup law S.realOperator (s + t) = S.realOperator s ∘ S.realOperator t bounds the norm of the composite by the product of the norms.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_continuousWithinAt_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (x : X) : ContinuousWithinAt (fun (t : ℝ) => (S.realOperator t) x) (Set.Ici 0) 0

Strong continuity at zero of t ↦ S.realOperator t x along 0 ≤ t.

structure TauCeti.Semigroups.ContractionSemigroup (X : Type u_1) [NormedAddCommGroup X] [NormedSpace ℝ X] extends TauCeti.Semigroups.StronglyContinuousSemigroup X : Type u_1

A contraction semigroup: ‖S(t)‖ ≤ 1 for all t ≥ 0 ([EN] Def. I.5.6, [Linares] Def. 3). Has the growth estimate M = 1, ω = 0.

• toFun : NNReal → X →L[ℝ] X
• map_zero' : self.toFun 0 = ContinuousLinearMap.id ℝ X
• map_add' (s t : NNReal) : self.toFun (s + t) = self.toFun s ∘SL self.toFun t
• continuousAt_zero' (x : X) : ContinuousAt (fun (t : NNReal) => (self.toFun t) x) 0
• contracting (t : NNReal) : ‖self.toFun t‖ ≤ 1

  ‖S(t)‖ ≤ 1 for all t : ℝ≥0.

@[instance_reducible]

instance TauCeti.Semigroups.ContractionSemigroup.instFunLike {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] : FunLike (ContractionSemigroup X) NNReal (X →L[ℝ] X)

Equations

• TauCeti.Semigroups.ContractionSemigroup.instFunLike = { coe := fun (S : TauCeti.Semigroups.ContractionSemigroup X) => ⇑S.toStronglyContinuousSemigroup, coe_injective := ⋯ }

theorem TauCeti.Semigroups.ContractionSemigroup.ext {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {S T : ContractionSemigroup X} (h : ∀ (t : NNReal), S t = T t) : S = T

theorem TauCeti.Semigroups.ContractionSemigroup.ext_iff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {S T : ContractionSemigroup X} : S = T ↔ ∀ (t : NNReal), S t = T t

@[simp]

theorem TauCeti.Semigroups.ContractionSemigroup.toStronglyContinuousSemigroup_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : ContractionSemigroup X) (t : NNReal) : S.toStronglyContinuousSemigroup t = S t

Basic Properties

theorem TauCeti.Semigroups.ContractionSemigroup.contracting_real {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : ContractionSemigroup X) (t : ℝ) (ht : 0 ≤ t) : ‖S.realOperator t‖ ≤ 1

A contraction semigroup is contractive at nonnegative real times.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_zero_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (x : X) : (S.realOperator 0) x = x

S(t) x at t = 0 equals x, pointwise version.

Results requiring completeness

When X is complete, pointwise boundedness on [0, 1] implies uniform operator-norm boundedness on [0, 1] via the Banach--Steinhaus theorem. From this, uniform boundedness on compact intervals and left-continuity (and thus full continuity) of orbits follow.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.normBoundedOnUnitInterval {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) : ∃ (M : ℝ), 1 ≤ M ∧ ∀ (t : ℝ), 0 ≤ t → t ≤ 1 → ‖S.realOperator t‖ ≤ M

The operator norm of a C₀-semigroup is bounded on [0, 1].

One direction of [EN] Prop. I.5.3: strong continuity implies uniform boundedness on compact intervals. This rests on the Banach--Steinhaus theorem and therefore requires X to be complete.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_continuousWithinAt {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) (x : X) (t₀ : ℝ) (ht₀ : 0 ≤ t₀) : ContinuousWithinAt (fun (t : ℝ) => (S.realOperator t) x) (Set.Ici 0) t₀

Strong continuity at every t₀ ≥ 0, not just at 0 ([EN] Prop. I.5.3, [Linares] Cor. 1).

Strong continuity holds at every t₀ ≥ 0, not only at 0.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_continuousOn_Ici {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) (x : X) : ContinuousOn (fun (t : ℝ) => (S.realOperator t) x) (Set.Ici 0)

The real-time orbit of a strongly continuous semigroup is continuous on the nonnegative half-line.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.continuous_realOperator_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) (x : X) : Continuous fun (t : ℝ) => (S.realOperator t) x

The real-time orbit is continuous on all of ℝ, using the constant extension at negative times.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_continuousAt_of_pos {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) (x : X) {t : ℝ} (ht : 0 < t) : ContinuousAt (fun (u : ℝ) => (S.realOperator u) x) t

The real-time orbit of a strongly continuous semigroup is continuous at positive times.