cauchySeq_iff_le_tendsto_0 — Mathlib

English

A Cauchy sequence on ℕ is equivalent to the existence of a bound b(n) with b(n)≥0 and a decay condition dist(s_n,s_m) ≤ b(N) for N≤n,m, together with Tendsto b atTop to 0.

Русский

Последовательность Коши на ℕ эквивалентна существованию функции-границы b(n)≥0 и схождения dist(s_n,s_m) ≤ b(N) при N≤n,m, вместе с Tendsto b к 0.

LaTeX

$$$\\displaystyle \\text{CauchySeq}(s) \\iff \\exists b: \\mathbb{N} \\to \\mathbb{R},\\; \\forall n, 0\\le b(n)\\land\\,\\big( \\forall n,m, N,\\ N\\le n,\\ N\\le m\\Rightarrow \\operatorname{dist}(s_n,s_m) \\le b(N) \\big) \\land \\text{Tendsto } b \\text{ 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 {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) :=
  ⟨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⟩

Похожие утверждения