English
The nth iterate of next is Lipschitz in the FunSpace metric, with a bound depending on n via a geometric series whose ratio involves max(tmax−t0, t0−tmin).
Русский
n-я итерация оператора next на линеет относительно метрики FunSpace: dist((next hf hx)^[n] α, (next hf hx)^[n] β) ≤ [K max( tmax−t0, t0−tmin) ]^n / n! · dist α,β, i.e., Lipschitz with a constant depending on n.
LaTeX
$$$\\forall E, f, t_{min}, t_{max}, t_0, x_0, a, r, L, K, hf, hx, α, β, n:\\quad\\n\\ dist((\\text{next } hf\\, hx)^{[n]}\\ α),((\\text{next } hf\\, hx)^{[n]}\\ β) \\le (K \\cdot |t_0-t|)^{n} / n! \\ dist(α,β).$$$
Lean4
/-- The `n`-th iterate of `next` is Lipschitz continuous with respect to `FunSpace`, with constant
$(K \max(t_{\mathrm{max}}, t_{\mathrm{min}})^n / n!$. -/
theorem dist_iterate_next_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] α) ((next hf hx)^[n] β) ≤ (K * max (tmax - t₀) (t₀ - tmin)) ^ n / n ! * dist α β :=
by
rw [← MetricSpace.isometry_induced FunSpace.toContinuousMap FunSpace.toContinuousMap.injective |>.dist_eq,
ContinuousMap.dist_le]
· intro t
apply le_trans <| dist_iterate_next_apply_le hf hx α β n t
gcongr
exact abs_sub_le_max_sub t.2.1 t.2.2 _
· have : 0 ≤ max (tmax - t₀) (t₀ - tmin) := le_max_of_le_left <| sub_nonneg_of_le t₀.2.2
positivity
