dist_iterate_succ_le_geometric — Mathlib

English

If f is K-Lipschitz, then the distance between the n-th and (n+1)-th iterate of x is bounded by dist(x, f(x)) times K^n.

Русский

Если f — Lipschitz с константой K, то dist(f^n(x), f^{n+1}(x)) ≤ dist(x, f(x))·K^n.

LaTeX

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

Lean4

theorem dist_iterate_succ_le_geometric {f : α → α} (hf : LipschitzWith K f) (x n) :
    dist (f^[n] x) (f^[n + 1] x) ≤ dist x (f x) * (K : ℝ) ^ n :=
  by
  rw [iterate_succ, mul_comm]
  simpa only [NNReal.coe_pow] using (hf.iterate n).dist_le_mul x (f x)

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