Smooth dependence of an ODE solution on its initial condition

Picard iteration produces a solution of γ' = v ∘ γ continuously, indeed Lipschitzly, in the initial condition. It says nothing about differentiability: the contraction argument is metric. This file upgrades continuity to smoothness of the same order as the field, jointly in the initial condition and in time. The local argument first gives this near time 0. The flow law then propagates the result to every time, at every finite order: for a fixed initial condition, the set of times where the solution is smooth is both open and closed.

The mechanism is a change of variables that turns the initial condition into a parameter of a new equation, so that ODE.exists_contDiffAt_picard_solution_of_contDiff applies. Writing a solution through x as t ↦ x + u (t / ε), the curve u solves

u' s = ε • v (x + u s), u 0 = 0

on the fixed time interval [0, 1], with (x, ε) a parameter and the initial state 0 fixed. At ε = 0 that field vanishes identically, which is exactly the degeneracy hypothesis of the parameterized Picard theorem, and the solution at the base parameter is the constant curve 0. Evaluating the resulting smooth family of paths at the endpoint s = 1 — a continuous linear map on the path space — produces x + u 1, which ODE_solution_unique identifies with the value of the global solution at time ε. Both the initial condition and the time are therefore smooth directions.

Main results

• ODE.contDiffAt_globalSolution: the global solution of a globally Lipschitz C^(n+1) field is C^(n+1) in time and initial condition near time 0, for n finite or infinite.
• ODE.contDiff_globalSolution: the global solution is C^(n+1) jointly in its initial condition and time, for every finite n.
• ODE.contDiff_globalSolution_apply: every time-t map is C^(n+1).
• ODE.exists_contDiffAt_localFlow: a vector field which is C^(n+1) on a neighbourhood of a point has a local flow through the nearby points which is C^(n+1) in time and initial condition near that point at time 0, and which obeys the flow law Φ x (t + u) = Φ (Φ x t) u.

The local flow produced here is the model-space input to the smooth flow of a vector field on a manifold, and in particular to the flow of the geodesic spray, whose base curves are the geodesics of a Riemannian metric.

References

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

theorem ODE.contDiffAt_globalSolution {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {n : ℕ∞} (v : E → E) {K : NNReal} (hv : LipschitzWith K v) (hvs : ContDiff ℝ (↑n + 1) v) (a : E) : ContDiffAt ℝ (↑n + 1) (fun (p : E × ℝ) => globalSolution v hv p.1 p.2) (a, 0)

The global solution of a globally Lipschitz field depends smoothly on time and on its initial condition, near time 0, at the order of the field.

theorem ODE.contDiff_globalSolution {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (n : ℕ) (v : E → E) {K : NNReal} (hv : LipschitzWith K v) (hvs : ContDiff ℝ (↑n + 1) v) : ContDiff ℝ (↑n + 1) fun (p : E × ℝ) => globalSolution v hv p.1 p.2

The global solution of a globally Lipschitz C^(n+1) field is C^(n+1) jointly in its initial condition and time.

For every finite positive regularity order, the global solution has the same joint regularity as the vector field.

theorem ODE.contDiff_globalSolution_apply {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (n : ℕ) (v : E → E) {K : NNReal} (hv : LipschitzWith K v) (hvs : ContDiff ℝ (↑n + 1) v) (t : ℝ) : ContDiff ℝ (↑n + 1) fun (x : E) => globalSolution v hv x t

At every fixed time, the global solution of a globally Lipschitz C^(n+1) field is a C^(n+1) function of its initial condition.

theorem ODE.exists_contDiffAt_localFlow {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ∞} (v : E → E) {a : E} {s : Set E} (hv : ContDiffOn ℝ (↑n + 1) v s) (hs : s ∈ nhds a) : ∃ (Φ : E → ℝ → E), ContDiffAt ℝ (↑n + 1) (fun (p : E × ℝ) => Φ p.1 p.2) (a, 0) ∧ (∀ (x : E), Φ x 0 = x) ∧ (∀ (x : E) (t u : ℝ), Φ x (t + u) = Φ (Φ x t) u) ∧ ∀ᶠ (p : E × ℝ) in nhds (a, 0), HasDerivAt (Φ p.1) (v (Φ p.1 p.2)) p.2

The local flow of a smooth vector field. A field which is C^(n+1) on a neighbourhood of a admits a flow Φ: a family of curves, one through each point, which start at that point, obey the flow law Φ x (t + u) = Φ (Φ x t) u, depend on the initial condition and the time in a C^(n+1) way near (a, 0), and solve the equation for every initial condition and time in some neighbourhood of (a, 0). No global hypothesis on the field is needed: a bump function cuts the field down to a globally Lipschitz one agreeing with it near a, and the two fields still agree along the curves at the times where the equation is claimed. The flow law holds for all times because Φ is the global flow of that cut-off field; only the equation for v is local.