The global solution of a globally Lipschitz autonomous ODE

Picard--Lindelöf solves γ' = v ∘ γ only on a small time interval, because a solution can escape to infinity in finite time. When the vector field is globally Lipschitz no such escape happens, and through every initial point there is exactly one solution defined on all of ℝ. This file constructs it, as ODE.globalSolution.

The construction is the Picard iteration performed once and for all on the whole line, in the weighted norm that makes it a contraction there. Writing w t = cosh (2 k t) for a Lipschitz constant k > 0 of v, a curve is presented as γ t = x + w t • u t with u : ℝ →ᵇ E bounded continuous, and the Picard operator becomes

(P u) t = (w t)⁻¹ • ∫ s in 0..t, v (x + w s • u s).

Since ∫ s in 0..t, w s = sinh (2 k t) / (2 k) and |sinh| ≤ cosh, the operator P maps ℝ →ᵇ E to itself and halves distances, for either sign of t, so there is no need to glue local solutions: P has a unique fixed point on the whole line. The associated curve satisfies γ t = x + ∫ s in 0..t, v (γ s), hence solves the differential equation. Uniqueness is Mathlib's ODE_solution_unique_univ, and the fixed point depends on the initial condition 1-Lipschitzly, which gives joint continuity in time and initial condition.

Main declarations

• ODE.globalSolution: the solution of γ' = v ∘ γ with γ 0 = x on all of ℝ.
• ODE.globalSolution_eq_integral: it satisfies the integral equation of the initial value problem.
• ODE.globalSolution_zero and ODE.hasDerivAt_globalSolution: it is a solution.
• ODE.eq_globalSolution: every global solution with the same initial value is equal to it.
• ODE.globalSolution_congr: it does not depend on the chosen Lipschitz bound.
• ODE.globalSolution_add: the flow law, following the solution for two successive times.
• ODE.globalSolution_neg: reversing time solves the negated field.
• ODE.dist_globalSolution_le: two solutions drift apart at most exponentially.
• ODE.continuous_globalSolution: joint continuity in time and initial condition.

References

• J. Dieudonné, Foundations of Modern Analysis, Academic Press, 1969, Chapter X.

noncomputable def ODE.globalSolution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : E → E) {K : NNReal} (hv : LipschitzWith K v) (x : E) : ℝ → E

The global solution of a globally Lipschitz autonomous ODE. For a Lipschitz vector field v on a Banach space, ODE.globalSolution v hv x is the unique curve γ : ℝ → E defined on the whole line with γ 0 = x and γ' t = v (γ t) for every t.

Equations

• ODE.globalSolution v hv x = ODE.picardCurve✝ (↑K + 1) x (ODE.picardFixedPoint✝ ⋯ ⋯ ⋯ x)

theorem ODE.globalSolution_eq_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : E → E) {K : NNReal} (hv : LipschitzWith K v) (x : E) (t : ℝ) : globalSolution v hv x t = x + ∫ (s : ℝ) in 0..t, v (globalSolution v hv x s)

The global solution satisfies the integral equation of the initial value problem.

@[simp]

theorem ODE.globalSolution_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : E → E) {K : NNReal} (hv : LipschitzWith K v) (x : E) : globalSolution v hv x 0 = x

The global solution starts at the prescribed initial point.

theorem ODE.continuous_globalSolution_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : E → E) {K : NNReal} (hv : LipschitzWith K v) (x : E) : Continuous (globalSolution v hv x)

The global solution is continuous.

theorem ODE.hasDerivAt_globalSolution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : E → E) {K : NNReal} (hv : LipschitzWith K v) (x : E) (t : ℝ) : HasDerivAt (globalSolution v hv x) (v (globalSolution v hv x t)) t

The global solution solves the differential equation at every time.

theorem ODE.isIntegralCurve_globalSolution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : E → E) {K : NNReal} (hv : LipschitzWith K v) (x : E) : IsIntegralCurve (globalSolution v hv x) fun (x : ℝ) (y : E) => v y

The global solution is an integral curve of v, read as a time-independent vector field.

theorem ODE.eq_globalSolution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : E → E) {K : NNReal} (hv : LipschitzWith K v) {γ : ℝ → E} (hγ : ∀ (t : ℝ), HasDerivAt γ (v (γ t)) t) : γ = globalSolution v hv (γ 0)

Uniqueness. Any curve defined on the whole line that solves γ' = v ∘ γ is the global solution through its own initial value.

theorem ODE.globalSolution_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : E → E) {K K' : NNReal} (hv : LipschitzWith K v) (hv' : LipschitzWith K' v) (x : E) : globalSolution v hv x = globalSolution v hv' x

Independence of the Lipschitz bound. Two Lipschitz witnesses for the same vector field, with possibly different constants, produce the same global solution.

theorem ODE.globalSolution_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : E → E) {K : NNReal} (hv : LipschitzWith K v) (x : E) (t s : ℝ) : globalSolution v hv x (t + s) = globalSolution v hv (globalSolution v hv x t) s

The flow law. Following the global solution from x for the time t + s is the same as following it from x for the time t and then, from where it has arrived, for the time s: both curves solve the equation on the whole line and start at the same point.

theorem ODE.globalSolution_neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : E → E) {K : NNReal} (hv : LipschitzWith K v) (x : E) (t : ℝ) : globalSolution v hv x (-t) = globalSolution (fun (z : E) => -v z) ⋯ x t

Reversing time turns the global solution of v into the global solution of -v.

theorem ODE.dist_globalSolution_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : E → E) {K : NNReal} (hv : LipschitzWith K v) (x y : E) (t : ℝ) : dist (globalSolution v hv x t) (globalSolution v hv y t) ≤ dist x y * Real.exp (↑K * |t|)

Continuous dependence on the initial condition. Two global solutions drift apart at most exponentially, at the rate given by the Lipschitz constant of the vector field, in both time directions.

theorem ODE.continuous_globalSolution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (v : E → E) {K : NNReal} (hv : LipschitzWith K v) : Continuous fun (p : ℝ × E) => globalSolution v hv p.2 p.1

Joint continuity of the global solution in time and initial condition.