mathlib documentation

analysis.ODE.picard_lindelof

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

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_lipschitz_of_continuous.

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.

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 picard_lindelof (E : Type u_2) [normed_group E] [normed_space E] :
Type u_2

This structure holds arguments of the Picard-Lipschitz (Cauchy-Lipschitz) theorem. 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.

Instances for picard_lindelof
@[protected, instance]
def picard_lindelof.has_coe_to_fun {E : Type u_1} [normed_group E] [normed_space E] :
has_coe_to_fun (picard_lindelof E) (λ (_x : picard_lindelof E), E → E)
Equations
@[protected, instance]
Equations
@[protected]
@[protected]
theorem picard_lindelof.norm_le {E : Type u_1} [normed_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_group E] [normed_space E] (v : picard_lindelof E) :

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

Equations
noncomputable def picard_lindelof.proj {E : Type u_1} [normed_group E] [normed_space E] (v : picard_lindelof E) :

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

Equations
theorem picard_lindelof.proj_coe {E : Type u_1} [normed_group E] [normed_space E] (v : picard_lindelof E) (t : (set.Icc v.t_min v.t_max)) :
v.proj t = t
theorem picard_lindelof.proj_of_mem {E : Type u_1} [normed_group E] [normed_space E] (v : picard_lindelof E) {t : } (ht : t set.Icc v.t_min v.t_max) :
(v.proj t) = t
@[continuity]
structure picard_lindelof.fun_space {E : Type u_1} [normed_group E] [normed_space E] (v : picard_lindelof E) :
Type u_1

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
@[protected, instance]
Equations
@[protected]
@[protected]
@[protected]
noncomputable def picard_lindelof.fun_space.v_comp {E : Type u_1} [normed_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_apply_le_dist {E : Type u_1} [normed_group E] [normed_space E] {v : picard_lindelof E} (f₁ f₂ : v.fun_space) (t : (set.Icc v.t_min v.t_max)) :
has_dist.dist (f₁ t) (f₂ t) has_dist.dist f₁ f₂
theorem picard_lindelof.fun_space.dist_le_of_forall {E : Type u_1} [normed_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
noncomputable def picard_lindelof.fun_space.next {E : Type u_1} [normed_group E] [normed_space E] {v : picard_lindelof E} [complete_space E] (f : v.fun_space) :

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.next_apply {E : Type u_1} [normed_group E] [normed_space E] {v : picard_lindelof E} (f : v.fun_space) [complete_space E] (t : (set.Icc v.t_min v.t_max)) :
(f.next) t = v.x₀ + ∫ (τ : ) in (v.t₀)..t, f.v_comp τ
theorem picard_lindelof.fun_space.dist_next_apply_le_of_le {E : Type u_1} [normed_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
theorem picard_lindelof.exists_fixed {E : Type u_1} [normed_group E] [normed_space E] (v : picard_lindelof E) [complete_space E] :
∃ (f : v.fun_space), f.next = f
theorem picard_lindelof.exists_solution {E : Type u_1} [normed_group E] [normed_space E] (v : picard_lindelof E) [complete_space E] :
∃ (f : → E), f (v.t₀) = v.x₀ ∀ (t : ), t set.Icc v.t_min v.t_maxhas_deriv_within_at f (v t (f t)) (set.Icc v.t_min v.t_max) t

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

theorem exists_forall_deriv_within_Icc_eq_of_lipschitz_of_continuous {E : Type u_1} [normed_group E] [normed_space E] [complete_space E] {v : E → E} {t_min t₀ t_max : } (ht₀ : t₀ set.Icc t_min t_max) (x₀ : E) {C R : } (hR : 0 R) {L : nnreal} (Hlip : ∀ (t : ), t set.Icc t_min t_maxlipschitz_on_with L (v t) (metric.closed_ball x₀ R)) (Hcont : ∀ (x : E), x metric.closed_ball x₀ Rcontinuous_on (λ (t : ), v t x) (set.Icc t_min t_max)) (Hnorm : ∀ (t : ), t set.Icc t_min t_max∀ (x : E), x metric.closed_ball x₀ Rv t x C) (Hmul_le : C * linear_order.max (t_max - t₀) (t₀ - t_min) R) :
∃ (f : → E), f t₀ = x₀ ∀ (t : ), t set.Icc t_min t_maxhas_deriv_within_at f (v t (f t)) (set.Icc t_min t_max) t

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