A uniform time of existence for autonomous ODEs

Picard–Lindelöf produces a solution of x' = g x through a single initial point. Extending an integral curve past a finite endpoint of its interval of definition needs more: a single time ε > 0 that works for every initial point near a given one, together with control on where the resulting solutions go. This file supplies both by shrinking Mathlib's Picard–Lindelöf solution space until all of its curves lie in a prescribed neighbourhood.

Main results

• ODE.exists_forall_mem_ball_exists_eq_forall_mem_Ioo_hasDerivAt_and_mem: for a C^1 autonomous vector field and a neighbourhood u of c, there are a radius r > 0 and a time ε > 0 such that every initial point of ball c r carries a solution on Ioo (t₀ - ε) (t₀ + ε) staying in u.

References

• Geodesics, the exponential map, and the Hopf–Rinow theorem roadmap, Layer 1, "Finite-endpoint extension criterion".

theorem ODE.exists_forall_mem_ball_exists_eq_forall_mem_Ioo_hasDerivAt_and_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {g : E → E} {c : E} [CompleteSpace E] (hg : ContDiffAt ℝ 1 g c) {u : Set E} (hu : u ∈ nhds c) (t₀ : ℝ) : ∃ r > 0, ∃ ε > 0, ∀ x ∈ Metric.ball c r, ∃ (f : ℝ → E), f t₀ = x ∧ ∀ t ∈ Set.Ioo (t₀ - ε) (t₀ + ε), HasDerivAt f (g (f t)) t ∧ f t ∈ u

Uniform time of existence. For an autonomous vector field g that is C^1 at c and a neighbourhood u of c, there are a radius r > 0 and a time ε > 0 such that every initial point in ball c r carries a solution of f' t = g (f t) on all of Ioo (t₀ - ε) (t₀ + ε), which moreover stays inside u.

Picard–Lindelöf alone gives a time of existence depending on the initial point; the content here is that it can be chosen uniformly, and that the solutions do not escape a prescribed neighbourhood.