Uniqueness for the abstract Cauchy problem

For the generator of a strongly continuous semigroup, every classical or mild solution agrees with its semigroup orbit on the nonnegative half-line. The interpolation s ↦ S(t - s)u(s) has zero derivative because the two generator contributions cancel. Only strong continuity of the semigroup is used; no operator-norm differentiability is assumed.

For mild solutions, the time integral of the difference of two solutions is a classical solution with zero initial value. Classical uniqueness makes this primitive zero, and the fundamental theorem of calculus then makes the solutions equal. Equality is asserted only on [0, ∞), since neither solution predicate constrains negative times.

References

• K.-J. Engel and R. Nagel, One-Parameter Semigroups for Linear Evolution Equations, Section II.6.

theorem TauCeti.Semigroups.IsClassicalSolution.eq_realOperator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {S : StronglyContinuousSemigroup X} {x : X} {u : ℝ → X} (hu : IsClassicalSolution S.generator x u) {t : ℝ} (ht : 0 ≤ t) : u t = (S.realOperator t) x

Every classical solution for a semigroup generator is its orbit, at every nonnegative time.

theorem TauCeti.Semigroups.IsClassicalSolution.unique {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {S : StronglyContinuousSemigroup X} {x : X} {u v : ℝ → X} (hu : IsClassicalSolution S.generator x u) (hv : IsClassicalSolution S.generator x v) : Set.EqOn u v (Set.Ici 0)

Classical solutions for a semigroup generator with the same initial value agree on [0, ∞).

theorem TauCeti.Semigroups.IsMildSolution.unique {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {S : StronglyContinuousSemigroup X} {x : X} {u v : ℝ → X} (hu : IsMildSolution S.generator x u) (hv : IsMildSolution S.generator x v) : Set.EqOn u v (Set.Ici 0)

Mild solutions for a semigroup generator with the same initial value agree on [0, ∞).

theorem TauCeti.Semigroups.IsMildSolution.eq_realOperator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {S : StronglyContinuousSemigroup X} {x : X} {u : ℝ → X} (hu : IsMildSolution S.generator x u) {t : ℝ} (ht : 0 ≤ t) : u t = (S.realOperator t) x

Every mild solution for a semigroup generator is its orbit, at every nonnegative time.