Smooth dependence of a flow on its initial point

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #60, the C^k half of Darboux's theorem.

FlowDerivative.lean proves that the flow of a C¹ time-dependent field is differentiable in the initial point, with derivative the solution Y of the variational equation Y' = D(f t)(α x t) ∘ Y. This file proves C^k dependence for a C^k field, by induction on k through the pair flow: (x, Z) ↦ (α x t, Y x t ∘ Z) is the flow of the field G t (z, Z) = (f t z, D(f t)(z) ∘ Z) on E × (E →L E), which is C^{k−1} when f is C^k; the induction hypothesis applied to it makes x ↦ Y x t = D(α · t)(x) of class C^{k−1}, so α · t is C^k. The linear ODE solutions it needs on the whole time interval are exists_linearODE_solution_Icc.

• hasFDerivAt_of_contDiffOn_uncurry — the partial derivative of a jointly C¹ field, D(f t)(z) = D(↿f)(t, z) ∘ inr;
• exists_isOpen_hasFDerivAt_of_contDiffOn_uncurry — an open neighbourhood of a compact on which a jointly C¹ field has the differentiability and joint continuity of D(f t) that hasFDerivAt_flow_of_variational_timeDependent asks for (the tube lemma);
• ★ exists_variational_of_lipschitz — C¹ dependence in Lipschitz form: a flow of a jointly C¹ field on an open set of initial points, confined to a compact and Lipschitz in the initial point, is differentiable in the initial point with derivative the variational solution, and that derivative is continuous in the initial point;
• ★★ contDiffOn_flow_of_contDiffOn — C^n dependence: if the field is jointly C^n on an open set (n ≤ ∞) and the flow is confined to a compact convex set and Lipschitz in the initial point, the time-t map is C^n on the open set of initial points.

Mathlib at the pin has Picard–Lindelöf (existence, uniqueness, Lipschitz dependence) and no differentiable or smooth dependence on the initial point. References: P. Hartman, Ordinary Differential Equations, Ch. V (Thm 3.1, 4.1); S. Lang, Real and Functional Analysis, XIV §3; Analysis/ODE/FlowDerivative.lean; Geometry/Manifold/Darboux.lean; specs/BACKLOG.md #60.

theorem hasFDerivAt_of_contDiffOn_uncurry {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {V : Set (ℝ × E)} (hV : IsOpen V) {n : WithTop ℕ∞} (hn : 1 ≤ n) (hf : ContDiffOn ℝ n (Function.uncurry f) V) {t : ℝ} {z : E} (hp : (t, z) ∈ V) : HasFDerivAt (f t) (fderiv ℝ (Function.uncurry f) (t, z) ∘SL ContinuousLinearMap.inr ℝ ℝ E) z

The partial derivative of a jointly C¹ field: D(f t)(z) = D(↿f)(t, z) ∘ inr.

theorem exists_isOpen_hasFDerivAt_of_contDiffOn_uncurry {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {V : Set (ℝ × E)} (hV : IsOpen V) {n : WithTop ℕ∞} (hn : 1 ≤ n) (hf : ContDiffOn ℝ n (Function.uncurry f) V) {T : ℝ} {K : Set E} (hK : IsCompact K) (hKV : Set.Icc 0 T ×ˢ K ⊆ V) : ∃ (U : Set E), IsOpen U ∧ K ⊆ U ∧ Set.Icc 0 T ×ˢ U ⊆ V ∧ (∀ t ∈ Set.Icc 0 T, ∀ z ∈ U, HasFDerivAt (f t) (fderiv ℝ (f t) z) z) ∧ ContinuousOn (fun (p : ℝ × E) => fderiv ℝ (f p.1) p.2) (Set.Icc 0 T ×ˢ U)

On an open neighbourhood U of a compact K with [0, T] × K inside the open set where the field is jointly C¹, the field is differentiable in z with (t, z) ↦ D(f t)(z) continuous — the hypotheses of hasFDerivAt_flow_of_variational_timeDependent.

theorem exists_variational_of_lipschitz {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : ℝ → E → E} {U : Set E} (hU : IsOpen U) {T : ℝ} (hT : 0 < T) (hfd : ∀ t ∈ Set.Icc 0 T, ∀ z ∈ U, HasFDerivAt (f t) (fderiv ℝ (f t) z) z) (hDc : ContinuousOn (fun (p : ℝ × E) => fderiv ℝ (f p.1) p.2) (Set.Icc 0 T ×ˢ U)) {K : Set E} (hK : IsCompact K) (hKU : K ⊆ U) {α : E → ℝ → E} {S : Set E} (hS : IsOpen S) (hα0 : ∀ x ∈ S, α x 0 = x) (hαd : ∀ x ∈ S, ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt (α x) (f t (α x t)) (Set.Icc 0 T) t) (hαK : ∀ x ∈ S, ∀ t ∈ Set.Icc 0 T, α x t ∈ K) {L' : NNReal} (hlip : ∀ t ∈ Set.Icc 0 T, LipschitzOnWith L' (fun (x : E) => α x t) S) {M : ℝ} (hM0 : 0 ≤ M) (hM : ∀ t ∈ Set.Icc 0 T, ∀ z ∈ K, ‖fderiv ℝ (f t) z‖ ≤ M) : ∃ (Y : E → ℝ → E →L[ℝ] E), (∀ x ∈ S, Y x 0 = 1 ∧ (∀ t ∈ Set.Icc 0 T, HasDerivWithinAt (Y x) (fderiv ℝ (f t) (α x t) ∘SL Y x t) (Set.Icc 0 T) t) ∧ ∀ t ∈ Set.Icc 0 T, HasFDerivAt (fun (x : E) => α x t) (Y x t) x) ∧ ∀ t ∈ Set.Icc 0 T, ContinuousOn (fun (x : E) => Y x t) S

★ C¹ dependence of a flow on the initial point, in Lipschitz form. Let f t be differentiable on an open U for t ∈ [0, T] with (t, z) ↦ D(f t)(z) continuous and bounded by M on a compact K ⊆ U, and let α be a flow of f on an open set S of initial points, confined to K and Lipschitz in the initial point uniformly in time. Then there is Y with Y x 0 = 1, solving the variational equation along the curve of x, such that α · t is differentiable at every x ∈ S with derivative Y x t, and x ↦ Y x t is continuous on S. (The variational solution exists on all of [0, T] by exists_linearODE_solution_Icc; the continuity is dist_le_of_linearODE_coeff_close with the uniform continuity of D(f t) on [0, T] × K and the Lipschitz separation of trajectories.)

theorem contDiffOn_flow_aux (k : ℕ) (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (f : ℝ → E → E) (V : Set (ℝ × E)) : IsOpen V → ∀ (T : ℝ), 0 < T → ContDiffOn ℝ (↑(k + 1)) (Function.uncurry f) V → ∀ (α : E → ℝ → E) (S : Set E), IsOpen S → ∀ (K : Set E), IsCompact K → Convex ℝ K → Set.Icc 0 T ×ˢ K ⊆ V → (∀ x ∈ S, α x 0 = x) → (∀ x ∈ S, ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt (α x) (f t (α x t)) (Set.Icc 0 T) t) → (∀ x ∈ S, ∀ t ∈ Set.Icc 0 T, α x t ∈ K) → ∀ (L' : NNReal), (∀ t ∈ Set.Icc 0 T, LipschitzOnWith L' (fun (x : E) => α x t) S) → ∀ t ∈ Set.Icc 0 T, ContDiffOn ℝ (↑(k + 1)) (fun (x : E) => α x t) S

The induction behind contDiffOn_flow_of_contDiffOn, on the order k + 1, generalised over the space: the step passes from (E, f, α) to the pair flow (x, Z) ↦ (α x t, Y x t ∘ Z) of the field (z, Z) ↦ (f t z, D(f t)(z) ∘ Z) on E × (E →L E), which is one order less smooth.

theorem contDiffOn_flow_of_contDiffOn {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : ℝ → E → E} {V : Set (ℝ × E)} (hV : IsOpen V) {T : ℝ} (hT : 0 < T) {n : ℕ∞} (hn : 1 ≤ n) (hf : ContDiffOn ℝ (↑n) (Function.uncurry f) V) {α : E → ℝ → E} {S : Set E} (hS : IsOpen S) {K : Set E} (hK : IsCompact K) (hKc : Convex ℝ K) (hKV : Set.Icc 0 T ×ˢ K ⊆ V) (hα0 : ∀ x ∈ S, α x 0 = x) (hαd : ∀ x ∈ S, ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt (α x) (f t (α x t)) (Set.Icc 0 T) t) (hαK : ∀ x ∈ S, ∀ t ∈ Set.Icc 0 T, α x t ∈ K) {L' : NNReal} (hlip : ∀ t ∈ Set.Icc 0 T, LipschitzOnWith L' (fun (x : E) => α x t) S) (t : ℝ) : t ∈ Set.Icc 0 T → ContDiffOn ℝ (↑n) (fun (x : E) => α x t) S

★★ C^n dependence of a flow on its initial point. Let f be a time-dependent field, jointly C^n (1 ≤ n ≤ ∞) on an open V ⊆ ℝ × E, and α a flow of f on an open set S of initial points for times in [0, T], confined to a compact convex K with [0, T] × K ⊆ V and Lipschitz in the initial point uniformly in time. Then the time-t map α · t is C^n on S.