English
The distance between α and the nth iterate of next is bounded by the finite sum of a geometric series in K and a finite sum in the iterated Lipschitz constant, times the distance between α and the next α.
Русский
Расстояние между α и n-й итерацией next ограничено суммой геометрического типа и суммой умножений константы Липшитца, умноженной на dist(α, next α).
LaTeX
$$$\\forall α,hf,hx,m,n:\\quad \\operatorname{dist}\\big(\\ α, (\\text{next hf hx})^{[m]}^{[n]} α\\big) ≤ \\Big(\\sum_{i=0}^{m-1} (K\\max(t_{max}-t_0,t_0-t_{min}))^i/i!\\Big) \\Big(\\sum_{i=0}^{n-1} C^i\\Big) \\operatorname{dist}(α,(\\text{next hf hx}) α).$$$
Lean4
/-- The pointwise distance between any two integral curves `α` and `β` over their domains is bounded
by a constant `L'` times the distance between their respective initial points. This is the result of
taking the limit of `dist_iterate_iterate_next_le_of_lipschitzWith` as `n → ∞`. This implies that
the local solution of a vector field is Lipschitz continuous in the initial condition. -/
theorem exists_forall_closedBall_funSpace_dist_le_mul [CompleteSpace E] (hf : IsPicardLindelof f t₀ x₀ a r L K) :
∃ L' : ℝ≥0,
∀ (x y : E) (hx : x ∈ closedBall x₀ r) (hy : y ∈ closedBall x₀ r) (α β : FunSpace t₀ x₀ r L)
(_ : IsFixedPt (next hf hx) α) (_ : IsFixedPt (next hf hy) β), dist α β ≤ L' * dist x y :=
by
obtain ⟨m, C, h⟩ := exists_contractingWith_iterate_next hf
let L' := (∑ i ∈ Finset.range m, (K * max (tmax - t₀) (t₀ - tmin)) ^ i / i !) * (1 - C)⁻¹
have hL' : 0 ≤ L' :=
by
have : 0 ≤ max (tmax - t₀) (t₀ - tmin) := le_max_of_le_left <| sub_nonneg_of_le t₀.2.2
positivity
refine ⟨⟨L', hL'⟩, fun x y hx hy α β hα hβ ↦ ?_⟩
rw [NNReal.coe_mk]
apply
le_of_tendsto_of_tendsto' (b := Filter.atTop) _ _ <|
dist_iterate_iterate_next_le_of_lipschitzWith hf hy α (h y hy).2
· apply Filter.Tendsto.comp (y := 𝓝 β) (tendsto_const_nhds.dist Filter.tendsto_id)
rw [h y hy |>.fixedPoint_unique (hβ.iterate m)]
exact h y hy |>.tendsto_iterate_fixedPoint α
· nth_rw 1 [← hα, dist_next_next]
apply Filter.Tendsto.mul_const
apply Filter.Tendsto.const_mul
convert hasSum_geometric_of_lt_one C.2 (h y hy).1 |>.tendsto_sum_nat
simp [NNReal.coe_sub <| le_of_lt (h y hy).1, NNReal.coe_one]
