English
There exists a fixed point α of the operator next hf hx in the space of curves, i.e., a curve that is unchanged by one Picard iteration.
Русский
Существует неподвижная точка α оператора next hf hx в пространстве кривых, т.е. кривой, которая не изменяется после одного шага итерации Пикара.
LaTeX
$$$\\exists α:\\; IsFixedPt\\ (\\text{next } hf\\ hx)\\ α.$$$
Lean4
/-- The map `next` has a fixed point in the space of curves. This will be used to construct a
solution `α : ℝ → E` to the ODE. -/
theorem exists_isFixedPt_next [CompleteSpace E] (hf : IsPicardLindelof f t₀ x₀ a r L K) (hx : x ∈ closedBall x₀ r) :
∃ α : FunSpace t₀ x₀ r L, IsFixedPt (next hf hx) α :=
let ⟨_, _, h⟩ := exists_contractingWith_iterate_next hf
⟨_, h x hx |>.isFixedPt_fixedPoint_iterate⟩
