English
If the distances between successive terms are bounded by a summable sequence, then the sequence is Cauchy.
Русский
Если расстояния между соседними члены последовательности ограничены суммируемой последовательностью, то последовательность является Cauchy.
LaTeX
$$$$\\text{If } d: \\mathbb{N} \\to \\mathbb{R} \\text{ with } \\forall n,\\ dist(f(n), f(n+1)) \\le d(n),\\; \\sum d(n) < \\infty, \\text{ then } f \\text{ is Cauchy}. $$$$
Lean4
/-- If the distance between consecutive points of a sequence is estimated by a summable series,
then the original sequence is a Cauchy sequence. -/
theorem cauchySeq_of_dist_le_of_summable (d : ℕ → ℝ) (hf : ∀ n, dist (f n) (f n.succ) ≤ d n) (hd : Summable d) :
CauchySeq f := by
lift d to ℕ → ℝ≥0 using fun n ↦ dist_nonneg.trans (hf n)
apply cauchySeq_of_edist_le_of_summable d (α := α) (f := f)
· exact_mod_cast hf
· exact_mod_cast hd
