English
If the m-th iterate has Lipschitz constant C, then for all n the distance between α and the n-th iterate of the m-th iterate is bounded by the product of the m-sum in i and the n-sum in C, times dist α(next hf hx α).
Русский
Если m-я итерация имеет константу Lipschitz C, то расстояние между α и n-й итерацией m-й итерации ограничено произведением сумм в i и C на dist α(next α).
LaTeX
$$$\\forall α, hf, hx, m, C, n:\\ dist(α, (\\text{next } hf hx)^{[m]}^{[n]} α) \\le (\\sum_{i=0}^{m-1} (K\\max(t_{max}-t_0,t_0-t_{min}))^i/i!) \\ (\\sum_{i=0}^{n-1} C^i) \\ dist(α, (\\text{next } hf hx) α).$$$
Lean4
/-- **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 exists_forall_mem_closedBall_eq_hasDerivWithinAt_continuousOn (hf : IsPicardLindelof f t₀ x₀ a r L K) :
∃ α : E × ℝ → E,
(∀ x ∈ closedBall x₀ r,
α ⟨x, t₀⟩ = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (α ⟨x, ·⟩) (f t (α ⟨x, t⟩)) (Icc tmin tmax) t) ∧
ContinuousOn α (closedBall x₀ r ×ˢ Icc tmin tmax) :=
by
obtain ⟨α, hα1, L', hα2⟩ := hf.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith
refine ⟨uncurry α, hα1, ?_⟩
apply continuousOn_prod_of_continuousOn_lipschitzOnWith _ L' _ hα2
intro x hx t ht
exact (hα1 x hx).2 t ht |>.continuousWithinAt
