English
There exists a fixed “flow” α: time → E solving the integral Picard equation: α(t) = picard f t0 x α(t), with α(t0) = x for any initial x in the closed ball.
Русский
Существует решение кривой α, удовлетворяющее интегральному уравнению Пикара–Линдельоф: α(t) = picard f t0 x α(t), причём α(t0)=x для каждого начального x в шаре.
LaTeX
$$$\\exists α:\\; α = (\\text{picard } f\\ t_0\\ x)\\circ α$, и для всех t в Icc(t_min,t_max) выполняется α(t) = picard f t0 x α(t).$$
Lean4
/-- **Picard-Lindelöf (Cauchy-Lipschitz) theorem**, integral 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_eq_picard (hf : IsPicardLindelof f t₀ x₀ a r L K) (hx : x ∈ closedBall x₀ r) :
∃ α : ℝ → E, α t₀ = x ∧ ∀ t ∈ Icc tmin tmax, α t = ODE.picard f t₀ x α t :=
by
obtain ⟨α, hα⟩ := FunSpace.exists_isFixedPt_next hf hx
refine ⟨(FunSpace.next hf hx α).compProj, by simp, fun t ht ↦ ?_⟩
rw [FunSpace.compProj_apply, FunSpace.next_apply, hα, projIcc_of_mem _ ht]
