English
There exist natural number n and nonnegative bound C such that the nth iterate of next is contracting with constant C, uniformly over all base points x in the closed ball of radius r around x0.
Русский
Существуют n ∈ ℕ и C ≥ 0 such that n-я итерация next является сжимающей с константой C, равномерно по всем базисным данным x внутри замкнутого шара вокруг x0.
LaTeX
$$$\\exists n\\in\\mathbb{N},\\exists C\\ge 0:\\forall x\\in\\overline{B}(x_0,r),\\text{ContractingWith } C\\ (\\text{next } hf\\, hx)^{[n]}.$$$
Lean4
/-- Some `n`-th iterate of `next` is a contracting map, and its associated Lipschitz constant is
independent of the initial point. -/
theorem exists_contractingWith_iterate_next (hf : IsPicardLindelof f t₀ x₀ a r L K) :
∃ (n : ℕ) (C : ℝ≥0), ∀ (x : E) (hx : x ∈ closedBall x₀ r), ContractingWith C (next hf hx)^[n] :=
by
obtain ⟨n, hn⟩ :=
FloorSemiring.tendsto_pow_div_factorial_atTop (K * max (tmax - t₀) (t₀ - tmin)) |>.eventually
(gt_mem_nhds zero_lt_one) |>.exists
have : (0 : ℝ) ≤ (K * max (tmax - t₀) (t₀ - tmin)) ^ n / n ! :=
by
have : 0 ≤ max (tmax - t₀) (t₀ - tmin) := le_max_of_le_left <| sub_nonneg_of_le t₀.2.2
positivity
refine ⟨n, ⟨_, this⟩, fun x hx ↦ ?_⟩
exact ⟨hn, LipschitzWith.of_dist_le_mul fun α β ↦ dist_iterate_next_iterate_next_le hf hx α β n⟩
