English
Distance between a curve α and its nth iterate under next is controlled by the sum of a finite geometric-type series in the distance between α and next α.
Русский
Расстояние между кривой α и её n-й итерацией под next ограничено суммой конечного ряда, зависящего от dist(α, next α).
LaTeX
$$$\\operatorname{dist}\\big(\\alpha, (\\text{next } hf\\ hx)^{[n]} \\alpha\\big) \\le \\Big(\\sum_{i=0}^{n-1} \\frac{(K \\max(t_{max}-t_0, t_0-t_{min}))^i}{i!}\\Big) \\operatorname{dist}\\big(\\alpha, (\\text{next } hf\\ hx) \\alpha\\big).$$$
Lean4
theorem dist_iterate_next_le (hf : IsPicardLindelof f t₀ x₀ a r L K) (hx : x ∈ 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 !) * dist α (next hf hx α) :=
by
nth_rw 1 [← iterate_zero_apply (next hf hx) α]
rw [Finset.sum_mul]
apply dist_le_range_sum_of_dist_le (f := fun i ↦ (next hf hx)^[i] α)
intro i hi
rw [iterate_succ_apply]
exact dist_iterate_next_iterate_next_le hf hx _ _ i
