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} [PseudoMetricSpace α] (B : ℕ → ℝ) (hB : ∀ (n : ℕ), 0 < B n) (H : ∀ (u : ℕ → α), (∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < B N) → ∃ (x : α), Filter.Tendsto u Filter.atTop (nhds x)) : CompleteSpace α

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 : β), ∀ m ≥ N, ∀ n ≥ N, 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 : β), ∀ n ≥ N, 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 : β), ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, 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 ≤ m → dist (s n) (s m) ≤ b n) (h₀ : Filter.Tendsto b Filter.atTop (nhds 0)) : CauchySeq s

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 ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) (h₀ : Filter.Tendsto b Filter.atTop (nhds 0)) : CauchySeq s

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 ≤ n → N ≤ m → dist (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 n → dist (u m) (u (f n)) < b n