English
For two curves α,β in FunSpace and any n≥0, the distance between their nth iterates under the operator next is bounded by a geometric term depending on the time displacement: dist((next hf hx)^[n] α t, (next hf hx)^[n] β t) ≤ (K|t−t0|)^n / n! · dist αβ.
Русский
Для двух кривых α,β в пространстве FunSpace при любом n≥0 расстояние между их n-ой итерацией применения оператора next ограничено геометрически: dist((next hf hx)^[n] α t, (next hf hx)^[n] β t) ≤ (K|t−t0|)^n / n! · dist αβ.
LaTeX
$$$\\forall E, [\\text{NormedSpace}], f, t_{min}, t_{max}, t\\_0, x_0, a, r, L, K, hf, hx, α, β, n, t:\\quad\\n\\ dist((\\text{next } hf\\, hx)^{[n]}\\ α\\ t),((\\text{next } hf\\, hx)^{[n]}\\ β\\ t)\\le (K \\cdot |t-t_0|)^n / n! \\cdot dist(α,β).$$$
Lean4
/-- A time-dependent bound on the distance between the `n`-th iterates of `next` on two curves -/
theorem dist_iterate_next_apply_le (hf : IsPicardLindelof f t₀ x₀ a r L K) (hx : x ∈ closedBall x₀ r)
(α β : FunSpace t₀ x₀ r L) (n : ℕ) (t : Icc tmin tmax) :
dist ((next hf hx)^[n] α t) ((next hf hx)^[n] β t) ≤ (K * |t.1 - t₀.1|) ^ n / n ! * dist α β := by
induction n generalizing t with
| zero => simpa using ContinuousMap.dist_apply_le_dist (f := toContinuousMap α) (g := toContinuousMap β) _
| succ n
hn =>
rw [iterate_succ_apply', iterate_succ_apply', dist_eq_norm, next_apply, next_apply, picard_apply, picard_apply,
add_sub_add_left_eq_sub, ←
intervalIntegral.integral_sub (intervalIntegrable_comp_compProj hf _ t) (intervalIntegrable_comp_compProj hf _ t)]
calc
_ ≤ ∫ τ in uIoc t₀.1 t.1, K ^ (n + 1) * |τ - t₀| ^ n / n ! * dist α β :=
by
rw [intervalIntegral.norm_intervalIntegral_eq]
apply MeasureTheory.norm_integral_le_of_norm_le (Continuous.integrableOn_uIoc (by fun_prop))
apply ae_restrict_mem measurableSet_Ioc |>.mono
intro t' ht'
have ht' : t' ∈ Icc tmin tmax := subset_trans uIoc_subset_uIcc (uIcc_subset_Icc t₀.2 t.2) ht'
rw [← dist_eq_norm, compProj_of_mem, compProj_of_mem]
exact dist_comp_iterate_next_le hf hx _ ⟨t', ht'⟩ (hn _)
_ ≤ (K * |t.1 - t₀.1|) ^ (n + 1) / (n + 1)! * dist α β :=
by
apply le_of_abs_le
rw [← intervalIntegral.abs_intervalIntegral_eq, intervalIntegral.integral_mul_const,
intervalIntegral.integral_div, intervalIntegral.integral_const_mul, abs_mul, abs_div, abs_mul,
intervalIntegral.abs_intervalIntegral_eq, integral_pow_abs_sub_uIoc, abs_div, abs_pow, abs_pow, abs_dist,
NNReal.abs_eq, abs_abs, mul_div, div_div, ← abs_mul, ← Nat.cast_succ, ← Nat.cast_mul, ← Nat.factorial_succ,
Nat.abs_cast, ← mul_pow]
