English
If the m-th iterate has Lipschitz constant C, then the distance between the m-th iterate and the n-th iterate is bounded by the product of a partial geometric sum (from m) and a geometric sum in C times the distance between α and next α.
Русский
Если m-я итерация имеет Lipschitz константу C, то расстояние между m-й и n-й итерациями ограничено произведением частной геометрической суммы и геометрической суммы в C на расстояние между α и next α.
LaTeX
$$$\\forall α, hf, hx, m, C, n:\\quad \\operatorname{dist}\\big(\\alpha, (\\text{next } hf\\ hx)^{[m]}^{[n]} \\alpha\\big) \\le \\Big(\\sum_{i=0}^{m-1} \\frac{(K\\max(t_{max}-t_0,t_0-t_{min}))^i}{i!}\\Big) \\Big(\\sum_{i=0}^{n-1} C^i\\Big) \\operatorname{dist}\\big(\\alpha, (\\text{next } hf\\ hx) \\alpha\\big).$$$
Lean4
theorem dist_iterate_iterate_next_le_of_lipschitzWith (hf : IsPicardLindelof f t₀ x₀ a r L K) (hx : x ∈ closedBall x₀ r)
(α : FunSpace t₀ x₀ r L) {m : ℕ} {C : ℝ≥0} (hm : LipschitzWith C (next hf hx)^[m]) (n : ℕ) :
dist α ((next hf hx)^[m]^[n] α) ≤
(∑ i ∈ Finset.range m, (K * max (tmax - t₀) (t₀ - tmin)) ^ i / i !) * (∑ i ∈ Finset.range n, (C : ℝ) ^ i) *
dist α (next hf hx α) :=
by
nth_rw 1 [← iterate_zero_apply (next hf hx) α]
rw [Finset.mul_sum, Finset.sum_mul]
apply dist_le_range_sum_of_dist_le (f := fun i ↦ (next hf hx)^[m]^[i] α)
intro i hi
rw [iterate_succ_apply]
apply le_trans <| hm.dist_iterate_succ_le_geometric α i
rw [mul_assoc, mul_comm ((C : ℝ) ^ i), ← mul_assoc]
gcongr
exact dist_iterate_next_le hf hx α m
