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 theorem
• IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt: the existence theorem for local solutions to time-dependent ODEs
• IsPicardLindelof.exists_forall_mem_closedBall_eq_forall_mem_Icc_hasDerivWithinAt: the existence theorem for local flows to time-dependent vector fields
• IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith: there exists a local flow to time-dependent vector fields, and it is Lipschitz-continuous with respect to the starting point.

Implementation notes

• The structure FunSpace and 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 FunSpace as the space of continuous functions from a closed interval to a closed ball. We instead define FunSpace here 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 space E until 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_unique and related theorems in Mathlib/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

structure IsPicardLindelof {E : Type u_1} [NormedAddCommGroup E] (f : ℝ → E → E) {tmin tmax : ℝ} (t₀ : ↑(Set.Icc tmin tmax)) (x₀ : E) (a r L K : NNReal) : Prop

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 K within 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.

• norm_le (t : ℝ) : t ∈ Set.Icc tmin tmax → ∀ x ∈ Metric.closedBall x₀ ↑a, ‖f t x‖ ≤ ↑L

  L is an upper bound of the norm of the vector field.

• mul_max_le : ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) ≤ ↑a - ↑r

  The time interval of validity

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.

noncomputable def ODE.picard {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E → E) (t₀ : ℝ) (x₀ : E) (α : ℝ → E) : ℝ → E

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.

@[simp]

theorem ODE.picard_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {α : ℝ → E} {t₀ : ℝ} {x₀ : E} {t : ℝ} : picard f t₀ x₀ α t = x₀ + ∫ (τ : ℝ) in t₀..t, f τ (α τ)

theorem ODE.picard_apply₀ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {α : ℝ → E} {t₀ : ℝ} {x₀ : E} : picard f t₀ x₀ α t₀ = x₀

theorem ODE.contDiffOn_comp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {α : ℝ → E} {s : Set ℝ} {u : Set E} {n : WithTop ℕ∞} (hf : ContDiffOn ℝ n (Function.uncurry f) (s ×ˢ u)) (hα : ContDiffOn ℝ n α s) (hmem : ∀ t ∈ s, α t ∈ u) : ContDiffOn ℝ n (fun (t : ℝ) => f t (α t)) s

Given a $C^n$ time-dependent vector field f and a $C^n$ curve α, the composition f t (α t) is $C^n$ in t.

theorem ODE.continuousOn_comp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {α : ℝ → E} {s : Set ℝ} {u : Set E} (hf : ContinuousOn (Function.uncurry f) (s ×ˢ u)) (hα : ContinuousOn α s) (hmem : Set.MapsTo α s u) : ContinuousOn (fun (t : ℝ) => f t (α t)) s

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.

structure ODE.FunSpace {E : Type u_1} [NormedAddCommGroup E] {tmin tmax : ℝ} (t₀ : ↑(Set.Icc tmin tmax)) (x₀ : E) (r L : NNReal) : Type u_1

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
• mem_closedBall₀ : self.toFun t₀ ∈ Metric.closedBall x₀ ↑r

instance ODE.FunSpace.instCoeFunForallElemRealIcc {E : Type u_1} [NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal} : CoeFun (FunSpace t₀ x₀ r L) fun (x : FunSpace t₀ x₀ r L) => ↑(Set.Icc tmin tmax) → E

instance ODE.FunSpace.instInhabited {E : Type u_1} [NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal} : Inhabited (FunSpace t₀ x₀ r L)

FunSpace t₀ x₀ r L contains the constant map at x₀.

theorem ODE.FunSpace.continuous {E : Type u_1} [NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal} (α : FunSpace t₀ x₀ L r) : Continuous α.toFun

def ODE.FunSpace.toContinuousMap {E : Type u_1} [NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal} : FunSpace t₀ x₀ r L ↪ C(↑(Set.Icc tmin tmax), E)

The embedding of FunSpace into the space of continuous maps

@[simp]

theorem ODE.FunSpace.toContinuousMap_apply_eq_apply {E : Type u_1} [NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal} (α : FunSpace t₀ x₀ r L) (t : ↑(Set.Icc tmin tmax)) : (toContinuousMap α) t = α.toFun t

noncomputable instance ODE.FunSpace.instMetricSpace {E : Type u_1} [NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal} : MetricSpace (FunSpace t₀ x₀ r L)

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.

theorem ODE.FunSpace.isUniformInducing_toContinuousMap {E : Type u_1} [NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal} : IsUniformInducing fun (α : FunSpace t₀ x₀ r L) => toContinuousMap α

theorem ODE.FunSpace.range_toContinuousMap {E : Type u_1} [NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal} : (Set.range fun (α : FunSpace t₀ x₀ r L) => toContinuousMap α) = {α : C(↑(Set.Icc tmin tmax), E) | LipschitzWith L ⇑α ∧ α t₀ ∈ Metric.closedBall x₀ ↑r}

instance ODE.FunSpace.instCompleteSpace {E : Type u_1} [NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal} [CompleteSpace E] : CompleteSpace (FunSpace t₀ x₀ r L)

We show that FunSpace is complete in order to apply the contraction mapping theorem.

noncomputable def ODE.FunSpace.compProj {E : Type u_1} [NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal} (α : FunSpace t₀ x₀ r L) (t : ℝ) : E

Extend the domain of α from Icc tmin tmax to ℝ such that α t = α tmin for all t ≤ tmin and α t = α tmax for all t ≥ tmax.

@[simp]

theorem ODE.FunSpace.compProj_apply {E : Type u_1} [NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal} {α : FunSpace t₀ x₀ r L} {t : ℝ} : α.compProj t = α.toFun (Set.projIcc tmin tmax ⋯ t)

theorem ODE.FunSpace.compProj_val {E : Type u_1} [NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal} {α : FunSpace t₀ x₀ r L} {t : ↑(Set.Icc tmin tmax)} : α.compProj ↑t = α.toFun t

theorem ODE.FunSpace.compProj_of_mem {E : Type u_1} [NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal} {α : FunSpace t₀ x₀ r L} {t : ℝ} (ht : t ∈ Set.Icc tmin tmax) : α.compProj t = α.toFun ⟨t, ht⟩

theorem ODE.FunSpace.continuous_compProj {E : Type u_1} [NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {r L : NNReal} (α : FunSpace t₀ x₀ r L) : Continuous α.compProj

theorem ODE.FunSpace.mem_closedBall {E : Type u_1} [NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L : NNReal} {α : FunSpace t₀ x₀ r L} (h : ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) ≤ ↑a - ↑r) {t : ↑(Set.Icc tmin tmax)} : α.toFun t ∈ Metric.closedBall x₀ ↑a

The image of a function in FunSpace is contained within a closed ball.

theorem ODE.FunSpace.compProj_mem_closedBall {E : Type u_1} [NormedAddCommGroup E] {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L : NNReal} (α : FunSpace t₀ x₀ r L) (h : ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) ≤ ↑a - ↑r) {t : ℝ} : α.compProj t ∈ Metric.closedBall x₀ ↑a

Contracting map on the space of Lipschitz functions

theorem ODE.FunSpace.continuousOn_comp_compProj {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) (α : FunSpace t₀ x₀ r L) : ContinuousOn (fun (t' : ℝ) => f t' (α.compProj t')) (Set.Icc tmin tmax)

The integrand in next is continuous.

theorem ODE.FunSpace.intervalIntegrable_comp_compProj {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) (α : FunSpace t₀ x₀ r L) (t : ↑(Set.Icc tmin tmax)) : IntervalIntegrable (fun (t' : ℝ) => f t' (α.compProj t')) MeasureTheory.volume ↑t₀ ↑t

The integrand in next is integrable.

noncomputable def ODE.FunSpace.next {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) (hx : x ∈ Metric.closedBall x₀ ↑r) (α : FunSpace t₀ x₀ r L) : FunSpace t₀ x₀ r L

The map on FunSpace defined by picard, some n-th iterate of which will be a contracting map

@[simp]

theorem ODE.FunSpace.next_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) (hx : x ∈ Metric.closedBall x₀ ↑r) (α : FunSpace t₀ x₀ r L) {t : ↑(Set.Icc tmin tmax)} : (next hf hx α).toFun t = picard f (↑t₀) x α.compProj ↑t

theorem ODE.FunSpace.next_apply₀ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) (hx : x ∈ Metric.closedBall x₀ ↑r) (α : FunSpace t₀ x₀ r L) : (next hf hx α).toFun t₀ = x

theorem ODE.FunSpace.dist_comp_iterate_next_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) (hx : x ∈ Metric.closedBall x₀ ↑r) (n : ℕ) (t : ↑(Set.Icc tmin tmax)) {α β : FunSpace t₀ x₀ r L} (h : dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n.factorial * dist α β) : dist (f (↑t) (((next hf hx)^[n] α).toFun t)) (f (↑t) (((next hf hx)^[n] β).toFun t)) ≤ ↑K ^ (n + 1) * |↑t - ↑t₀| ^ n / ↑n.factorial * dist α β

A key step in the inductive case of dist_iterate_next_apply_le

theorem ODE.FunSpace.dist_iterate_next_apply_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) (hx : x ∈ Metric.closedBall x₀ ↑r) (α β : FunSpace t₀ x₀ r L) (n : ℕ) (t : ↑(Set.Icc tmin tmax)) : dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n.factorial * dist α β

A time-dependent bound on the distance between the n-th iterates of next on two curves

theorem ODE.FunSpace.dist_iterate_next_iterate_next_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) (hx : x ∈ Metric.closedBall x₀ ↑r) (α β : FunSpace t₀ x₀ r L) (n : ℕ) : dist ((next hf hx)^[n] α) ((next hf hx)^[n] β) ≤ (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ n / ↑n.factorial * dist α β

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!$.

theorem ODE.FunSpace.exists_contractingWith_iterate_next {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) : ∃ (n : ℕ) (C : NNReal), ∀ (x : E) (hx : x ∈ Metric.closedBall x₀ ↑r), ContractingWith C (next hf hx)^[n]

Some n-th iterate of next is a contracting map, and its associated Lipschitz constant is independent of the initial point.

theorem ODE.FunSpace.exists_isFixedPt_next {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x : E} {a r L K : NNReal} [CompleteSpace E] (hf : IsPicardLindelof f t₀ x₀ a r L K) (hx : x ∈ Metric.closedBall x₀ ↑r) : ∃ (α : FunSpace t₀ x₀ r L), Function.IsFixedPt (next hf hx) α

The map next has a fixed point in the space of curves. This will be used to construct a solution α : ℝ → E to the ODE.

Lipschitz continuity of the solution with respect to the initial condition

The proof relies on the fact that the repeated application of next to any curve α converges to the fixed point of next, so it suffices to bound the distance between α and next^[n] α. Since there is some m : ℕ such that next^[m] is a contracting map, it further suffices to bound the distance between α and next^[m]^[n] α.

theorem ODE.FunSpace.dist_next_next {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x y : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) (hx : x ∈ Metric.closedBall x₀ ↑r) (hy : y ∈ Metric.closedBall x₀ ↑r) (α : FunSpace t₀ x₀ r L) : dist (next hf hx α) (next hf hy α) = dist x y

A key step in the base case of exists_forall_closedBall_funSpace_dist_le_mul

theorem ODE.FunSpace.dist_iterate_next_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) (hx : x ∈ Metric.closedBall x₀ ↑r) (α : FunSpace t₀ x₀ r L) (n : ℕ) : dist α ((next hf hx)^[n] α) ≤ (∑ i ∈ Finset.range n, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i.factorial) * dist α (next hf hx α)

theorem ODE.FunSpace.dist_iterate_iterate_next_le_of_lipschitzWith {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) (hx : x ∈ Metric.closedBall x₀ ↑r) (α : FunSpace t₀ x₀ r L) {m : ℕ} {C : NNReal} (hm : LipschitzWith C (next hf hx)^[m]) (n : ℕ) : dist α ((next hf hx)^[m]^[n] α) ≤ ((∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i.factorial) * ∑ i ∈ Finset.range n, ↑C ^ i) * dist α (next hf hx α)

theorem ODE.FunSpace.exists_forall_closedBall_funSpace_dist_le_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal} [CompleteSpace E] (hf : IsPicardLindelof f t₀ x₀ a r L K) : ∃ (L' : NNReal), ∀ (x y : E) (hx : x ∈ Metric.closedBall x₀ ↑r) (hy : y ∈ Metric.closedBall x₀ ↑r) (α β : FunSpace t₀ x₀ r L), Function.IsFixedPt (next hf hx) α → Function.IsFixedPt (next hf hy) β → dist α β ≤ ↑L' * dist x y

The pointwise distance between any two integral curves α and β over their domains is bounded by a constant L' times the distance between their respective initial points. This is the result of taking the limit of dist_iterate_iterate_next_le_of_lipschitzWith as n → ∞. This implies that the local solution of a vector field is Lipschitz continuous in the initial condition.

Properties of the integral equation

theorem ODE.hasDerivWithinAt_picard_Icc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {α : ℝ → E} {u : Set E} {t₀ tmin tmax : ℝ} (ht₀ : t₀ ∈ Set.Icc tmin tmax) (hf : ContinuousOn (Function.uncurry f) (Set.Icc tmin tmax ×ˢ u)) (hα : ContinuousOn α (Set.Icc tmin tmax)) (hmem : ∀ t ∈ Set.Icc tmin tmax, α t ∈ u) (x₀ : E) {t : ℝ} (ht : t ∈ Set.Icc tmin tmax) : HasDerivWithinAt (picard f t₀ x₀ α) (f t (α t)) (Set.Icc tmin tmax) t

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

theorem IsPicardLindelof.continuousOn_uncurry {E : Type u_1} [NormedAddCommGroup E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) : ContinuousOn (Function.uncurry f) (Set.Icc tmin tmax ×ˢ Metric.closedBall x₀ ↑a)

theorem IsPicardLindelof.of_time_independent {E : Type u_1} [NormedAddCommGroup E] {f : E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal} (hb : ∀ x ∈ Metric.closedBall x₀ ↑a, ‖f x‖ ≤ ↑L) (hl : LipschitzOnWith K f (Metric.closedBall x₀ ↑a)) (hm : ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) ≤ ↑a - ↑r) : IsPicardLindelof (fun (x : ℝ) => f) t₀ x₀ a r L K

The special case where the vector field is independent of time

theorem IsPicardLindelof.of_contDiffAt_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → E} {x₀ : E} (hf : ContDiffAt ℝ 1 f x₀) (t₀ : ℝ) : ∃ (ε : ℝ) (hε : 0 < ε) (a : NNReal) (r : NNReal) (L : NNReal) (K : NNReal) (_ : 0 < r), IsPicardLindelof (fun (x : ℝ) => f) ⟨t₀, ⋯⟩ x₀ a r L K

A time-independent, continuously differentiable ODE satisfies the hypotheses of the Picard-Lindelöf theorem.

Existence of solutions to ODEs

theorem IsPicardLindelof.exists_eq_forall_mem_Icc_eq_picard {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) (hx : x ∈ Metric.closedBall x₀ ↑r) : ∃ (α : ℝ → E), α ↑t₀ = x ∧ ∀ t ∈ Set.Icc tmin tmax, α t = ODE.picard f (↑t₀) x α t

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.

theorem IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) (hx : x ∈ Metric.closedBall x₀ ↑r) : ∃ (α : ℝ → E), α ↑t₀ = x ∧ ∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Set.Icc tmin tmax) t

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.

theorem IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt₀ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a 0 L K) : ∃ (α : ℝ → E), α ↑t₀ = x₀ ∧ ∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Set.Icc tmin tmax) t

Picard-Lindelöf (Cauchy-Lipschitz) theorem, differential form.

@[deprecated IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt₀ (since := "2025-06-24")]

theorem IsPicardLindelof.exists_forall_hasDerivWithinAt_Icc_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a 0 L K) : ∃ (α : ℝ → E), α ↑t₀ = x₀ ∧ ∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Set.Icc tmin tmax) t

Alias of IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt₀.

---

Picard-Lindelöf (Cauchy-Lipschitz) theorem, differential form.

theorem IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) : ∃ (α : E → ℝ → E), (∀ x ∈ Metric.closedBall x₀ ↑r, α x ↑t₀ = x ∧ ∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt (α x) (f t (α x t)) (Set.Icc tmin tmax) t) ∧ ∃ (L' : NNReal), ∀ t ∈ Set.Icc tmin tmax, LipschitzOnWith L' (fun (x : E) => α x t) (Metric.closedBall x₀ ↑r)

Picard-Lindelöf (Cauchy-Lipschitz) theorem, differential form. This version shows the existence of a local flow and that it is Lipschitz continuous in the initial point.

theorem IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_continuousOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) : ∃ (α : E × ℝ → E), (∀ x ∈ Metric.closedBall x₀ ↑r, α (x, ↑t₀) = x ∧ ∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt (fun (x_1 : ℝ) => α (x, x_1)) (f t (α (x, t))) (Set.Icc tmin tmax) t) ∧ ContinuousOn α (Metric.closedBall x₀ ↑r ×ˢ Set.Icc tmin tmax)

Picard-Lindelöf (Cauchy-Lipschitz) theorem, differential form. This version shows the existence of a local flow and that it is continuous on its domain as a (partial) map E × ℝ → E.

theorem IsPicardLindelof.exists_forall_mem_closedBall_eq_forall_mem_Icc_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K) : ∃ (α : E → ℝ → E), ∀ x ∈ Metric.closedBall x₀ ↑r, α x ↑t₀ = x ∧ ∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt (α x) (f t (α x t)) (Set.Icc tmin tmax) t

Picard-Lindelöf (Cauchy-Lipschitz) theorem, differential form. This version shows the existence of a local flow.

$C^1$ vector field

theorem ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : E → E} {x₀ : E} (hf : ContDiffAt ℝ 1 f x₀) (t₀ : ℝ) : ∃ r > 0, ∃ ε > 0, ∀ x ∈ Metric.closedBall x₀ r, ∃ (α : ℝ → E), α t₀ = x ∧ ∀ t ∈ Set.Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t

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₀.

theorem ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt₀ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : E → E} {x₀ : E} (hf : ContDiffAt ℝ 1 f x₀) (t₀ : ℝ) : ∃ (α : ℝ → E), α t₀ = x₀ ∧ ∃ ε > 0, ∀ t ∈ Set.Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t

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₀.

@[deprecated ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt₀ (since := "2025-06-24")]

theorem ContDiffAt.exists_forall_hasDerivAt_Ioo_eq_of_contDiffAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : E → E} {x₀ : E} (hf : ContDiffAt ℝ 1 f x₀) (t₀ : ℝ) : ∃ (α : ℝ → E), α t₀ = x₀ ∧ ∃ ε > 0, ∀ t ∈ Set.Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t

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₀.

theorem ContDiffAt.exists_eventually_eq_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : E → E} {x₀ : E} (hf : ContDiffAt ℝ 1 f x₀) (t₀ : ℝ) : ∃ (α : E → ℝ → E), ∀ᶠ (xt : E × ℝ) in nhds x₀ ×ˢ nhds t₀, α xt.1 t₀ = xt.1 ∧ HasDerivAt (α xt.1) (f (α xt.1 xt.2)) xt.2

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.