English
If the distance between successive terms of a sequence is bounded above by a nonnegative extended real sequence d, and the sequence tends to a, then for every n, the distance from f(n) to a is bounded by the tail sum ∑_{m≥n} d(m).
Русский
Если расстояние между соседними членами последовательности не превышает неположительное вещественное число в бесконечно больших результатах, и последовательность стремится к a, то для каждого n расстояние от f(n) до a не превышает хвостовую сумму по m≥n.
LaTeX
$$$\text{edist}(f(n), a) \leq \sum_{m \ge n} d(m)$$$
Lean4
/-- If `edist (f n) (f (n+1))` is bounded above by a function `d : ℕ → ℝ≥0∞`,
then the distance from `f n` to the limit is bounded by `∑'_{k=n}^∞ d k`. -/
theorem edist_le_tsum_of_edist_le_of_tendsto {f : ℕ → α} (d : ℕ → ℝ≥0∞) (hf : ∀ n, edist (f n) (f n.succ) ≤ d n) {a : α}
(ha : Tendsto f atTop (𝓝 a)) (n : ℕ) : edist (f n) a ≤ ∑' m, d (n + m) :=
by
refine le_of_tendsto (tendsto_const_nhds.edist ha) (mem_atTop_sets.2 ⟨n, fun m hnm => ?_⟩)
change edist _ _ ≤ _
refine le_trans (edist_le_Ico_sum_of_edist_le hnm fun _ _ => hf _) ?_
rw [Finset.sum_Ico_eq_sum_range]
exact ENNReal.summable.sum_le_tsum _ (fun _ _ => zero_le _)
