apriori_dist_iterate_fixedPoint_le

English

A priori estimates give a bound dist(f^[n]x, fixedPoint) ≤ dist x (f x) · K^n /(1 − K).

Русский

Априорная оценка: расстояние от n-й итерации до фиксированной точки не более dist(x,f(x))·K^n/(1−K).

LaTeX

$$$\\operatorname{edist}\\bigl(f^{[n]}(x), \\mathrm{fixedPoint}(f,hf)\\bigr) \\le \\operatorname{edist}(x, f x) \\cdot \\dfrac{K^{n}}{1 - K}.$$$

Lean4

theorem apriori_dist_iterate_fixedPoint_le (x n) :
    dist (f^[n] x) (fixedPoint f hf) ≤ dist x (f x) * (K : ℝ) ^ n / (1 - K) :=
  calc
    _ ≤ dist (f^[n] x) (f^[n + 1] x) / (1 - K) := hf.aposteriori_dist_iterate_fixedPoint_le x n
    _ ≤ _ := by gcongr; exacts [hf.one_sub_K_pos.le, hf.toLipschitzWith.dist_iterate_succ_le_geometric x n]

Похожие утверждения