Mathlib.Topology.MetricSpace.Cauchy

Module docstring

{"## 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 "}

Metric.complete_of_convergent_controlled_sequences theorem

 (B : ℕ → Real) (hB : ∀ n, 0 < B n)
  (H : ∀ u : ℕ → α, (∀ N n m : ℕ, N ≤ n → N ≤ m → dist (u n) (u m) < B N) → ∃ x, Tendsto u atTop (𝓝 x)) :
  CompleteSpace α

Full source

/-- 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_convergent_controlled_sequences (B : ℕ → Real) (hB : ∀ n, 0 < B n)
    (H : ∀ u : ℕ → α, (∀ N n m : ℕ, N ≤ n → N ≤ m → dist (u n) (u m) < B N) →
      ∃ x, Tendsto u atTop (𝓝 x)) :
    CompleteSpace α :=
  UniformSpace.complete_of_convergent_controlled_sequences
    (fun n => { p : α × α | dist p.1 p.2 < B n }) (fun n => dist_mem_uniformity <| hB n) H

Completeness Criterion via Controlled Cauchy Sequences in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space and $(B_n)_{n \in \mathbb{N}}$ a sequence of positive real numbers. Suppose that for every sequence $(u_n)_{n \in \mathbb{N}}$ in $\alpha$ satisfying the controlled Cauchy condition \[ \forall N\ n\ m,\ N \leq n \land N \leq m \implies \text{dist}(u_n, u_m) < B_N, \] there exists a point $x \in \alpha$ such that $u_n$ converges to $x$ as $n \to \infty$. Then $\alpha$ is a complete pseudometric space.

Metric.complete_of_cauchySeq_tendsto theorem

: (∀ u : ℕ → α, CauchySeq u → ∃ a, Tendsto u atTop (𝓝 a)) → CompleteSpace α

Full source

/-- A pseudo-metric space is complete iff every Cauchy sequence converges. -/
theorem Metric.complete_of_cauchySeq_tendsto :
    (∀ u : ℕ → α, CauchySeq u → ∃ a, Tendsto u atTop (𝓝 a)) → CompleteSpace α :=
  EMetric.complete_of_cauchySeq_tendsto

Characterization of Complete Pseudometric Spaces via Cauchy Sequences

Informal description

A pseudometric space $\alpha$ is complete if and only if every Cauchy sequence in $\alpha$ converges to some limit point in $\alpha$. That is, for every sequence $u : \mathbb{N} \to \alpha$ that is Cauchy, there exists an element $a \in \alpha$ such that $u$ tends to $a$ in the topology induced by the pseudometric.

Metric.cauchySeq_iff theorem

{u : β → α} : CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε

Full source

/-- 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 {u : β → α} :
    CauchySeqCauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε :=
  uniformity_basis_dist.cauchySeq_iff

Characterization of Cauchy Sequences in Pseudometric Spaces via Distance

Informal description

Let $\alpha$ be a pseudometric space and $\beta$ a nonempty directed set (join-semilattice). A sequence $u : \beta \to \alpha$ is Cauchy if and only if for every $\varepsilon > 0$, there exists $N \in \beta$ such that for all $m, n \geq N$, the distance between $u(m)$ and $u(n)$ is less than $\varepsilon$, i.e., $\text{dist}(u(m), u(n)) < \varepsilon$.

Metric.cauchySeq_iff' theorem

{u : β → α} : CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) (u N) < ε

Full source

/-- A variation around the pseudometric characterization of Cauchy sequences -/
theorem Metric.cauchySeq_iff' {u : β → α} :
    CauchySeqCauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) (u N) < ε :=
  uniformity_basis_dist.cauchySeq_iff'

Characterization of Cauchy Sequences via Distance to a Fixed Term

Informal description

A sequence $u : \beta \to \alpha$ in a pseudometric space $\alpha$ is a Cauchy sequence if and only if for every $\varepsilon > 0$, there exists an index $N$ such that for all $n \geq N$, the distance between $u(n)$ and $u(N)$ is less than $\varepsilon$, i.e., $\text{dist}(u(n), u(N)) < \varepsilon$.

Metric.uniformCauchySeqOn_iff theorem

 {γ : Type*} {F : β → γ → α} {s : Set γ} :
  UniformCauchySeqOn F atTop s ↔ ∀ ε > (0 : ℝ), ∃ N : β, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε

Full source

/-- 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 Metric.uniformCauchySeqOn_iff {γ : Type*} {F : β → γ → α} {s : Set γ} :
    UniformCauchySeqOnUniformCauchySeqOn F atTop s ↔ ∀ ε > (0 : ℝ),
      ∃ N : β, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε := by
  constructor
  · intro h ε hε
    let u := { a : α × α | dist a.fst a.snd < ε }
    have hu : u ∈ 𝓤 α := Metric.mem_uniformity_dist.mpr ⟨ε, hε, by simp [u]⟩
    rw [← Filter.eventually_atTop_prod_self' (p := fun m =>
      ∀ x ∈ s, dist (F m.fst x) (F m.snd x) < ε)]
    specialize h u hu
    rw [prod_atTop_atTop_eq] at h
    exact h.mono fun n h x hx => h x hx
  · intro h u hu
    rcases Metric.mem_uniformity_dist.mp hu with ⟨ε, hε, hab⟩
    rcases h ε hε with ⟨N, hN⟩
    rw [prod_atTop_atTop_eq, eventually_atTop]
    use (N, N)
    intro b hb x hx
    rcases hb with ⟨hbl, hbr⟩
    exact hab (hN b.fst hbl.ge b.snd hbr.ge x hx)

Characterization of Uniformly Cauchy Sequences in Pseudometric Spaces via Distance

Informal description

Let $\alpha$ be a pseudometric space, $\beta$ a nonempty directed set (join-semilattice), $\gamma$ a type, and $F : \beta \to \gamma \to \alpha$ a sequence of functions. The sequence $F$ is uniformly Cauchy on a set $s \subseteq \gamma$ if and only if for every $\varepsilon > 0$, there exists $N \in \beta$ such that for all $m, n \geq N$ and all $x \in s$, the distance between $F_m(x)$ and $F_n(x)$ is less than $\varepsilon$, i.e., $\text{dist}(F_m(x), F_n(x)) < \varepsilon$.

cauchySeq_of_le_tendsto_0' theorem

 {s : β → α} (b : β → ℝ) (h : ∀ n m : β, n ≤ m → dist (s n) (s m) ≤ b n) (h₀ : Tendsto b atTop (𝓝 0)) : CauchySeq s

Full source

/-- 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' {s : β → α} (b : β → ℝ)
    (h : ∀ n m : β, n ≤ m → dist (s n) (s m) ≤ b n) (h₀ : Tendsto b atTop (𝓝 0)) : CauchySeq s :=
  Metric.cauchySeq_iff'.2 fun ε ε0 => (h₀.eventually (gt_mem_nhds ε0)).exists.imp fun N hN n hn =>
    calc dist (s n) (s N) = dist (s N) (s n) := dist_comm _ _
    _ ≤ b N := h _ _ hn
    _ < ε := hN

Cauchy Criterion via Dominating Sequence Tending to Zero

Informal description

Let $\alpha$ be a pseudometric space and $\beta$ a preorder. Given a sequence $s : \beta \to \alpha$ and a sequence $b : \beta \to \mathbb{R}$ such that: 1. For all $n, m \in \beta$ with $n \leq m$, the distance between $s(n)$ and $s(m)$ is bounded by $b(n)$, i.e., $\text{dist}(s(n), s(m)) \leq b(n)$. 2. The sequence $b$ tends to $0$ as $n$ tends to infinity. Then $s$ is a Cauchy sequence.

cauchySeq_of_le_tendsto_0 theorem

 {s : β → α} (b : β → ℝ) (h : ∀ n m N : β, N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) (h₀ : Tendsto b atTop (𝓝 0)) :
  CauchySeq s

Full source

/-- 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_of_le_tendsto_0 {s : β → α} (b : β → ℝ)
    (h : ∀ n m N : β, N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) (h₀ : Tendsto b atTop (𝓝 0)) :
    CauchySeq s :=
  cauchySeq_of_le_tendsto_0' b (fun _n _m hnm => h _ _ _ le_rfl hnm) h₀

Cauchy Criterion via Uniformly Dominating Sequence Tending to Zero

Informal description

Let $\alpha$ be a pseudometric space and $\beta$ a preorder. Given a sequence $s : \beta \to \alpha$ and a sequence $b : \beta \to \mathbb{R}$ such that: 1. For all $n, m, N \in \beta$ with $N \leq n$ and $N \leq m$, the distance between $s(n)$ and $s(m)$ is bounded by $b(N)$, i.e., $\text{dist}(s(n), s(m)) \leq b(N)$. 2. The sequence $b$ tends to $0$ as $n$ tends to infinity. Then $s$ is a Cauchy sequence.

cauchySeq_bdd theorem

{u : ℕ → α} (hu : CauchySeq u) : ∃ R > 0, ∀ m n, dist (u m) (u n) < R

Full source

/-- A Cauchy sequence on the natural numbers is bounded. -/
theorem cauchySeq_bdd {u : ℕ → α} (hu : CauchySeq u) : ∃ R > 0, ∀ m n, dist (u m) (u n) < R := by
  rcases Metric.cauchySeq_iff'.1 hu 1 zero_lt_one with ⟨N, hN⟩
  rsuffices ⟨R, R0, H⟩ : ∃ R > 0, ∀ n, dist (u n) (u N) < R
  · exact ⟨_, add_pos R0 R0, fun m n =>
      lt_of_le_of_lt (dist_triangle_right _ _ _) (add_lt_add (H m) (H n))⟩
  let R := Finset.sup (Finset.range N) fun n => nndist (u n) (u N)
  refine ⟨↑R + 1, add_pos_of_nonneg_of_pos R.2 zero_lt_one, fun n => ?_⟩
  rcases le_or_lt N n with h | h
  · exact lt_of_lt_of_le (hN _ h) (le_add_of_nonneg_left R.2)
  · have : _ ≤ R := Finset.le_sup (Finset.mem_range.2 h)
    exact lt_of_le_of_lt this (lt_add_of_pos_right _ zero_lt_one)

Boundedness of Cauchy Sequences in Pseudometric Spaces

Informal description

For any Cauchy sequence $u : \mathbb{N} \to \alpha$ in a pseudometric space $\alpha$, there exists a positive real number $R$ such that the distance between any two terms of the sequence is less than $R$, i.e., $\text{dist}(u(m), u(n)) < R$ for all $m, n \in \mathbb{N}$.

cauchySeq_iff_le_tendsto_0 theorem

 {s : ℕ → α} :
  CauchySeq s ↔
    ∃ b : ℕ → ℝ, (∀ n, 0 ≤ b n) ∧ (∀ n m N : ℕ, N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)

Full source

/-- Yet another metric characterization of Cauchy sequences on integers. This one is often the
most efficient. -/
theorem cauchySeq_iff_le_tendsto_0 {s : ℕ → α} :
    CauchySeqCauchySeq s ↔
      ∃ b : ℕ → ℝ,
        (∀ n, 0 ≤ b n) ∧
          (∀ n m N : ℕ, N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0) :=
  ⟨fun hs => by
    /- `s` is a Cauchy sequence. The sequence `b` will be constructed by taking
      the supremum of the distances between `s n` and `s m` for `n m ≥ N`.
      First, we prove that all these distances are bounded, as otherwise the Sup
      would not make sense. -/
    let S N := (fun p : ℕ × ℕ => dist (s p.1) (s p.2)) '' { p | p.1 ≥ N ∧ p.2 ≥ N }
    have hS : ∀ N, ∃ x, ∀ y ∈ S N, y ≤ x := by
      rcases cauchySeq_bdd hs with ⟨R, -, hR⟩
      refine fun N => ⟨R, ?_⟩
      rintro _ ⟨⟨m, n⟩, _, rfl⟩
      exact le_of_lt (hR m n)
    -- Prove that it bounds the distances of points in the Cauchy sequence
    have ub : ∀ m n N, N ≤ m → N ≤ n → dist (s m) (s n) ≤ sSup (S N) := fun m n N hm hn =>
      le_csSup (hS N) ⟨⟨_, _⟩, ⟨hm, hn⟩, rfl⟩
    have S0m : ∀ n, (0 : ℝ) ∈ S n := fun n => ⟨⟨n, n⟩, ⟨le_rfl, le_rfl⟩, dist_self _⟩
    have S0 := fun n => le_csSup (hS n) (S0m n)
    -- Prove that it tends to `0`, by using the Cauchy property of `s`
    refine ⟨fun N => sSup (S N), S0, ub, Metric.tendsto_atTop.2 fun ε ε0 => ?_⟩
    refine (Metric.cauchySeq_iff.1 hs (ε / 2) (half_pos ε0)).imp fun N hN n hn => ?_
    rw [Real.dist_0_eq_abs, abs_of_nonneg (S0 n)]
    refine lt_of_le_of_lt (csSup_le ⟨_, S0m _⟩ ?_) (half_lt_self ε0)
    rintro _ ⟨⟨m', n'⟩, ⟨hm', hn'⟩, rfl⟩
    exact le_of_lt (hN _ (le_trans hn hm') _ (le_trans hn hn')),
   fun ⟨b, _, b_bound, b_lim⟩ => cauchySeq_of_le_tendsto_0 b b_bound b_lim⟩

Characterization of Cauchy Sequences via Dominating Sequence Tending to Zero

Informal description

A sequence $s : \mathbb{N} \to \alpha$ in a pseudometric space $\alpha$ is Cauchy if and only if there exists a nonnegative real-valued sequence $b : \mathbb{N} \to \mathbb{R}$ such that: 1. For all $n, m, N \in \mathbb{N}$ with $N \leq n$ and $N \leq m$, the distance between $s(n)$ and $s(m)$ is bounded by $b(N)$, i.e., $\text{dist}(s(n), s(m)) \leq b(N)$. 2. The sequence $b$ tends to $0$ as $n$ tends to infinity.

Metric.exists_subseq_bounded_of_cauchySeq theorem

 (u : ℕ → α) (hu : CauchySeq u) (b : ℕ → ℝ) (hb : ∀ n, 0 < b n) :
  ∃ f : ℕ → ℕ, StrictMono f ∧ ∀ n, ∀ m ≥ f n, dist (u m) (u (f n)) < b n

Full source

lemma Metric.exists_subseq_bounded_of_cauchySeq (u : ℕ → α) (hu : CauchySeq u) (b : ℕ → ℝ)
    (hb : ∀ n, 0 < b n) :
    ∃ f : ℕ → ℕ, StrictMono f ∧ ∀ n, ∀ m ≥ f n, dist (u m) (u (f n)) < b n := by
  rw [cauchySeq_iff] at hu
  have hu' : ∀ k, ∀ᶠ (n : ℕ) in atTop, ∀ m ≥ n, dist (u m) (u n) < b k := by
    intro k
    rw [eventually_atTop]
    obtain ⟨N, hN⟩ := hu (b k) (hb k)
    exact ⟨N, fun m hm r hr => hN r (hm.trans hr) m hm⟩
  exact Filter.extraction_forall_of_eventually hu'

Existence of Subsequence with Bounded Distances for Cauchy Sequences in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space, $u : \mathbb{N} \to \alpha$ a Cauchy sequence, and $b : \mathbb{N} \to \mathbb{R}$ a sequence of positive real numbers. Then there exists a strictly increasing function $f : \mathbb{N} \to \mathbb{N}$ such that for all $n \in \mathbb{N}$ and all $m \geq f(n)$, the distance between $u(m)$ and $u(f(n))$ is less than $b(n)$, i.e., $\text{dist}(u(m), u(f(n))) < b(n)$.