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
- hR : 0 ≤ R
- lipschitz : ∀ (t : ℝ), t ∈ Set.Icc tMin tMax → LipschitzOnWith L (v t) (Metric.closedBall x₀ R)
- cont : ∀ (x : E), x ∈ Metric.closedBall x₀ R → ContinuousOn (fun t => v t x) (Set.Icc tMin tMax)
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
- toFun : ℝ → E → E
- tMin : ℝ
- tMax : ℝ
- t₀ : ↑(Set.Icc s.tMin s.tMax)
- x₀ : E
- C : NNReal
- R : NNReal
- L : NNReal
- isPicardLindelof : IsPicardLindelof s.toFun s.tMin (↑s.t₀) s.tMax s.x₀ s.L ↑s.R ↑s.C
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
The maximum of distances from t₀ to the endpoints of [tMin, tMax].
Instances For
Projection $ℝ → [t_{\min}, t_{\max}]$ sending $(-∞, t_{\min}]$ to $t_{\min}$ and $[t_{\max}, ∞)$ to $t_{\max}$.
Instances For
- toFun : ↑(Set.Icc v.tMin v.tMax) → E
- map_t₀' : PicardLindelof.FunSpace.toFun s v.t₀ = v.x₀
- lipschitz' : LipschitzWith v.C s.toFun
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
Each curve in PicardLindelof.FunSpace is continuous.
Instances For
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
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
Picard-Lindelöf (Cauchy-Lipschitz) theorem. Use
IsPicardLindelof.exists_forall_hasDerivWithinAt_Icc_eq instead for the public API.
Picard-Lindelöf (Cauchy-Lipschitz) theorem.
A time-independent, locally continuously differentiable ODE satisfies the hypotheses of the Picard-Lindelöf theorem.
A time-independent, locally continuously differentiable ODE admits a solution in some open interval.
A time-independent, continuously differentiable ODE admits a solution in some open interval.