dist_le_tsum_dist_of_tendsto — Mathlib

English

For any n, the distance from f(n) to a is bounded by the tail sum of the distances between successive terms.

Русский

Для любого n расстояние между f(n) и a не превышает хвостовую сумму расстояний между соседними членами.

LaTeX

$$$$\\operatorname{dist}(f(n), a) \\le \\sum_{m=0}^{\\infty} \\operatorname{dist}(f(n+m), f(n+m+1)).$$$$

Lean4

theorem dist_le_tsum_dist_of_tendsto (h : Summable fun n ↦ dist (f n) (f n.succ)) (ha : Tendsto f atTop (𝓝 a)) (n) :
    dist (f n) a ≤ ∑' m, dist (f (n + m)) (f (n + m).succ) :=
  show dist (f n) a ≤ ∑' m, (fun x ↦ dist (f x) (f x.succ)) (n + m) from
    dist_le_tsum_of_dist_le_of_tendsto (fun n ↦ dist (f n) (f n.succ)) (fun _ ↦ le_rfl) h ha n

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