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.instCoeFunForallRealForall = { 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]
.
Instances For
Projection $ℝ → [t_{\min}, t_{\max}]$ sending $(-∞, t_{\min}]$ to $t_{\min}$ and $[t_{\max}, ∞)$ to $t_{\max}$.
Equations
- v.proj = 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.instCoeFunForallElemRealIccTMinTMax = { coe := PicardLindelof.FunSpace.toFun }
Each curve in PicardLindelof.FunSpace
is continuous.
Equations
- PicardLindelof.FunSpace.toContinuousMap = { toFun := fun (f : v.FunSpace) => { toFun := f.toFun, continuous_toFun := ⋯ }, inj' := ⋯ }
Instances For
Equations
- PicardLindelof.FunSpace.instMetricSpace = 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
- f.vComp t = v.toFun (↑(v.proj t)) (f.toFun (v.proj 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
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.