tendsto_iterate_efixedPoint — Mathlib

English

The iterates f^[n] x converge to efixedPoint f hf x hx as n → ∞.

Русский

Итерации f^[n] x сходятся к efixedPoint f hf x hx при n → ∞.

LaTeX

$$$ Tendsto (\lambda n, f^{[n]} x)\, atTop\, (\mathcal{N}\, efixedPoint\, f\, hf\, x\, hx) $$$

Lean4

theorem tendsto_iterate_efixedPoint (hf : ContractingWith K f) {x : α} (hx : edist x (f x) ≠ ∞) :
    Tendsto (fun n ↦ f^[n] x) atTop (𝓝 <| efixedPoint f hf x hx) :=
  (Classical.choose_spec <| hf.exists_fixedPoint x hx).2.1

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