# Documentation

Mathlib.Analysis.ODE.PicardLindelof

# 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 IsPicardLindelof.exists_forall_hasDerivWithinAt_Icc_eq.

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 PicardLindelof that holds all assumptions of the main theorem. This structure and lemmas in the PicardLindelof namespace should be treated as private implementation details. This is not to be confused with the Prop- valued structure IsPicardLindelof, 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 Mathlib/Analysis/ODE/Gronwall.lean.

## Tags #

differential equation

structure IsPicardLindelof {E : Type u_2} (v : EE) (tMin : ) (t₀ : ) (tMax : ) (x₀ : E) (L : NNReal) (R : ) (C : ) :

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

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

Instances For
structure PicardLindelof (E : Type u_2) [] :
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 IsPicardLindelof.exists_forall_hasDerivWithinAt_Icc_eq instead of using this structure.

The similarly named IsPicardLindelof 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
instance PicardLindelof.instCoeFunPicardLindelofForAllReal {E : Type u_1} [] :
CoeFun () fun x => EE
theorem PicardLindelof.tMin_le_tMax {E : Type u_1} [] (v : ) :
v.tMin v.tMax
theorem PicardLindelof.nonempty_Icc {E : Type u_1} [] (v : ) :
Set.Nonempty (Set.Icc v.tMin v.tMax)
theorem PicardLindelof.lipschitzOnWith {E : Type u_1} [] (v : ) {t : } (ht : t Set.Icc v.tMin v.tMax) :
LipschitzOnWith v.L () (Metric.closedBall v.x₀ v.R)
theorem PicardLindelof.continuousOn {E : Type u_1} [] (v : ) :
ContinuousOn (Function.uncurry v.toFun) (Set.Icc v.tMin v.tMax ×ˢ Metric.closedBall v.x₀ v.R)
theorem PicardLindelof.norm_le {E : Type u_1} [] (v : ) {t : } (ht : t Set.Icc v.tMin v.tMax) {x : E} (hx : x Metric.closedBall v.x₀ v.R) :
v.C
def PicardLindelof.tDist {E : Type u_1} [] (v : ) :

The maximum of distances from t₀ to the endpoints of [tMin, tMax].

Instances For
theorem PicardLindelof.tDist_nonneg {E : Type u_1} [] (v : ) :
theorem PicardLindelof.dist_t₀_le {E : Type u_1} [] (v : ) (t : ↑(Set.Icc v.tMin v.tMax)) :
dist t v.t₀
def PicardLindelof.proj {E : Type u_1} [] (v : ) :
↑(Set.Icc v.tMin v.tMax)

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

Instances For
theorem PicardLindelof.proj_coe {E : Type u_1} [] (v : ) (t : ↑(Set.Icc v.tMin v.tMax)) :
= t
theorem PicardLindelof.proj_of_mem {E : Type u_1} [] (v : ) {t : } (ht : t Set.Icc v.tMin v.tMax) :
↑() = t
theorem PicardLindelof.continuous_proj {E : Type u_1} [] (v : ) :
structure PicardLindelof.FunSpace {E : Type u_1} [] (v : ) :
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
theorem PicardLindelof.FunSpace.lipschitz {E : Type u_1} [] {v : } (f : ) :
LipschitzWith v.C f.toFun
theorem PicardLindelof.FunSpace.continuous {E : Type u_1} [] {v : } (f : ) :
Continuous f.toFun
def PicardLindelof.FunSpace.toContinuousMap {E : Type u_1} [] {v : } :
C(↑(Set.Icc v.tMin v.tMax), E)

Each curve in PicardLindelof.FunSpace is continuous.

Instances For
theorem PicardLindelof.FunSpace.uniformInducing_toContinuousMap {E : Type u_1} [] {v : } :
UniformInducing PicardLindelof.FunSpace.toContinuousMap
theorem PicardLindelof.FunSpace.range_toContinuousMap {E : Type u_1} [] {v : } :
Set.range PicardLindelof.FunSpace.toContinuousMap = {f | f v.t₀ = v.x₀ LipschitzWith v.C f}
theorem PicardLindelof.FunSpace.map_t₀ {E : Type u_1} [] {v : } (f : ) :
= v.x₀
theorem PicardLindelof.FunSpace.mem_closedBall {E : Type u_1} [] {v : } (f : ) (t : ↑(Set.Icc v.tMin v.tMax)) :
Metric.closedBall v.x₀ v.R
def PicardLindelof.FunSpace.vComp {E : Type u_1} [] {v : } (f : ) (t : ) :
E

Given a curve $γ \colon [t_{\min}, t_{\max}] → E$, PicardLindelof.vComp 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.

Instances For
theorem PicardLindelof.FunSpace.vComp_apply_coe {E : Type u_1} [] {v : } (f : ) (t : ↑(Set.Icc v.tMin v.tMax)) :
theorem PicardLindelof.FunSpace.continuous_vComp {E : Type u_1} [] {v : } (f : ) :
theorem PicardLindelof.FunSpace.norm_vComp_le {E : Type u_1} [] {v : } (f : ) (t : ) :
v.C
theorem PicardLindelof.FunSpace.dist_apply_le_dist {E : Type u_1} [] {v : } (f₁ : ) (f₂ : ) (t : ↑(Set.Icc v.tMin v.tMax)) :
dist f₁ f₂
theorem PicardLindelof.FunSpace.dist_le_of_forall {E : Type u_1} [] {v : } {f₁ : } {f₂ : } {d : } (h : ∀ (t : ↑(Set.Icc v.tMin v.tMax)), d) :
dist f₁ f₂ d
theorem PicardLindelof.FunSpace.intervalIntegrable_vComp {E : Type u_1} [] {v : } (f : ) (t₁ : ) (t₂ : ) :
IntervalIntegrable () MeasureTheory.volume t₁ t₂
def PicardLindelof.FunSpace.next {E : Type u_1} [] {v : } (f : ) :

The Picard-Lindelöf operator. This is a contracting map on PicardLindelof.FunSpace 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.

Instances For
theorem PicardLindelof.FunSpace.next_apply {E : Type u_1} [] {v : } (f : ) (t : ↑(Set.Icc v.tMin v.tMax)) :
= v.x₀ + ∫ (τ : ) in v.t₀..t,
theorem PicardLindelof.FunSpace.hasDerivWithinAt_next {E : Type u_1} [] {v : } (f : ) [] (t : ↑(Set.Icc v.tMin v.tMax)) :
HasDerivWithinAt (().toFun ) () (Set.Icc v.tMin v.tMax) t
theorem PicardLindelof.FunSpace.dist_next_apply_le_of_le {E : Type u_1} [] {v : } {f₁ : } {f₂ : } {n : } {d : } (h : ∀ (t : ↑(Set.Icc v.tMin v.tMax)), (v.L * |t - v.t₀|) ^ n / ↑() * d) (t : ↑(Set.Icc v.tMin v.tMax)) :
(v.L * |t - v.t₀|) ^ (n + 1) / ↑(Nat.factorial (n + 1)) * d
theorem PicardLindelof.FunSpace.dist_iterate_next_apply_le {E : Type u_1} [] {v : } (f₁ : ) (f₂ : ) (n : ) (t : ↑(Set.Icc v.tMin v.tMax)) :
(v.L * |t - v.t₀|) ^ n / ↑() * dist f₁ f₂
theorem PicardLindelof.FunSpace.dist_iterate_next_le {E : Type u_1} [] {v : } (f₁ : ) (f₂ : ) (n : ) :
(v.L * ) ^ n / ↑() * dist f₁ f₂
theorem PicardLindelof.exists_contracting_iterate {E : Type u_1} [] (v : ) :
N K, ContractingWith K PicardLindelof.FunSpace.next^[N]
theorem PicardLindelof.exists_fixed {E : Type u_1} [] (v : ) [] :
f,
theorem PicardLindelof.exists_solution {E : Type u_1} [] (v : ) [] :
f, f v.t₀ = v.x₀ ∀ (t : ), t Set.Icc v.tMin v.tMaxHasDerivWithinAt f (PicardLindelof.toFun v t (f t)) (Set.Icc v.tMin v.tMax) t

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

theorem IsPicardLindelof.norm_le₀ {E : Type u_2} {v : EE} {tMin : } {t₀ : } {tMax : } {x₀ : E} {C : } {R : } {L : NNReal} (hpl : IsPicardLindelof v tMin t₀ tMax x₀ L R C) :
v t₀ x₀ C
theorem IsPicardLindelof.exists_forall_hasDerivWithinAt_Icc_eq {E : Type u_1} [] [] {v : EE} {tMin : } {t₀ : } {tMax : } (x₀ : E) {C : } {R : } {L : NNReal} (hpl : IsPicardLindelof v tMin t₀ tMax x₀ L R C) :
f, f t₀ = x₀ ∀ (t : ), t Set.Icc tMin tMaxHasDerivWithinAt f (v t (f t)) (Set.Icc tMin tMax) t

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

theorem exists_isPicardLindelof_const_of_contDiffOn_nhds {E : Type u_1} [] [] {v : EE} (t₀ : ) (x₀ : E) {s : Set E} (hv : ContDiffOn 1 v s) (hs : s nhds x₀) :
ε, ε > 0 L R C, IsPicardLindelof (fun x => 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_contDiffOn_nhds {E : Type u_1} [] [] {v : EE} (t₀ : ) (x₀ : E) {s : Set E} (hv : ContDiffOn 1 v s) (hs : s nhds x₀) :
ε, ε > 0 f, f t₀ = x₀ ∀ (t : ), t Set.Ioo (t₀ - ε) (t₀ + ε)f t s HasDerivAt f (v (f t)) t

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

theorem exists_forall_hasDerivAt_Ioo_eq_of_contDiff {E : Type u_1} [] [] {v : EE} (t₀ : ) (x₀ : E) (hv : ) :
ε, ε > 0 f, f t₀ = x₀ ∀ (t : ), t Set.Ioo (t₀ - ε) (t₀ + ε)HasDerivAt f (v (f t)) t

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