Picard-Lindelöf (Cauchy-Lipschitz) Theorem #
We prove the (local) existence of integral curves and flows to time-dependent vector fields.
Let f : ℝ → E → E be a time-dependent (local) vector field on a Banach space, and let t₀ : ℝ
and x₀ : E. If f is Lipschitz continuous in x within a closed ball around x₀ of radius
a ≥ 0 at every t and continuous in t at every x, then there exists a (local) solution
α : ℝ → E to the initial value problem α t₀ = x₀ and deriv α t = f t (α t) for all
t ∈ Icc tmin tmax, where L * max (tmax - t₀) (t₀ - tmin) ≤ a.
We actually prove a more general version of this theorem for the existence of local flows. If there
is some r ≥ 0 such that L * max (tmax - t₀) (t₀ - tmin) ≤ a - r, then for every
x ∈ closedBall x₀ r, there exists a (local) solution α x with the initial condition α t₀ = x.
In other words, there exists a local flow α : E → ℝ → E defined on closedBall x₀ r and
Icc tmin tmax.
The proof relies on demonstrating the existence of a solution α to the following integral
equation:
$$\alpha(t) = x_0 + \int_{t_0}^t f(\tau, \alpha(\tau))\,\mathrm{d}\tau.$$
This is done via the contraction mapping theorem, applied to the space of Lipschitz continuous
functions from a closed interval to a Banach space. The needed contraction map is constructed by
repeated applications of the right hand side of this equation.
Main definitions and results #
picard f t₀ x₀ α t: the Picard iteration, applied to the curveαIsPicardLindelof: the structure holding the assumptions of the Picard-Lindelöf theoremIsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt: the existence theorem for local solutions to time-dependent ODEsIsPicardLindelof.exists_forall_mem_closedBall_eq_forall_mem_Icc_hasDerivWithinAt: the existence theorem for local flows to time-dependent vector fields
Implementation notes #
- The structure
FunSpaceand theorems within this namespace are implementation details of the proof of the Picard-Lindelöf theorem and are not intended to be used outside of this file. - Some sources, such as Lang, define
FunSpaceas the space of continuous functions from a closed interval to a closed ball. We instead defineFunSpacehere as the space of Lipschitz continuous functions from a closed interval. This slightly stronger condition allows us to postpone the usage of the completeness condition on the spaceEuntil the application of the contraction mapping theorem. - We have chosen to formalise many of the real constants as
ℝ≥0, so that the non-negativity of certain quantities constructed from them can be shown more easily. When subtraction is involved, especially note whether it is the usual subtraction between two reals or the truncated subtraction between two non-negative reals. - In this file, We only prove the existence of a solution. For uniqueness, see
ODE_solution_uniqueand related theorems inMathlib/Analysis/ODE/Gronwall.lean.
Tags #
differential equation, dynamical system, initial value problem, Picard-Lindelöf theorem, Cauchy-Lipschitz theorem
Assumptions of the Picard-Lindelöf theorem #
Prop structure holding the assumptions of the Picard-Lindelöf theorem.
IsPicardLindelof f t₀ x₀ a r L K, where t₀ ∈ Icc tmin tmax, means that the time-dependent vector
field f satisfies the conditions to admit an integral curve α : ℝ → E to f defined on
Icc tmin tmax with the initial condition α t₀ = x, where ‖x - x₀‖ ≤ r. Note that the initial
point x is allowed to differ from the point x₀ about which the conditions on f are stated.
- lipschitzOnWith (t : ℝ) : t ∈ Set.Icc tmin tmax → LipschitzOnWith K (f t) (Metric.closedBall x₀ ↑a)
The vector field at any time is Lipschitz with constant
Kwithin a closed ball. - continuousOn (x : E) : x ∈ Metric.closedBall x₀ ↑a → ContinuousOn (fun (x_1 : ℝ) => f x_1 x) (Set.Icc tmin tmax)
The vector field is continuous in time within a closed ball.
Lis an upper bound of the norm of the vector field.The time interval of validity
Instances For
Integral equation #
For any time-dependent vector field f : ℝ → E → E, we define an integral equation that is
equivalent to the initial value problem defined by f.
The Picard iteration. It will be shown that if α : ℝ → E and picard f t₀ x₀ α agree on an
interval containing t₀, then α is a solution to f with α t₀ = x₀ on this interval.
Instances For
Given a $C^n$ time-dependent vector field f and a $C^n$ curve α, the composition f t (α t)
is $C^n$ in t.
Given a continuous time-dependent vector field f and a continuous curve α, the composition
f t (α t) is continuous in t.
Space of Lipschitz functions on a closed interval #
We define the space of Lipschitz continuous functions from a closed interval. This will be shown to
be a complete metric space on which picard is a contracting map, leading to a fixed point that
will serve as the solution to the ODE. The domain is a closed interval in order to easily inherit
the sup metric from continuous maps on compact spaces. We cannot use functions ℝ → E with junk
values outside the domain, as the supremum within a closed interval will only be a pseudo-metric,
and the contracting map will fail to have a fixed point. In order to accommodate flows, we do not
require a specific initial condition. Rather, FunSpace contains curves whose initial condition is
within a closed ball.
The space of L-Lipschitz functions α : Icc tmin tmax → E
- toFun : ↑(Set.Icc tmin tmax) → E
The domain is
Icc tmin tmax. - lipschitzWith : LipschitzWith L self.toFun
Instances For
Equations
- ODE.FunSpace.instCoeFunForallElemRealIcc = { coe := fun (α : ODE.FunSpace t₀ x₀ r L) => α.toFun }
FunSpace t₀ x₀ r L contains the constant map at x₀.
The embedding of FunSpace into the space of continuous maps
Equations
- ODE.FunSpace.toContinuousMap = { toFun := fun (α : ODE.FunSpace t₀ x₀ r L) => { toFun := α.toFun, continuous_toFun := ⋯ }, inj' := ⋯ }
Instances For
The metric between two curves α and β is the supremum of the metric between α t and β t
over all t in the domain. This is finite when the domain is compact, such as a closed
interval in our case.
We show that FunSpace is complete in order to apply the contraction mapping theorem.
Extend the domain of α from Icc tmin tmax to ℝ such that α t = α tmin for all t ≤ tmin
and α t = α tmax for all t ≥ tmax.
Equations
- α.compProj t = α.toFun (Set.projIcc tmin tmax ⋯ t)
Instances For
The image of a function in FunSpace is contained within a closed ball.
Contracting map on the space of Lipschitz functions #
The integrand in next is continuous.
The integrand in next is integrable.
The map on FunSpace defined by picard, some n-th iterate of which will be a contracting
map
Equations
- ODE.FunSpace.next hf hx α = { toFun := fun (t : ↑(Set.Icc tmin tmax)) => ODE.picard f (↑t₀) x α.compProj ↑t, lipschitzWith := ⋯, mem_closedBall₀ := ⋯ }
Instances For
A key step in the inductive case of dist_iterate_next_apply_le
A time-dependent bound on the distance between the n-th iterates of next on two curves
The n-th iterate of next is Lipschitz continuous with respect to FunSpace, with constant
$(K \max(t_{\mathrm{max}}, t_{\mathrm{min}})^n / n!$.
Some n-th iterate of next is a contracting map, and its associated Lipschitz constant is
independent of the initial point.
The map next has a fixed point in the space of curves. This will be used to construct a
solution α : ℝ → E to the ODE.
Properties of the integral equation #
If the time-dependent vector field f and the curve α are continuous, then f t (α t) is the
derivative of picard f t₀ x₀ α.
Properties of IsPicardLindelof #
The special case where the vector field is independent of time
A time-independent, continuously differentiable ODE satisfies the hypotheses of the Picard-Lindelöf theorem.
Existence of solutions to ODEs #
Picard-Lindelöf (Cauchy-Lipschitz) theorem, integral form. This version shows the existence
of a local solution whose initial point x may be be different from the centre x₀ of the closed
ball within which the properties of the vector field hold.
Picard-Lindelöf (Cauchy-Lipschitz) theorem, differential form. This version shows the
existence of a local solution whose initial point x may be be different from the centre x₀ of
the closed ball within which the properties of the vector field hold.
Picard-Lindelöf (Cauchy-Lipschitz) theorem, differential form.
Alias of IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt₀.
Picard-Lindelöf (Cauchy-Lipschitz) theorem, differential form.
Picard-Lindelöf (Cauchy-Lipschitz) theorem, differential form. This version shows the existence of a local flow.
$C^1$ vector field #
If a vector field f : E → E is continuously differentiable at x₀ : E, then it admits an
integral curve α : ℝ → E defined on an open interval, with initial condition α t₀ = x, where
x may be different from x₀.
If a vector field f : E → E is continuously differentiable at x₀ : E, then it admits an
integral curve α : ℝ → E defined on an open interval, with initial condition α t₀ = x₀.
Alias of ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt₀.
If a vector field f : E → E is continuously differentiable at x₀ : E, then it admits an
integral curve α : ℝ → E defined on an open interval, with initial condition α t₀ = x₀.
If a vector field f : E → E is continuously differentiable at x₀ : E, then it admits a flow
α : E → ℝ → E defined on an open domain, with initial condition α x t₀ = x for all x within
the domain.