English
If the tail distances bound by a summable d(n) and f tends to a, then dist(f(n), a) is bounded by the tail sum of d.
Русский
Если хвостовые расстояния ограничены суммируемой последовательностью d(n) и f(n) стремится к a, то dist(f(n), a) ограничено хвостовой суммой d.
LaTeX
$$$$\\operatorname{dist}(f(n), a) \\le \\sum_{m=0}^{\\infty} d(n+m).$$$$
Lean4
theorem dist_le_tsum_of_dist_le_of_tendsto (d : ℕ → ℝ) (hf : ∀ n, dist (f n) (f n.succ) ≤ d n) (hd : Summable d) {a : α}
(ha : Tendsto f atTop (𝓝 a)) (n : ℕ) : dist (f n) a ≤ ∑' m, d (n + m) :=
by
refine le_of_tendsto (tendsto_const_nhds.dist ha) (eventually_atTop.2 ⟨n, fun m hnm ↦ ?_⟩)
refine le_trans (dist_le_Ico_sum_of_dist_le hnm fun _ _ ↦ hf _) ?_
rw [sum_Ico_eq_sum_range]
refine Summable.sum_le_tsum (range _) (fun _ _ ↦ le_trans dist_nonneg (hf _)) ?_
exact hd.comp_injective (add_right_injective n)
