Smooth parameter dependence for autonomous ODEs

This file develops the Banach-space implicit-equation argument that makes a local solution of a smooth parameterized autonomous ODE depend smoothly on its parameter.

Main results

• ODE.exists_contDiffAt_picard_solution_of_contDiff: for a globally C^(n+1) field on complete spaces, with n finite or infinite, a C^(n+1) family of local solutions of the Picard integral equation, satisfying the ODE at interior times and from the right at the initial endpoint.
• ODE.exists_contDiffAt_picard_solution: the same for a germ of a C^(n+1) field with n finite, in finite dimension.

theorem ODE.exists_contDiffAt_picard_solution_of_contDiff {E F : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace E] [CompleteSpace F] {n : ℕ∞} (f : E × F → F) (p₀ : E) (x₀ : F) (hf : ContDiff ℝ (↑n + 1) f) (hzero : ∀ᶠ (y : F) in nhds x₀, f (p₀, y) = 0) : ∃ (γ : E → C(↑(Set.Icc 0 1), F)), ContDiffAt ℝ (↑n + 1) γ p₀ ∧ γ p₀ = ContinuousMap.const (↑(Set.Icc 0 1)) x₀ ∧ ∀ᶠ (p : E) in nhds p₀, (∀ (t : ↑(Set.Icc 0 1)), (γ p) t = x₀ + ∫ (s : ℝ) in 0..↑t, f (p, (γ p) (Set.projIcc 0 1 ⋯ s))) ∧ (∀ t ∈ Set.Ioo 0 1, HasDerivAt (fun (s : ℝ) => (γ p) (Set.projIcc 0 1 ⋯ s)) (f (p, (γ p) (Set.projIcc 0 1 ⋯ t))) t) ∧ ∀ t ∈ Set.Ico 0 1, HasDerivWithinAt (fun (s : ℝ) => (γ p) (Set.projIcc 0 1 ⋯ s)) (f (p, (γ p) (Set.projIcc 0 1 ⋯ t))) (Set.Ici t) t

A globally C^(n+1) parameterized autonomous vector field on complete spaces, which vanishes near the base state at the base parameter, admits a C^(n+1) family of local solutions through that state, for n finite or infinite. Each nearby path satisfies the Picard integral equation, the corresponding ODE at every interior time, and its right-hand version at the initial endpoint.

theorem ODE.exists_contDiffAt_picard_solution {E F : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] (n : ℕ) (f : E × F → F) (p₀ : E) (x₀ : F) (hf : ContDiffAt ℝ (↑n + 1) f (p₀, x₀)) (hzero : ∀ᶠ (y : F) in nhds x₀, f (p₀, y) = 0) : ∃ (γ : E → C(↑(Set.Icc 0 1), F)), ContDiffAt ℝ (↑n + 1) γ p₀ ∧ γ p₀ = ContinuousMap.const (↑(Set.Icc 0 1)) x₀ ∧ ∀ᶠ (p : E) in nhds p₀, (∀ (t : ↑(Set.Icc 0 1)), (γ p) t = x₀ + ∫ (s : ℝ) in 0..↑t, f (p, (γ p) (Set.projIcc 0 1 ⋯ s))) ∧ (∀ t ∈ Set.Ioo 0 1, HasDerivAt (fun (s : ℝ) => (γ p) (Set.projIcc 0 1 ⋯ s)) (f (p, (γ p) (Set.projIcc 0 1 ⋯ t))) t) ∧ ∀ t ∈ Set.Ico 0 1, HasDerivWithinAt (fun (s : ℝ) => (γ p) (Set.projIcc 0 1 ⋯ s)) (f (p, (γ p) (Set.projIcc 0 1 ⋯ t))) (Set.Ici t) t

A parameterized autonomous vector field which is C^(n+1) at the base point of a finite-dimensional space and vanishes near the base state at the base parameter admits a C^(n+1) family of local solutions through that state. Each nearby path satisfies the Picard integral equation, the corresponding ODE at every interior time, and its right-hand version at the initial endpoint.