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
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.
- hR : 0 ≤ R
- lipschitz : ∀ t ∈ Set.Icc tMin tMax, LipschitzOnWith L (v t) (Metric.closedBall x₀ R)
- cont : ∀ x ∈ Metric.closedBall x₀ R, ContinuousOn (fun (t : ℝ) => v t x) (Set.Icc tMin tMax)
- norm_le : ∀ t ∈ Set.Icc tMin tMax, ∀ x ∈ Metric.closedBall x₀ R, ‖v t x‖ ≤ C
Instances For
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.
- toFun : ℝ → E → E
- tMin : ℝ
- tMax : ℝ
- t₀ : ↑(Set.Icc self.tMin self.tMax)
- x₀ : E
- C : NNReal
- R : NNReal
- L : NNReal
- isPicardLindelof : IsPicardLindelof self.toFun self.tMin (↑self.t₀) self.tMax self.x₀ self.L ↑self.R ↑self.C
Instances For
Equations
- PicardLindelof.instCoeFunPicardLindelofForAllReal = { coe := PicardLindelof.toFun }
Equations
- One or more equations did not get rendered due to their size.
The maximum of distances from t₀ to the endpoints of [tMin, tMax].
Equations
- PicardLindelof.tDist v = max (v.tMax - ↑v.t₀) (↑v.t₀ - v.tMin)
Instances For
Projection $ℝ → [t_{\min}, t_{\max}]$ sending $(-∞, t_{\min}]$ to $t_{\min}$ and $[t_{\max}, ∞)$ to $t_{\max}$.
Equations
- PicardLindelof.proj v = Set.projIcc v.tMin v.tMax ⋯
Instances For
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)$.
- toFun : ↑(Set.Icc v.tMin v.tMax) → E
- map_t₀' : self.toFun v.t₀ = v.x₀
- lipschitz' : LipschitzWith v.C self.toFun
Instances For
Equations
- PicardLindelof.FunSpace.instCoeFunFunSpaceForAllElemRealIccInstPreorderRealTMinTMax = { coe := PicardLindelof.FunSpace.toFun }
Each curve in PicardLindelof.FunSpace is continuous.
Equations
- PicardLindelof.FunSpace.toContinuousMap = { toFun := fun (f : PicardLindelof.FunSpace v) => { toFun := f.toFun, continuous_toFun := ⋯ }, inj' := ⋯ }
Instances For
Equations
- PicardLindelof.FunSpace.instMetricSpaceFunSpace = MetricSpace.induced ⇑PicardLindelof.FunSpace.toContinuousMap ⋯ inferInstance
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.
Equations
- PicardLindelof.FunSpace.vComp f t = v.toFun (↑(PicardLindelof.proj v t)) (f.toFun (PicardLindelof.proj v t))
Instances For
Equations
- ⋯ = ⋯
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.
Equations
- PicardLindelof.FunSpace.next f = { toFun := fun (t : ↑(Set.Icc v.tMin v.tMax)) => v.x₀ + ∫ (τ : ℝ) in ↑v.t₀..↑t, PicardLindelof.FunSpace.vComp f τ, map_t₀' := ⋯, lipschitz' := ⋯ }
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, continuously differentiable ODE satisfies the hypotheses of the Picard-Lindelöf theorem.
A time-independent, continuously differentiable ODE admits a solution in some open interval.
A time-independent, continuously differentiable ODE admits a solution in some open interval.