The abstract Cauchy problem for a semigroup generator

This file introduces classical and mild solutions of the autonomous abstract Cauchy problem u' = A u, u(0) = x on the nonnegative half-line. The classical formulation uses the derivative within the whole nonnegative half-line, which is two-sided at positive times and right-sided at zero. A mild solution instead asks for continuity and the integrated identity

A (integral u on (0, t]) = u t - x.

The orbit t ↦ S(t)x of a strongly continuous semigroup is a mild solution for every initial vector. When the initial vector lies in the generator domain, domain invariance and the orbit derivative formula upgrade it to a classical solution.

The definitions and proofs follow Engel--Nagel, One-Parameter Semigroups for Linear Evolution Equations, Section II.6.

Main declarations

• IsClassicalSolution: classical solutions on [0, ∞).
• IsMildSolution: mild solutions in integrated form.
• StronglyContinuousSemigroup.isClassicalSolution_realOperator: generator-domain orbits are classical solutions.
• StronglyContinuousSemigroup.isMildSolution_realOperator: all orbits are mild solutions.

def TauCeti.Semigroups.IsClassicalSolution {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (A : X →ₗ.[ℝ] X) (x : X) (u : ℝ → X) : Prop

A classical solution of u' = A u, u(0) = x, on [0, ∞). Its values belong to the domain of A, and it has a continuous derivative within [0, ∞) equal to A (u t).

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.Semigroups.IsClassicalSolution.apply_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} {x : X} {u : ℝ → X} (hu : IsClassicalSolution A x u) : u 0 = x

A classical solution takes its prescribed initial value at time zero.

theorem TauCeti.Semigroups.isClassicalSolution_iff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} {x : X} {u : ℝ → X} : IsClassicalSolution A x u ↔ u 0 = x ∧ ∃ (u' : ℝ → X), ContinuousOn u' (Set.Ici 0) ∧ ∀ (t : ℝ), 0 ≤ t → ∃ (hut : u t ∈ A.domain), HasDerivWithinAt u (u' t) (Set.Ici 0) t ∧ u' t = ↑A ⟨u t, hut⟩

Characterization of a classical solution by its initial value and continuously differentiable equation.

theorem TauCeti.Semigroups.IsClassicalSolution.mem_domain {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} {x : X} {u : ℝ → X} (hu : IsClassicalSolution A x u) {t : ℝ} (ht : 0 ≤ t) : u t ∈ A.domain

Every value of a classical solution at nonnegative time belongs to the operator domain.

theorem TauCeti.Semigroups.IsClassicalSolution.hasDerivWithinAt {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} {x : X} {u : ℝ → X} (hu : IsClassicalSolution A x u) {t : ℝ} (ht : 0 ≤ t) : HasDerivWithinAt u (↑A ⟨u t, ⋯⟩) (Set.Ici 0) t

The derivative within the nonnegative half-line of a classical solution is the operator applied to its value.

theorem TauCeti.Semigroups.IsClassicalSolution.continuousOn {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →ₗ.[ℝ] X} {x : X} {u : ℝ → X} (hu : IsClassicalSolution A x u) : ContinuousOn u (Set.Ici 0)

A classical solution is continuous on the nonnegative half-line.

def TauCeti.Semigroups.IsMildSolution {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →ₗ.[ℝ] X) (x : X) (u : ℝ → X) : Prop

A mild solution of u' = A u, u(0) = x, on [0, ∞). The integral is pointwise Bochner integration in X. Requiring the integral to lie in the domain makes the expression A (∫ s in (0, t], u s) meaningful for an unbounded operator.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.Semigroups.IsMildSolution.continuousOn {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {x : X} {u : ℝ → X} (hu : IsMildSolution A x u) : ContinuousOn u (Set.Ici 0)

A mild solution is continuous on the nonnegative half-line.

theorem TauCeti.Semigroups.IsMildSolution.apply_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {x : X} {u : ℝ → X} (hu : IsMildSolution A x u) : u 0 = x

A mild solution takes its prescribed initial value at time zero.

theorem TauCeti.Semigroups.isMildSolution_iff {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {x : X} {u : ℝ → X} : IsMildSolution A x u ↔ ContinuousOn u (Set.Ici 0) ∧ u 0 = x ∧ ∀ (t : ℝ), 0 ≤ t → ∃ (hut : ∫ (s : ℝ) in Set.Ioc 0 t, u s ∈ A.domain), ↑A ⟨∫ (s : ℝ) in Set.Ioc 0 t, u s, hut⟩ = u t - x

Characterization of a mild solution by continuity and its integrated Cauchy equation.

theorem TauCeti.Semigroups.IsMildSolution.integral_mem_domain {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {x : X} {u : ℝ → X} (hu : IsMildSolution A x u) {t : ℝ} (ht : 0 ≤ t) : ∫ (s : ℝ) in Set.Ioc 0 t, u s ∈ A.domain

The time integral of a mild solution belongs to the operator domain.

theorem TauCeti.Semigroups.IsMildSolution.map_integral_eq_sub {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A : X →ₗ.[ℝ] X} {x : X} {u : ℝ → X} (hu : IsMildSolution A x u) {t : ℝ} (ht : 0 ≤ t) : ↑A ⟨∫ (s : ℝ) in Set.Ioc 0 t, u s, ⋯⟩ = u t - x

The integrated Cauchy equation satisfied by a mild solution.

theorem TauCeti.Semigroups.StronglyContinuousSemigroup.isClassicalSolution_realOperator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (S : StronglyContinuousSemigroup X) (x : ↥S.domain) : IsClassicalSolution S.generator ↑x fun (t : ℝ) => (S.realOperator t) ↑x

The orbit of a generator-domain vector is a classical solution of the abstract Cauchy problem for the generator.

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

Every orbit is a mild solution of the abstract Cauchy problem for the generator.