# Documentation

Mathlib.Topology.MetricSpace.Cauchy

## Cauchy sequences in (pseudo-)metric spaces #

Various results on Cauchy sequences in (pseudo-)metric spaces, including

• Metric.complete_of_cauchySeq_tendsto A pseudo-metric space is complete iff each Cauchy sequences converges to some limit point.
• cauchySeq_bdd: a Cauchy sequence on the natural numbers is bounded
• various characterisation of Cauchy and uniformly Cauchy sequences

## Tags #

metric, pseudo_metric, Cauchy sequence

theorem Metric.complete_of_convergent_controlled_sequences {α : Type u} (B : ) (hB : ∀ (n : ), 0 < B n) (H : ∀ (u : α), (∀ (N n m : ), N nN mdist (u n) (u m) < B N)∃ (x : α), Filter.Tendsto u Filter.atTop (nhds x)) :

A very useful criterion to show that a space is complete is to show that all sequences which satisfy a bound of the form dist (u n) (u m) < B N for all n m ≥ N are converging. This is often applied for B N = 2^{-N}, i.e., with a very fast convergence to 0, which makes it possible to use arguments of converging series, while this is impossible to do in general for arbitrary Cauchy sequences.

theorem Metric.complete_of_cauchySeq_tendsto {α : Type u} :
(∀ (u : α), ∃ (a : α), Filter.Tendsto u Filter.atTop (nhds a))

A pseudo-metric space is complete iff every Cauchy sequence converges.

theorem Metric.cauchySeq_iff {α : Type u} {β : Type v} [] [] {u : βα} :
ε > 0, ∃ (N : β), mN, nN, dist (u m) (u n) < ε

In a pseudometric space, Cauchy sequences are characterized by the fact that, eventually, the distance between its elements is arbitrarily small

theorem Metric.cauchySeq_iff' {α : Type u} {β : Type v} [] [] {u : βα} :
ε > 0, ∃ (N : β), nN, dist (u n) (u N) < ε

A variation around the pseudometric characterization of Cauchy sequences

theorem Metric.uniformCauchySeqOn_iff {α : Type u} {β : Type v} [] [] {γ : Type u_3} {F : βγα} {s : Set γ} :
UniformCauchySeqOn F Filter.atTop s ε > 0, ∃ (N : β), mN, nN, xs, dist (F m x) (F n x) < ε

In a pseudometric space, uniform Cauchy sequences are characterized by the fact that, eventually, the distance between all its elements is uniformly, arbitrarily small.

theorem cauchySeq_of_le_tendsto_0' {α : Type u} {β : Type v} [] [] {s : βα} (b : β) (h : ∀ (n m : β), n mdist (s n) (s m) b n) (h₀ : Filter.Tendsto b Filter.atTop (nhds 0)) :

If the distance between s n and s m, n ≤ m is bounded above by b n and b converges to zero, then s is a Cauchy sequence.

theorem cauchySeq_of_le_tendsto_0 {α : Type u} {β : Type v} [] [] {s : βα} (b : β) (h : ∀ (n m N : β), N nN mdist (s n) (s m) b N) (h₀ : Filter.Tendsto b Filter.atTop (nhds 0)) :

If the distance between s n and s m, n, m ≥ N is bounded above by b N and b converges to zero, then s is a Cauchy sequence.

theorem cauchySeq_bdd {α : Type u} {u : α} (hu : ) :
∃ R > 0, ∀ (m n : ), dist (u m) (u n) < R

A Cauchy sequence on the natural numbers is bounded.

theorem cauchySeq_iff_le_tendsto_0 {α : Type u} {s : α} :
∃ (b : ), (∀ (n : ), 0 b n) (∀ (n m N : ), N nN mdist (s n) (s m) b N) Filter.Tendsto b Filter.atTop (nhds 0)

Yet another metric characterization of Cauchy sequences on integers. This one is often the most efficient.