English
Let S be a complete forward-invariant subset under f with contraction constant K, and x ∈ S with hx: edist x (f x) ≠ ∞. Then for every n ∈ ℕ, the distance between f^[n] x and the fixed point efixedPoint'(f,…) is bounded by edist x (f x) · K^n / (1 − K).
Русский
Пусть S — полное впередInvariant подмножество, на котором действует сжатие f с константой K, и x ∈ S такое, что edist(x, f(x)) конечна. Тогда для каждого n ∈ ℕ расстояние между f^[n] x и фиксированной точкой efixedPoint'(f,…) ограничено выражением edist(x, f(x)) · K^n / (1 − K).
LaTeX
$$$\\operatorname{edist}\\bigl(f^{[n]}(x), \\mathrm{efixedPoint}'(f,hsc,hsf,hf,x,hxs,hx)\\bigr) \\\\le \\operatorname{edist}(x,f(x)) \\cdot \\dfrac{K^{n}}{1-K}.$$$
Lean4
theorem apriori_edist_iterate_efixedPoint_le' {s : Set α} (hsc : IsComplete s) (hsf : MapsTo f s s)
(hf : ContractingWith K <| hsf.restrict f s s) {x : α} (hxs : x ∈ s) (hx : edist x (f x) ≠ ∞) (n : ℕ) :
edist (f^[n] x) (efixedPoint' f hsc hsf hf x hxs hx) ≤ edist x (f x) * (K : ℝ≥0∞) ^ n / (1 - K) :=
(Classical.choose_spec <| hf.exists_fixedPoint' hsc hsf hxs hx).2.2.2 n
