apriori_edist_iterate_efixedPoint_le

English

An a priori bound holds for the distance between iterates and the fixed point: edist(f^[n] x, efixedPoint) ≤ edist x f x · K^n /(1 − K).

Русский

Априорное ограничение на edist между итератом и фиксированной точкой: edist(f^[n] x, efixedPoint) ≤ edist x f x · K^n /(1 − K).

LaTeX

$$$ edist(f^{[n]} x, efixedPoint\, f\, hf\, x\, hx) \le edist(x, f(x)) \cdot K^n /(1 - K) $$$

Lean4

theorem apriori_edist_iterate_efixedPoint_le (hf : ContractingWith K f) {x : α} (hx : edist x (f x) ≠ ∞) (n : ℕ) :
    edist (f^[n] x) (efixedPoint f hf x hx) ≤ edist x (f x) * (K : ℝ≥0∞) ^ n / (1 - K) :=
  (Classical.choose_spec <| hf.exists_fixedPoint x hx).2.2 n

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