Existence and uniqueness of solutions to ODEs

This file collects the public-facing existence and uniqueness theorems for solutions to ODEs in normed spaces.

Main results

• IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt: the Picard-Lindelöf theorem, stating the existence of a local solution to a time-dependent ODE.
• IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith: the existence of a local flow that is Lipschitz continuous in the initial point.
• IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_continuousOn: the existence of a local flow E × ℝ → E that is continuous on its domain.
• IsPicardLindelof.exists_forall_mem_closedBall_eq_forall_mem_Icc_hasDerivWithinAt: the existence of a local flow to a time-dependent vector field.
• ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt: a C¹ vector field admits solutions on open intervals for all nearby initial points.
• ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt₀: a C¹ vector field admits a local solution.
• ContDiffAt.exists_eventually_eq_hasDerivAt: a C¹ vector field admits a local flow.
• ODE_solution_unique and variants: uniqueness statements for ODE solutions on various intervals.

Tags

integral curve, vector field, existence, uniqueness, Picard-Lindelöf, Gronwall

Existence of solutions to ODEs

theorem IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) (hx : x ∈ Metric.closedBall x₀ ↑r) : ∃ (α : ℝ → E), α ↑t₀ = x ∧ ∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Set.Icc tmin tmax) t

Picard-Lindelöf (Cauchy-Lipschitz) theorem, differential form. This version shows the existence of a local solution whose initial point x may be different from the centre x₀ of the closed ball within which the properties of the vector field hold.

theorem IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt₀ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a 0 L K) : ∃ (α : ℝ → E), α ↑t₀ = x₀ ∧ ∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Set.Icc tmin tmax) t

Picard-Lindelöf (Cauchy-Lipschitz) theorem, differential form.

theorem IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) : ∃ (α : E → ℝ → E), (∀ x ∈ Metric.closedBall x₀ ↑r, α x ↑t₀ = x ∧ ∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt (α x) (f t (α x t)) (Set.Icc tmin tmax) t) ∧ ∃ (L' : NNReal), ∀ t ∈ Set.Icc tmin tmax, LipschitzOnWith L' (fun (x : E) => α x t) (Metric.closedBall x₀ ↑r)

Picard-Lindelöf (Cauchy-Lipschitz) theorem, differential form. This version shows the existence of a local flow and that it is Lipschitz continuous in the initial point.

theorem IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_continuousOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) : ∃ (α : E × ℝ → E), (∀ x ∈ Metric.closedBall x₀ ↑r, α (x, ↑t₀) = x ∧ ∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt (fun (x_1 : ℝ) => α (x, x_1)) (f t (α (x, t))) (Set.Icc tmin tmax) t) ∧ ContinuousOn α (Metric.closedBall x₀ ↑r ×ˢ Set.Icc tmin tmax)

Picard-Lindelöf (Cauchy-Lipschitz) theorem, differential form. This version shows the existence of a local flow and that it is continuous on its domain as a (partial) map E × ℝ → E.

theorem IsPicardLindelof.exists_forall_mem_closedBall_eq_forall_mem_Icc_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) : ∃ (α : E → ℝ → E), ∀ x ∈ Metric.closedBall x₀ ↑r, α x ↑t₀ = x ∧ ∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt (α x) (f t (α x t)) (Set.Icc tmin tmax) t

Picard-Lindelöf (Cauchy-Lipschitz) theorem, differential form. This version shows the existence of a local flow.

$C^1$ vector field

theorem ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : E → E} {x₀ : E} (hf : ContDiffAt ℝ 1 f x₀) (t₀ : ℝ) : ∃ r > 0, ∃ ε > 0, ∀ x ∈ Metric.closedBall x₀ r, ∃ (α : ℝ → E), α t₀ = x ∧ ∀ t ∈ Set.Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t

If a vector field f : E → E is continuously differentiable at x₀ : E, then it admits an integral curve α : ℝ → E defined on an open interval, with initial condition α t₀ = x, where x may be different from x₀.

theorem ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt₀ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : E → E} {x₀ : E} (hf : ContDiffAt ℝ 1 f x₀) (t₀ : ℝ) : ∃ (α : ℝ → E), α t₀ = x₀ ∧ ∃ ε > 0, ∀ t ∈ Set.Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t

If a vector field f : E → E is continuously differentiable at x₀ : E, then it admits an integral curve α : ℝ → E defined on an open interval, with initial condition α t₀ = x₀.

theorem ContDiffAt.exists_eventually_eq_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : E → E} {x₀ : E} (hf : ContDiffAt ℝ 1 f x₀) (t₀ : ℝ) : ∃ (α : E → ℝ → E), ∀ᶠ (xt : E × ℝ) in nhds x₀ ×ˢ nhds t₀, α xt.1 t₀ = xt.1 ∧ HasDerivAt (α xt.1) (f (α xt.1 xt.2)) xt.2

If a vector field f : E → E is continuously differentiable at x₀ : E, then it admits a flow α : E → ℝ → E defined on an open domain, with initial condition α x t₀ = x for all x within the domain.

Uniqueness of solutions to ODEs

theorem ODE_solution_unique_of_mem_Icc_right {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal} {f g : ℝ → E} {a b : ℝ} (hv : ∀ t ∈ Set.Ico a b, LipschitzOnWith K (v t) (s t)) (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt f (v t (f t)) (Set.Ici t) t) (hfs : ∀ t ∈ Set.Ico a b, f t ∈ s t) (hg : ContinuousOn g (Set.Icc a b)) (hg' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt g (v t (g t)) (Set.Ici t) t) (hgs : ∀ t ∈ Set.Ico a b, g t ∈ s t) (ha : f a = g a) : Set.EqOn f g (Set.Icc a b)

There exists only one solution of an ODE $\dot x=v(t, x)$ in a set s ⊆ ℝ × E with a given initial value provided that the RHS is Lipschitz continuous in x within s, and we consider only solutions included in s.

This version shows uniqueness in a closed interval Icc a b, where a is the initial time.

theorem ODE_solution_unique_of_mem_Icc_left {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal} {f g : ℝ → E} {a b : ℝ} (hv : ∀ t ∈ Set.Ioc a b, LipschitzOnWith K (v t) (s t)) (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ t ∈ Set.Ioc a b, HasDerivWithinAt f (v t (f t)) (Set.Iic t) t) (hfs : ∀ t ∈ Set.Ioc a b, f t ∈ s t) (hg : ContinuousOn g (Set.Icc a b)) (hg' : ∀ t ∈ Set.Ioc a b, HasDerivWithinAt g (v t (g t)) (Set.Iic t) t) (hgs : ∀ t ∈ Set.Ioc a b, g t ∈ s t) (hb : f b = g b) : Set.EqOn f g (Set.Icc a b)

A time-reversed version of ODE_solution_unique_of_mem_Icc_right. Uniqueness is shown in a closed interval Icc a b, where b is the "initial" time.

theorem ODE_solution_unique_of_mem_Icc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal} {f g : ℝ → E} {a b t₀ : ℝ} (hv : ∀ t ∈ Set.Ioo a b, LipschitzOnWith K (v t) (s t)) (ht : t₀ ∈ Set.Ioo a b) (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ t ∈ Set.Ioo a b, HasDerivAt f (v t (f t)) t) (hfs : ∀ t ∈ Set.Ioo a b, f t ∈ s t) (hg : ContinuousOn g (Set.Icc a b)) (hg' : ∀ t ∈ Set.Ioo a b, HasDerivAt g (v t (g t)) t) (hgs : ∀ t ∈ Set.Ioo a b, g t ∈ s t) (heq : f t₀ = g t₀) : Set.EqOn f g (Set.Icc a b)

A version of ODE_solution_unique_of_mem_Icc_right for uniqueness in a closed interval whose interior contains the initial time.

theorem ODE_solution_unique_of_mem_Ioo {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal} {f g : ℝ → E} {a b t₀ : ℝ} (hv : ∀ t ∈ Set.Ioo a b, LipschitzOnWith K (v t) (s t)) (ht : t₀ ∈ Set.Ioo a b) (hf : ∀ t ∈ Set.Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t) (hg : ∀ t ∈ Set.Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t) (heq : f t₀ = g t₀) : Set.EqOn f g (Set.Ioo a b)

A version of ODE_solution_unique_of_mem_Icc for uniqueness in an open interval.

theorem ODE_solution_unique_of_eventually {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal} {f g : ℝ → E} {t₀ : ℝ} (hv : ∀ᶠ (t : ℝ) in nhds t₀, LipschitzOnWith K (v t) (s t)) (hf : ∀ᶠ (t : ℝ) in nhds t₀, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t) (hg : ∀ᶠ (t : ℝ) in nhds t₀, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t) (heq : f t₀ = g t₀) : f =ᶠ[nhds t₀] g

Local uniqueness of ODE solutions.

theorem ODE_solution_unique {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {K : NNReal} {f g : ℝ → E} {a b : ℝ} (hv : ∀ (t : ℝ), LipschitzWith K (v t)) (hf : ContinuousOn f (Set.Icc a b)) (hf' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt f (v t (f t)) (Set.Ici t) t) (hg : ContinuousOn g (Set.Icc a b)) (hg' : ∀ t ∈ Set.Ico a b, HasDerivWithinAt g (v t (g t)) (Set.Ici t) t) (ha : f a = g a) : Set.EqOn f g (Set.Icc a b)

There exists only one solution of an ODE $\dot x=v(t, x)$ with a given initial value provided that the RHS is Lipschitz continuous in x.

theorem ODE_solution_unique_univ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal} {f g : ℝ → E} {t₀ : ℝ} (hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)) (hf : ∀ (t : ℝ), HasDerivAt f (v t (f t)) t ∧ f t ∈ s t) (hg : ∀ (t : ℝ), HasDerivAt g (v t (g t)) t ∧ g t ∈ s t) (heq : f t₀ = g t₀) : f = g

There exists only one global solution to an ODE $\dot x=v(t, x)$ with a given initial value provided that the RHS is Lipschitz continuous.