aposteriori_dist_iterate_fixedPoint_le

English

A posteriori estimates bound the distance to the fixed point in terms of the gap between successive iterates: dist(f^[n]x, fixedPoint) ≤ dist(f^[n]x, f^[n+1]x) /(1 − K).

Русский

Апостериорная оценка ограничивает расстояние до фиксированной точки по зазору между соседними итерациями: d(f^n x, p) ≤ d(f^n x, f^{n+1}x)/(1−K).

LaTeX

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

Lean4

/-- A posteriori estimates on the convergence of iterates to the fixed point. -/
theorem aposteriori_dist_iterate_fixedPoint_le (x n) :
    dist (f^[n] x) (fixedPoint f hf) ≤ dist (f^[n] x) (f^[n + 1] x) / (1 - K) :=
  by
  rw [iterate_succ']
  apply hf.dist_fixedPoint_le

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