Linear differential equations with measurable coefficients

Let E be a Banach space and consider the linear initial value problem

x' = M(t) x + F(t), x(a) = x₀

on [a, b], where M : ℝ → E →L[ℝ] E is almost everywhere strongly measurable and essentially bounded by K on (a, b), and F : ℝ → E is integrable there. Neither M nor F need be continuous in t, so Mathlib's Picard–Lindelöf theorem does not apply; the equation is understood in Carathéodory's sense, as the integral equation

x t = x₀ + ∫ s in a..t, (M s (x s) + F s),

that is x = ODE.picard (fun s y ↦ M s y + F s) a x₀ x on [a, b], for x continuous on [a, b]. This file proves that this equation has a solution (TauCeti.exists_continuousOn_eq_forall_mem_Icc_eq_picard) and that the solution is unique (TauCeti.eqOn_of_forall_mem_Icc_eq_picard). For continuous coefficients and classical solutions on the whole line, Continuous.eq_of_hasDerivAt_clm_apply deduces uniqueness for v' = B(t) v from Mathlib's ODE_solution_unique_of_mem_Ioo.

Linear equations with merely measurable, bounded coefficients arise as the Galerkin approximations of linear parabolic equations, whose coefficients are only measurable in time.

References

• E. A. Coddington, N. Levinson, Theory of Ordinary Differential Equations, Chapter 2.
• Mathlib's Mathlib/Analysis/ODE/PicardLindelof.lean (Yury Kudryashov, Winston Yin). The existence and uniqueness proofs here follow its argument that some iterate of the Picard map is a contraction.

theorem TauCeti.integrableOn_clm_apply_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : ℝ → E →L[ℝ] E} {F : ℝ → E} {a b K : ℝ} (hM : MeasureTheory.AEStronglyMeasurable M (MeasureTheory.volume.restrict (Set.Ioo a b))) (hK : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ‖M t‖ ≤ K) (hF : MeasureTheory.IntegrableOn F (Set.Ioo a b) MeasureTheory.volume) {x : ℝ → E} (hx : ContinuousOn x (Set.Icc a b)) : MeasureTheory.IntegrableOn (fun (s : ℝ) => (M s) (x s) + F s) (Set.Ioo a b) MeasureTheory.volume

The right-hand side s ↦ M s (x s) + F s of a linear equation with essentially bounded measurable M and integrable F on (a, b) is integrable on (a, b) along every curve x continuous on [a, b].

theorem TauCeti.exists_continuousOn_eq_forall_mem_Icc_eq_picard {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : ℝ → E →L[ℝ] E} {F : ℝ → E} {a b K : ℝ} [CompleteSpace E] (hM : MeasureTheory.AEStronglyMeasurable M (MeasureTheory.volume.restrict (Set.Ioo a b))) (hK : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ‖M t‖ ≤ K) (hF : MeasureTheory.IntegrableOn F (Set.Ioo a b) MeasureTheory.volume) (x₀ : E) : ∃ (x : ℝ → E), ContinuousOn x (Set.Icc a b) ∧ x a = x₀ ∧ ∀ t ∈ Set.Icc a b, x t = ODE.picard (fun (s : ℝ) (y : E) => (M s) y + F s) a x₀ x t

Carathéodory's existence theorem for linear equations. Let M : ℝ → E →L[ℝ] E be almost everywhere strongly measurable and essentially bounded on (a, b), and let F : ℝ → E be integrable on (a, b). Then the linear equation x' = M(t) x + F(t) with x(a) = x₀ has a solution in Carathéodory's sense: a curve x continuous on [a, b] with x a = x₀ and x t = x₀ + ∫ s in a..t, (M s (x s) + F s) for every t ∈ [a, b].

theorem TauCeti.eqOn_of_forall_mem_Icc_eq_picard {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {M : ℝ → E →L[ℝ] E} {F : ℝ → E} {a b K : ℝ} {x₀ : E} (hM : MeasureTheory.AEStronglyMeasurable M (MeasureTheory.volume.restrict (Set.Ioo a b))) (hK : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ‖M t‖ ≤ K) (hF : MeasureTheory.IntegrableOn F (Set.Ioo a b) MeasureTheory.volume) {x₁ x₂ : ℝ → E} (hx₁ : ContinuousOn x₁ (Set.Icc a b)) (hx₂ : ContinuousOn x₂ (Set.Icc a b)) (h₁ : ∀ t ∈ Set.Icc a b, x₁ t = ODE.picard (fun (s : ℝ) (y : E) => (M s) y + F s) a x₀ x₁ t) (h₂ : ∀ t ∈ Set.Icc a b, x₂ t = ODE.picard (fun (s : ℝ) (y : E) => (M s) y + F s) a x₀ x₂ t) : Set.EqOn x₁ x₂ (Set.Icc a b)

Uniqueness for linear equations with measurable coefficients. Let M : ℝ → E →L[ℝ] E be almost everywhere strongly measurable and essentially bounded on (a, b), and let F : ℝ → E be integrable on (a, b). Two curves continuous on [a, b] that solve x t = x₀ + ∫ s in a..t, (M s (x s) + F s) on [a, b] agree on [a, b].

theorem Continuous.eq_of_hasDerivAt_clm_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {B : ℝ → X →L[ℝ] X} (hB : Continuous B) {v w : ℝ → X} (hv : ∀ (t : ℝ), HasDerivAt v ((B t) (v t)) t) (hw : ∀ (t : ℝ), HasDerivAt w ((B t) (w t)) t) {t₀ : ℝ} (h : v t₀ = w t₀) : v = w

Uniqueness for time-dependent linear equations. Two solutions of v' = B(t) v on the line, for a continuous family B of bounded operators, that agree at one time agree everywhere. On a bounded interval B is bounded, so the equation is uniformly Lipschitz there.