edist_iterate_succ_le_geometric — Mathlib

English

If f is K-Lipschitz, then for x and n, edist(f^[n] x, f^[n+1] x) ≤ edist(x, f x) · K^n.

Русский

Если f липшицево с константой K, то для любого x и n выполняется edist(f^[n] x, f^[n+1] x) ≤ edist(x, f x) · K^n.

LaTeX

$$$\\operatorname{edist}(f^{[n]} x, f^{[n+1]} x) \\le \\operatorname{edist}(x, f x) \\cdot K^n$$$

Lean4

theorem edist_iterate_succ_le_geometric {f : α → α} (hf : LipschitzWith K f) (x n) :
    edist (f^[n] x) (f^[n + 1] x) ≤ edist x (f x) * (K : ℝ≥0∞) ^ n :=
  by
  rw [iterate_succ, mul_comm]
  simpa only [ENNReal.coe_pow] using (hf.iterate n) x (f x)

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