English
Let f be a Picard–Lindelöf vector field on a time interval [tmin,tmax] with center x0 and radius r, and let hx denote that x lies in the closed ball centered at x0 of radius r. For two curves α,β in the Picard–Lindelöf space and for any natural n and time t in the interval, if the distance between the nth iterates of next evaluated at t satisfies a geometric bound with factor (K|t−t0|)^n/n!, then after applying the map f at time t to those nth iterates the distance is bounded by K^{n+1}|t−t0|^n/n! times the original distance between α and β.
Русский
Пусть f удовлетворяет условиям теоремы Пикара–Линдельё проста на интервале времени [tmin,tmax], центр x0 и радиус r; hx означает x в шаре. Пусть α,β — две кривые из пространства FunSpace, n ∈ ℕ и t ∈ Icc(tmin,tmax). Если расстояние между n-митыми приложениями next к α и β удовлетворяет неравенству ≤ (K|t−t0|)^n/n! · dist(α,β), то после применения f в момент t к этим n-митым можем заключить, что dist(f(t, (next hf hx)^n α t), f(t, (next hf hx)^n β t)) ≤ K^{n+1}|t−t0|^n/n! · dist(α,β).
LaTeX
$$$\\forall E, f, t_{min}, t_{max}, t_0, x_0, a, r, L, K:\\quad \\text{(IsPicardLindelof } f\, t_0\, x_0\, a\, r\, L\, K) \\ \\Rightarrow \\\\ \\forall \\text{hx},\\ x\\in \\overline{B}(x_0,r),\\forall n\\in\\mathbb{N},\\forall t\\in Icc(t_{min},t_{max})\\\\\n\\ dist\\left((\\text{next } f x)^{[n]}\\alpha\\, t\\right),\\left((\\text{next } f x)^{[n]}\\beta\\, t\\right) \\le (K \\lvert t-t_0\\rvert)^n/n! \\cdot \\operatorname{dist}(\\alpha,\\beta) \\\\Rightarrow \\\\ dist\\left(f(t, (\\text{next } f x)^{[n]}\\alpha\\, t), f(t, (\\text{next } f x)^{[n]}\\beta\\, t)\\right) \\le K^{n+1} \\lvert t-t_0\\rvert^n / n! \\cdot \\operatorname{dist}(\\alpha,\\beta).$$$
Lean4
/-- A key step in the inductive case of `dist_iterate_next_apply_le` -/
theorem dist_comp_iterate_next_le (hf : IsPicardLindelof f t₀ x₀ a r L K) (hx : x ∈ closedBall x₀ r) (n : ℕ)
(t : Icc tmin tmax) {α β : FunSpace t₀ x₀ r L}
(h : dist ((next hf hx)^[n] α t) ((next hf hx)^[n] β t) ≤ (K * |t - t₀.1|) ^ n / n ! * dist α β) :
dist (f t ((next hf hx)^[n] α t)) (f t ((next hf hx)^[n] β t)) ≤ K ^ (n + 1) * |t - t₀.1| ^ n / n ! * dist α β :=
calc
_ ≤ K * dist ((next hf hx)^[n] α t) ((next hf hx)^[n] β t) :=
hf.lipschitzOnWith t.1 t.2 |>.dist_le_mul _ (FunSpace.mem_closedBall hf.mul_max_le) _
(FunSpace.mem_closedBall hf.mul_max_le)
_ ≤ K ^ (n + 1) * |t - t₀.1| ^ n / n ! * dist α β :=
by
rw [pow_succ', mul_assoc, mul_div_assoc, mul_assoc]
gcongr
rwa [← mul_pow]
