English
There exists a curve α with α(t0) = x and HasDerivWithinAt α(t) = f(t, α(t)) for all t in Icc(tmin,tmax).
Русский
Существует кривая α с α(t0)=x и HasDerivWithinAt α(t) = f(t, α(t)) на Icc(tmin,tmax).
LaTeX
$$$\\exists α:\\; α(t_0) = x \\land \\forall t\\in Icc(t_{min},t_{max}),\\ HasDerivWithinAt\\ α(t)\\ (f(t, α(t))).$$$
Lean4
/-- **Picard-Lindelöf (Cauchy-Lipschitz) theorem**, differential form. This version shows the
existence of a local solution whose initial point `x` may be different from the centre `x₀` of
the closed ball within which the properties of the vector field hold. -/
theorem exists_eq_forall_mem_Icc_hasDerivWithinAt (hf : IsPicardLindelof f t₀ x₀ a r L K) (hx : x ∈ closedBall x₀ r) :
∃ α : ℝ → E, α t₀ = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t :=
by
obtain ⟨α, hα⟩ := FunSpace.exists_isFixedPt_next hf hx
refine ⟨α.compProj, by rw [FunSpace.compProj_val, ← hα, FunSpace.next_apply₀], fun t ht ↦ ?_⟩
apply
hasDerivWithinAt_picard_Icc t₀.2 hf.continuousOn_uncurry α.continuous_compProj.continuousOn
(fun _ ht' ↦ α.compProj_mem_closedBall hf.mul_max_le) x ht |>.congr_of_mem
_ ht
intro t' ht'
nth_rw 1 [← hα]
rw [FunSpace.compProj_of_mem ht', FunSpace.next_apply]
