English
In an emetric space, a sequence (or net) is Cauchy iff there exists a nonincreasing function bounding pairwise edist.
Русский
В эметрическом пространстве последовательность Коши эквивалентна существованию функции, ограничивающей попарное edist.
LaTeX
$$$\text{CauchySeq } s \iff \exists b: β \to \mathbb{R}_{\ge 0}^{\infty}, (\forall n,m,N, N\le n\land N\le m \Rightarrow edist(s_n,s_m) \le b(N)) \land \text{Tendsto } b atTop (\mathcal{N} 0).$$$
Lean4
/-- Yet another metric characterization of Cauchy sequences on integers. This one is often the
most efficient. -/
theorem cauchySeq_iff_le_tendsto_0 [Nonempty β] [SemilatticeSup β] {s : β → α} :
CauchySeq s ↔ ∃ b : β → ℝ≥0∞, (∀ n m N : β, N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0) :=
EMetric.cauchySeq_iff.trans <| by
constructor
· intro hs
refine
⟨fun N => EMetric.diam (s '' Ici N), fun n m N hn hm => ?_, ?_⟩
-- Prove that it bounds the distances of points in the Cauchy sequence
·
exact
EMetric.edist_le_diam_of_mem (mem_image_of_mem _ hn)
(mem_image_of_mem _ hm)
-- Prove that it tends to `0`, by using the Cauchy property of `s`
· refine ENNReal.tendsto_nhds_zero.2 fun ε ε0 => ?_
rcases hs ε ε0 with ⟨N, hN⟩
refine (eventually_ge_atTop N).mono fun n hn => EMetric.diam_le ?_
rintro _ ⟨k, hk, rfl⟩ _ ⟨l, hl, rfl⟩
exact (hN _ (hn.trans hk) _ (hn.trans hl)).le
· rintro ⟨b, ⟨b_bound, b_lim⟩⟩ ε εpos
have : ∀ᶠ n in atTop, b n < ε := b_lim.eventually (gt_mem_nhds εpos)
rcases this.exists with ⟨N, hN⟩
refine ⟨N, fun m hm n hn => ?_⟩
calc
edist (s m) (s n) ≤ b N := b_bound m n N hm hn
_ < ε := hN
