Documentation

Mathlib.Topology.MetricSpace.Cauchy

Cauchy sequences in (pseudo-)metric spaces #

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

Tags #

metric, pseudo_metric, Cauchy sequence

theorem Metric.complete_of_convergent_controlled_sequences {α : Type u} [PseudoMetricSpace α] (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} [PseudoMetricSpace α] :
(∀ (u : α), CauchySeq u∃ (a : α), Filter.Tendsto u Filter.atTop (nhds a))CompleteSpace α

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

theorem Metric.cauchySeq_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [Nonempty β] [SemilatticeSup β] {u : βα} :
CauchySeq 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} [PseudoMetricSpace α] [Nonempty β] [SemilatticeSup β] {u : βα} :
CauchySeq 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} [PseudoMetricSpace α] [Nonempty β] [SemilatticeSup β] {γ : 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} [PseudoMetricSpace α] [Nonempty β] [SemilatticeSup β] {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} [PseudoMetricSpace α] [Nonempty β] [SemilatticeSup β] {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} [PseudoMetricSpace α] {u : α} (hu : CauchySeq u) :
∃ 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} [PseudoMetricSpace α] {s : α} :
CauchySeq 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.

theorem Metric.exists_subseq_bounded_of_cauchySeq {α : Type u} [PseudoMetricSpace α] (u : α) (hu : CauchySeq u) (b : ) (hb : ∀ (n : ), 0 < b n) :
∃ (f : ), StrictMono f ∀ (n m : ), m f ndist (u m) (u (f n)) < b n