mathlib3 documentation

analysis.ODE.picard_lindelof

Picard-Lindelöf (Cauchy-Lipschitz) Theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove that an ordinary differential equation $\dot x=v(t, x)$ such that $v$ is Lipschitz continuous in $x$ and continuous in $t$ has a local solution, see exists_forall_deriv_within_Icc_eq_of_is_picard_lindelof.

As a corollary, we prove that a time-independent locally continuously differentiable ODE has a local solution.

Implementation notes #

In order to split the proof into small lemmas, we introduce a structure picard_lindelof that holds all assumptions of the main theorem. This structure and lemmas in the picard_lindelof namespace should be treated as private implementation details. This is not to be confused with the Prop- valued structure is_picard_lindelof, which holds the long hypotheses of the Picard-Lindelöf theorem for actual use as part of the public API.

We only prove existence of a solution in this file. For uniqueness see ODE_solution_unique and related theorems in analysis.ODE.gronwall.

Tags #

differential equation

structure is_picard_lindelof {E : Type u_2} [normed_add_comm_group E] (v : E E) (t_min t₀ t_max : ) (x₀ : E) (L : nnreal) (R C : ) :
Prop

Prop structure holding the hypotheses of the Picard-Lindelöf theorem.

The similarly named picard_lindelof structure is part of the internal API for convenience, so as not to constantly invoke choice, but is not intended for public use.

structure picard_lindelof (E : Type u_2) [normed_add_comm_group E] [normed_space E] :
Type u_2

This structure holds arguments of the Picard-Lipschitz (Cauchy-Lipschitz) theorem. It is part of the internal API for convenience, so as not to constantly invoke choice. Unless you want to use one of the auxiliary lemmas, use exists_forall_deriv_within_Icc_eq_of_lipschitz_of_continuous instead of using this structure.

The similarly named is_picard_lindelof is a bundled Prop holding the long hypotheses of the Picard-Lindelöf theorem as named arguments. It is used as part of the public API.

Instances for picard_lindelof
@[protected, instance]
Equations
theorem picard_lindelof.norm_le {E : Type u_1} [normed_add_comm_group E] [normed_space E] (v : picard_lindelof E) {t : } (ht : t set.Icc v.t_min v.t_max) {x : E} (hx : x metric.closed_ball v.x₀ (v.R)) :
v t x (v.C)
noncomputable def picard_lindelof.t_dist {E : Type u_1} [normed_add_comm_group E] [normed_space E] (v : picard_lindelof E) :

The maximum of distances from t₀ to the endpoints of [t_min, t_max].

Equations

Projection $ℝ → [t_{\min}, t_{\max}]$ sending $(-∞, t_{\min}]$ to $t_{\min}$ and $[t_{\max}, ∞)$ to $t_{\max}$.

Equations

The space of curves $γ \colon [t_{\min}, t_{\max}] \to E$ such that $γ(t₀) = x₀$ and $γ$ is Lipschitz continuous with constant $C$. The map sending $γ$ to $\mathbf Pγ(t)=x₀ + ∫_{t₀}^{t} v(τ, γ(τ))\,dτ$ is a contracting map on this space, and its fixed point is a solution of the ODE $\dot x=v(t, x)$.

Instances for picard_lindelof.fun_space
noncomputable def picard_lindelof.fun_space.v_comp {E : Type u_1} [normed_add_comm_group E] [normed_space E] {v : picard_lindelof E} (f : v.fun_space) (t : ) :
E

Given a curve $γ \colon [t_{\min}, t_{\max}] → E$, v_comp is the function $F(t)=v(π t, γ(π t))$, where π is the projection $ℝ → [t_{\min}, t_{\max}]$. The integral of this function is the image of γ under the contracting map we are going to define below.

Equations
theorem picard_lindelof.fun_space.dist_le_of_forall {E : Type u_1} [normed_add_comm_group E] [normed_space E] {v : picard_lindelof E} {f₁ f₂ : v.fun_space} {d : } (h : (t : (set.Icc v.t_min v.t_max)), has_dist.dist (f₁ t) (f₂ t) d) :
has_dist.dist f₁ f₂ d

The Picard-Lindelöf operator. This is a contracting map on picard_lindelof.fun_space v such that the fixed point of this map is the solution of the corresponding ODE.

More precisely, some iteration of this map is a contracting map.

Equations
theorem picard_lindelof.fun_space.dist_next_apply_le_of_le {E : Type u_1} [normed_add_comm_group E] [normed_space E] {v : picard_lindelof E} [complete_space E] {f₁ f₂ : v.fun_space} {n : } {d : } (h : (t : (set.Icc v.t_min v.t_max)), has_dist.dist (f₁ t) (f₂ t) ((v.L) * |t - (v.t₀)|) ^ n / (n.factorial) * d) (t : (set.Icc v.t_min v.t_max)) :
has_dist.dist ((f₁.next) t) ((f₂.next) t) ((v.L) * |t - (v.t₀)|) ^ (n + 1) / ((n + 1).factorial) * d

Picard-Lindelöf (Cauchy-Lipschitz) theorem. Use exists_forall_deriv_within_Icc_eq_of_is_picard_lindelof instead for the public API.

theorem is_picard_lindelof.norm_le₀ {E : Type u_1} [normed_add_comm_group E] {v : E E} {t_min t₀ t_max : } {x₀ : E} {C R : } {L : nnreal} (hpl : is_picard_lindelof v t_min t₀ t_max x₀ L R C) :
v t₀ x₀ C
theorem exists_forall_deriv_within_Icc_eq_of_is_picard_lindelof {E : Type u_1} [normed_add_comm_group E] [normed_space E] [complete_space E] {v : E E} {t_min t₀ t_max : } (x₀ : E) {C R : } {L : nnreal} (hpl : is_picard_lindelof v t_min t₀ t_max x₀ L R C) :
(f : E), f t₀ = x₀ (t : ), t set.Icc t_min t_max has_deriv_within_at f (v t (f t)) (set.Icc t_min t_max) t

Picard-Lindelöf (Cauchy-Lipschitz) theorem.

theorem exists_is_picard_lindelof_const_of_cont_diff_on_nhds {E : Type u_1} [normed_add_comm_group E] [normed_space E] [proper_space E] {v : E E} (t₀ : ) (x₀ : E) {s : set E} (hv : cont_diff_on 1 v s) (hs : s nhds x₀) :
(ε : ) (H : ε > 0) (L : nnreal) (R C : ), is_picard_lindelof (λ (t : ), v) (t₀ - ε) t₀ (t₀ + ε) x₀ L R C

A time-independent, locally continuously differentiable ODE satisfies the hypotheses of the Picard-Lindelöf theorem.

theorem exists_forall_deriv_at_Ioo_eq_of_cont_diff_on_nhds {E : Type u_1} [normed_add_comm_group E] [normed_space E] [proper_space E] {v : E E} (t₀ : ) (x₀ : E) {s : set E} (hv : cont_diff_on 1 v s) (hs : s nhds x₀) :
(ε : ) (H : ε > 0) (f : E), f t₀ = x₀ (t : ), t set.Ioo (t₀ - ε) (t₀ + ε) f t s has_deriv_at f (v (f t)) t

A time-independent, locally continuously differentiable ODE admits a solution in some open interval.

theorem exists_forall_deriv_at_Ioo_eq_of_cont_diff {E : Type u_1} [normed_add_comm_group E] [normed_space E] [proper_space E] {v : E E} (t₀ : ) (x₀ : E) (hv : cont_diff 1 v) :
(ε : ) (H : ε > 0) (f : E), f t₀ = x₀ (t : ), t set.Ioo (t₀ - ε) (t₀ + ε) has_deriv_at f (v (f t)) t

A time-independent, continuously differentiable ODE admits a solution in some open interval.