Differentiability of semigroup orbits

This file characterizes membership in the infinitesimal generator domain by right differentiability of the orbit at zero. For a vector in the generator domain, it computes the right derivative at every nonnegative time in the equivalent forms A (S t x) and S t (A x). It also proves that a generator-domain orbit has a derivative within the whole nonnegative half-line, hence a two-sided derivative at positive times.

Finally, StronglyContinuousSemigroup.slope_apply_realOperator_eq rebases an orbit inside a slope by the semigroup law, and StronglyContinuousSemigroup.hasDerivWithinAt_apply_realOperator_of_tendsto differentiates an orbit inside an operator family: the right derivative of u ↦ F u (S u x) at s is the sum of the limit of the rebased orbit difference quotient pushed through F u and the right derivative of u ↦ F u (S s x).

References

The argument follows Engel--Nagel, One-Parameter Semigroups for Linear Evolution Equations, Lemma II.1.3(ii).

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_hasDerivWithinAt_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (x : ↥S.domain) : HasDerivWithinAt (fun (s : ℝ) => (S.realOperator s) ↑x) (↑S.generator ⟨↑x, ⋯⟩) (Set.Ici 0) 0

At time zero, the right derivative of the orbit of a generator-domain vector is its generator.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_differentiableWithinAt_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (x : ↥S.domain) : DifferentiableWithinAt ℝ (fun (s : ℝ) => (S.realOperator s) ↑x) (Set.Ici 0) 0

The orbit of a generator-domain vector is right-differentiable at time zero.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_derivWithin_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (x : ↥S.domain) : derivWithin (fun (s : ℝ) => (S.realOperator s) ↑x) (Set.Ici 0) 0 = ↑S.generator ⟨↑x, ⋯⟩

The right derivative at zero of the orbit of a generator-domain vector is its generator.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_hasDerivWithinAt_zero_iff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (x y : X) : HasDerivWithinAt (fun (s : ℝ) => (S.realOperator s) x) y (Set.Ici 0) 0 ↔ ∃ (hx : x ∈ S.domain), ↑S.generator ⟨x, ⋯⟩ = y

The orbit has right derivative y at zero exactly when its initial vector belongs to the generator domain and the generator value is y.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.mem_domain_iff_differentiableWithinAt_realOperator_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (x : X) : x ∈ S.domain ↔ DifferentiableWithinAt ℝ (fun (s : ℝ) => (S.realOperator s) x) (Set.Ici 0) 0

A vector belongs to the generator domain exactly when its orbit is right-differentiable at time zero.

Right derivatives at nonnegative times

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.slope_apply_realOperator_eq {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (F : ℝ → X →L[ℝ] X) (x : X) {s u : ℝ} (hs : 0 ≤ s) (hu : s ≤ u) : slope (fun (v : ℝ) => (F v) ((S.realOperator v) x)) s u = (F u) ((u - s)⁻¹ • ((S.realOperator (u - s)) ((S.realOperator s) x) - (S.realOperator s) x)) + slope (fun (v : ℝ) => (F v) ((S.realOperator s) x)) s u

Rebasing a semigroup orbit inside a slope. For any family F of operators and nonnegative times 0 ≤ s ≤ u, the slope at s of u ↦ F u (S u x) splits, by the semigroup law S u x = S (u - s) (S s x), into the difference quotient of the orbit of S s x rebased at s and pushed through F u, plus the slope of u ↦ F u (S s x).

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.hasDerivWithinAt_apply_realOperator_of_tendsto {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (F : ℝ → X →L[ℝ] X) (x : X) {s : ℝ} (hs : 0 ≤ s) {b c : X} (hquot : Filter.Tendsto (fun (u : ℝ) => (F u) ((u - s)⁻¹ • ((S.realOperator (u - s)) ((S.realOperator s) x) - (S.realOperator s) x))) (nhdsWithin s (Set.Ioi s)) (nhds b)) (hslope : HasDerivWithinAt (fun (v : ℝ) => (F v) ((S.realOperator s) x)) c (Set.Ici s) s) : HasDerivWithinAt (fun (u : ℝ) => (F u) ((S.realOperator u) x)) (b + c) (Set.Ici s) s

Differentiating an orbit inside an operator family. At a nonnegative time s, if the difference quotient of the orbit of S s x, rebased at s and pushed through F u, converges to b, and u ↦ F u (S s x) has right derivative c at s, then u ↦ F u (S u x) has right derivative b + c at s. With F ≡ id and S s x in the generator domain this specialises to realOperator_hasDerivWithinAt; generator uniqueness takes F u = S' (t - u) for a second semigroup S'.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_hasDerivWithinAt {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {x : X} {t : ℝ} (ht : 0 ≤ t) (hxt : (S.realOperator t) x ∈ S.domain) : HasDerivWithinAt (fun (s : ℝ) => (S.realOperator s) x) (↑S.generator ⟨(S.realOperator t) x, ⋯⟩) (Set.Ici t) t

At every nonnegative time, if the evolved vector belongs to the generator domain, then the right derivative of the orbit is the generator evaluated on that evolved vector.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_hasDerivWithinAt_map_generator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (x : ↥S.domain) {t : ℝ} (ht : 0 ≤ t) : HasDerivWithinAt (fun (s : ℝ) => (S.realOperator s) ↑x) ((S.realOperator t) (↑S.generator ⟨↑x, ⋯⟩)) (Set.Ici t) t

At every nonnegative time, the right derivative of the orbit is the semigroup operator applied to the generator.

Derivatives within the nonnegative half-line

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_hasDerivWithinAt_Ici {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) [CompleteSpace X] (x : ↥S.domain) {t : ℝ} (ht : 0 ≤ t) : HasDerivWithinAt (fun (s : ℝ) => (S.realOperator s) ↑x) (↑S.generator ⟨(S.realOperator t) ↑x, ⋯⟩) (Set.Ici 0) t

On the nonnegative half-line, the orbit of a generator-domain vector has derivative equal to the generator evaluated on the evolved vector. At positive times this is a two-sided derivative; only the derivative at zero is one-sided.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_differentiableWithinAt {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (x : ↥S.domain) {t : ℝ} (ht : 0 ≤ t) : DifferentiableWithinAt ℝ (fun (s : ℝ) => (S.realOperator s) ↑x) (Set.Ici t) t

The orbit of a generator-domain vector is right-differentiable at every nonnegative time.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_derivWithin {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) {x : X} {t : ℝ} (ht : 0 ≤ t) (hxt : (S.realOperator t) x ∈ S.domain) : derivWithin (fun (s : ℝ) => (S.realOperator s) x) (Set.Ici t) t = ↑S.generator ⟨(S.realOperator t) x, ⋯⟩

The right derivative of an orbit at a nonnegative time is the generator evaluated on the evolved vector, provided that vector belongs to the generator domain.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_derivWithin_map_generator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) (x : ↥S.domain) {t : ℝ} (ht : 0 ≤ t) : derivWithin (fun (s : ℝ) => (S.realOperator s) ↑x) (Set.Ici t) t = (S.realOperator t) (↑S.generator ⟨↑x, ⋯⟩)

The right derivative of the orbit at a nonnegative time is the semigroup operator applied to the generator.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.realOperator_derivWithin_Ici {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (S : StronglyContinuousSemigroup X) [CompleteSpace X] (x : ↥S.domain) {t : ℝ} (ht : 0 ≤ t) : derivWithin (fun (s : ℝ) => (S.realOperator s) ↑x) (Set.Ici 0) t = (S.realOperator t) (↑S.generator ⟨↑x, ⋯⟩)

On the whole nonnegative half-line, the derivative of a generator-domain orbit is the orbit of its generator. In particular, the derivative at zero is a right derivative.