English
Under the same hypotheses as the previous lemma, with n replaced by 0, the distance between x and the fixed point efixedPoint' is bounded by edist x (f x) divided by (1 − K).
Русский
При тех же предпосылках, если заменить n на 0, расстояние между x и фиксированной точкой efixedPoint' не превышает edist(x, f(x)) / (1 − K).
LaTeX
$$$\\operatorname{edist}\\bigl(x, \\mathrm{efixedPoint}'(f,hsc,hsf,hf,x,hxs,hx)\\bigr) \\le \\dfrac{\\operatorname{edist}(x,f(x))}{1 - K}.$$$
Lean4
theorem edist_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) ≠ ∞) :
edist x (efixedPoint' f hsc hsf hf x hxs hx) ≤ edist x (f x) / (1 - K) :=
by
convert hf.apriori_edist_iterate_efixedPoint_le' hsc hsf hxs hx 0
rw [pow_zero, mul_one]
