English
For a Cauchy sequence u: ℕ → α, there exists a strictly increasing f: ℕ → ℕ such that the series ∑ dist(u(f(i+1)), u(f(i))) is summable.
Русский
Для-кючевой последовательности u: ℕ → α существует строго возрастающая подпоследовательность f, такая что сумма расстояний ∑ dist(u(f(i+1)), u(f(i))) сходится.
LaTeX
$$$\exists f: \mathbb{N} \to \mathbb{N}, \text{StrictMono}(f) \wedge \text{Summable}\Bigl( \lambda i. \mathrm{dist}\bigl(u(f(i+1)), u(f(i))\bigr)\Bigr)$$$
Lean4
theorem exists_subseq_summable_dist_of_cauchySeq (u : ℕ → α) (hu : CauchySeq u) :
∃ f : ℕ → ℕ, StrictMono f ∧ Summable fun i => dist (u (f (i + 1))) (u (f i)) :=
by
obtain ⟨f, hf₁, hf₂⟩ :=
Metric.exists_subseq_bounded_of_cauchySeq u hu (fun n => (1 / (2 : ℝ)) ^ n) (fun n => by positivity)
refine ⟨f, hf₁, ?_⟩
refine Summable.of_nonneg_of_le (fun n => by positivity) ?_ summable_geometric_two
exact fun n => le_of_lt <| hf₂ n (f (n + 1)) <| hf₁.monotone (Nat.le_add_right n 1)
