Analysis
5.2. Equivalent Cauchy sequences

Imports

import Mathlib.Tactic
import Analysis.Section_5_1

Analysis I, Section 5.2: Equivalent Cauchy sequences

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

Notion of an ε-close and eventually ε-close sequences of rationals.
Notion of an equivalent Cauchy sequence of rationals.

Tips from past users

Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.

(Add tip here)

              abbrev Rat.CloseSeq (ε: ℚ) (a b: Chapter5.Sequence) : Prop :=
  ∀ n, n ≥ a.n₀ → n ≥ b.n₀ → ε.Close (a n) (b n)abbrev Rat.EventuallyClose (ε: ℚ) (a b: Chapter5.Sequence) : Prop :=
  ∃ N, ε.CloseSeq (a.from N) (b.from N)namespace Chapter5

Definition 5.2.1 ($ε$-close sequences)

lemma Rat.closeSeq_def (ε: ℚ) (a b: Sequence) :
    ε.CloseSeq a b ↔ ∀ n, n ≥ a.n₀ → n ≥ b.n₀ → ε.Close (a n) (b n) := byε:ℚa:Sequenceb:Sequence⊢ ε.CloseSeq a b ↔ ∀ n ≥ a.n₀, n ≥ b.n₀ → ε.Close (a.seq n) (b.seq n) rflAll goals completed! 🐙

              /-- Example 5.2.2 -/
declaration uses `sorry`example : (0.1:ℚ).CloseSeq ((fun n:ℕ ↦ ((-1)^n:ℚ)):Sequence)
((fun n:ℕ ↦ ((1.1:ℚ) * (-1)^n)):Sequence) := by⊢ Rat.CloseSeq 0.1 (↑fun n ↦ (-1) ^ n) ↑fun n ↦ 1.1 * (-1) ^ n sorryAll goals completed! 🐙/-- Example 5.2.2 -/
declaration uses `sorry`example : ¬ (0.1:ℚ).Steady ((fun n:ℕ ↦ ((-1)^n:ℚ)):Sequence) := by⊢ ¬Rat.Steady 0.1 ↑fun n ↦ (-1) ^ n sorryAll goals completed! 🐙/-- Example 5.2.2 -/
declaration uses `sorry`example : ¬ (0.1:ℚ).Steady ((fun n:ℕ ↦ ((1.1:ℚ) * (-1)^n)):Sequence) := by⊢ ¬Rat.Steady 0.1 ↑fun n ↦ 1.1 * (-1) ^ n sorryAll goals completed! 🐙

Definition 5.2.3 (Eventually ε-close sequences)

lemma Rat.eventuallyClose_def (ε: ℚ) (a b: Sequence) :
    ε.EventuallyClose a b ↔ ∃ N, ε.CloseSeq (a.from N) (b.from N) := byε:ℚa:Sequenceb:Sequence⊢ ε.EventuallyClose a b ↔ ∃ N, ε.CloseSeq (a.from N) (b.from N) rflAll goals completed! 🐙

Definition 5.2.3 (Eventually ε-close sequences)

lemma declaration uses `sorry`Rat.eventuallyClose_iff (ε: ℚ) (a b: ℕ → ℚ) :
    ε.EventuallyClose (a:Sequence) (b:Sequence) ↔ ∃ N, ∀ n ≥ N, |a n - b n| ≤ ε := byε:ℚa:ℕ → ℚb:ℕ → ℚ⊢ ε.EventuallyClose ↑a ↑b ↔ ∃ N, ∀ n ≥ N, |a n - b n| ≤ ε sorryAll goals completed! 🐙

              /-- Example 5.2.5 -/
declaration uses `sorry`example : ¬ (0.1:ℚ).CloseSeq ((fun n:ℕ ↦ (1:ℚ)+10^(-(n:ℤ)-1)):Sequence)
  ((fun n:ℕ ↦ (1:ℚ)-10^(-(n:ℤ)-1)):Sequence) := by⊢ ¬Rat.CloseSeq 0.1 (↑fun n ↦ 1 + 10 ^ (-↑n - 1)) ↑fun n ↦ 1 - 10 ^ (-↑n - 1) sorryAll goals completed! 🐙declaration uses `sorry`example : (0.1:ℚ).EventuallyClose ((fun n:ℕ ↦ (1:ℚ)+10^(-(n:ℤ)-1)):Sequence)
  ((fun n:ℕ ↦ (1:ℚ)-10^(-(n:ℤ)-1)):Sequence) := by⊢ Rat.EventuallyClose 0.1 (↑fun n ↦ 1 + 10 ^ (-↑n - 1)) ↑fun n ↦ 1 - 10 ^ (-↑n - 1) sorryAll goals completed! 🐙declaration uses `sorry`example : (0.01:ℚ).EventuallyClose ((fun n:ℕ ↦ (1:ℚ)+10^(-(n:ℤ)-1)):Sequence)
  ((fun n:ℕ ↦ (1:ℚ)-10^(-(n:ℤ)-1)):Sequence) := by⊢ Rat.EventuallyClose 1e-2 (↑fun n ↦ 1 + 10 ^ (-↑n - 1)) ↑fun n ↦ 1 - 10 ^ (-↑n - 1) sorryAll goals completed! 🐙

Definition 5.2.6 (Equivalent sequences)

abbrev Sequence.Equiv (a b: ℕ → ℚ) : Prop :=
  ∀ ε > (0:ℚ), ε.EventuallyClose (a:Sequence) (b:Sequence)

Definition 5.2.6 (Equivalent sequences)

lemma Sequence.equiv_def (a b: ℕ → ℚ) :
    Equiv a b ↔ ∀ (ε:ℚ), ε > 0 → ε.EventuallyClose (a:Sequence) (b:Sequence) := bya:ℕ → ℚb:ℕ → ℚ⊢ Equiv a b ↔ ∀ ε > 0, ε.EventuallyClose ↑a ↑b rflAll goals completed! 🐙

Definition 5.2.6 (Equivalent sequences)

lemma declaration uses `sorry`Sequence.equiv_iff (a b: ℕ → ℚ) : Equiv a b ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, |a n - b n| ≤ ε := bya:ℕ → ℚb:ℕ → ℚ⊢ Equiv a b ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, |a n - b n| ≤ ε
  sorryAll goals completed! 🐙

Proposition 5.2.8

lemma Sequence.equiv_example :
  -- This proof is perhaps more complicated than it needs to be; a shorter version may be
  -- possible that is still faithful to the original text.
  Equiv (fun n:ℕ ↦ (1:ℚ)+10^(-(n:ℤ)-1)) (fun n:ℕ ↦ (1:ℚ)-10^(-(n:ℤ)-1)) := by⊢ Equiv (fun n ↦ 1 + 10 ^ (-↑n - 1)) fun n ↦ 1 - 10 ^ (-↑n - 1)
  set a := fun n:ℕ ↦ (1:ℚ)+10^(-(n:ℤ)-1)a:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)⊢ Equiv a fun n ↦ 1 - 10 ^ (-↑n - 1)
  set b := fun n:ℕ ↦ (1:ℚ)-10^(-(n:ℤ)-1)a:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)⊢ Equiv a b
  rw [equiv_iff]a:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, |a n - b n| ≤ ε
  intro ε hεa:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0⊢ ∃ N, ∀ n ≥ N, |a n - b n| ≤ ε
  have hab (n:ℕ) : |a n - b n| = 2 * 10 ^ (-(n:ℤ)-1) := calc
    _ = |((1:ℚ) + (10:ℚ)^(-(n:ℤ)-1)) - ((1:ℚ) - (10:ℚ)^(-(n:ℤ)-1))| := rfl
    _ = |2 * (10:ℚ)^(-(n:ℤ)-1)| := bya:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0n:ℕ⊢ |1 + 10 ^ (-↑n - 1) - (1 - 10 ^ (-↑n - 1))| = |2 * 10 ^ (-↑n - 1)| ring_nfAll goals completed! 🐙
    _ = _ := abs_of_nonneg (bya:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0n:ℕ⊢ 0 ≤ 2 * 10 ^ (-↑n - 1) positivityAll goals completed! 🐙)
  have hab' (N:ℕ) : ∀ n ≥ N, |a n - b n| ≤ 2 * 10 ^(-(N:ℤ)-1) := by⊢ Equiv (fun n ↦ 1 + 10 ^ (-↑n - 1)) fun n ↦ 1 - 10 ^ (-↑n - 1)
    intro n hna:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)N:ℕn:ℕhn:n ≥ N⊢ |a n - b n| ≤ 2 * 10 ^ (-↑N - 1); rw [hab n]a:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)N:ℕn:ℕhn:n ≥ N⊢ 2 * 10 ^ (-↑n - 1) ≤ 2 * 10 ^ (-↑N - 1); gcongrhbc.haa:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)N:ℕn:ℕhn:n ≥ N⊢ 1 ≤ 10; norm_numAll goals completed! 🐙
  have hN : ∃ N:ℕ, 2 * (10:ℚ) ^(-(N:ℤ)-1) ≤ ε := by⊢ Equiv (fun n ↦ 1 + 10 ^ (-↑n - 1)) fun n ↦ 1 - 10 ^ (-↑n - 1)
    have hN' (N:ℕ) : 2 * (10:ℚ)^(-(N:ℤ)-1) ≤ 2/(N+1) := calc
      _ = 2 / (10:ℚ)^(N+1) := bya:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)N:ℕ⊢ 2 * 10 ^ (-↑N - 1) = 2 / 10 ^ (N + 1)
        field_simpa:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)N:ℕ⊢ 10 ^ (-↑N - 1) * 10 ^ (N + 1) = 1
        simp [←Section_4_3.pow_eq_zpow, ←zpow_add₀ (show 10 ≠ (0:ℚ) by norm_num)]All goals completed! 🐙
      _ ≤ _ := bya:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)N:ℕ⊢ 2 / 10 ^ (N + 1) ≤ 2 / (↑N + 1)
        gcongrhdba:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)N:ℕ⊢ ↑N + 1 ≤ 10 ^ (N + 1)
        apply le_trans _ (pow_le_pow_left₀ (show 0 ≤ (2:ℚ) bya:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)N:ℕ⊢ 2 / 10 ^ (N + 1) ≤ 2 / (↑N + 1) norm_numAll goals completed! 🐙)
          (show (2:ℚ) ≤ 10 bya:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)N:ℕ⊢ 2 / 10 ^ (N + 1) ≤ 2 / (↑N + 1) norm_numAll goals completed! 🐙) _)
        convert Nat.cast_le.mpr (Section_4_3.two_pow_geq (N+1)) using 1h.e'_3a:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)N:ℕ⊢ ↑N + 1 = ↑(N + 1)h.e'_4a:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)N:ℕ⊢ 2 ^ (N + 1) = ↑(2 ^ (N + 1))convert_2a:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)N:ℕ⊢ AddMonoidWithOne ℚconvert_4a:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)N:ℕ⊢ AddLeftMono ℚconvert_5a:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)N:ℕ⊢ ZeroLEOneClass ℚconvert_6a:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)N:ℕ⊢ CharZero ℚ <;>h.e'_3a:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)N:ℕ⊢ ↑N + 1 = ↑(N + 1)h.e'_4a:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)N:ℕ⊢ 2 ^ (N + 1) = ↑(2 ^ (N + 1))convert_2a:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)N:ℕ⊢ AddMonoidWithOne ℚconvert_4a:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)N:ℕ⊢ AddLeftMono ℚconvert_5a:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)N:ℕ⊢ ZeroLEOneClass ℚconvert_6a:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)N:ℕ⊢ CharZero ℚ try infer_instanceAll goals completed! 🐙
        all_goals simpAll goals completed! 🐙
    choose N hN using exists_nat_gt (2 / ε)a:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)hN':∀ (N : ℕ), 2 * 10 ^ (-↑N - 1) ≤ 2 / (↑N + 1)N:ℕhN:2 / ε < ↑N⊢ ∃ N, 2 * 10 ^ (-↑N - 1) ≤ ε
    refine ⟨ N, (hN' N).trans ?_ ⟩a:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)hN':∀ (N : ℕ), 2 * 10 ^ (-↑N - 1) ≤ 2 / (↑N + 1)N:ℕhN:2 / ε < ↑N⊢ 2 / (↑N + 1) ≤ ε
    rw [div_le_iff₀ (by positivity)]a:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)hN':∀ (N : ℕ), 2 * 10 ^ (-↑N - 1) ≤ 2 / (↑N + 1)N:ℕhN:2 / ε < ↑N⊢ 2 ≤ ε * (↑N + 1)
    rw [div_lt_iff₀ hε] at hNa:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)hN':∀ (N : ℕ), 2 * 10 ^ (-↑N - 1) ≤ 2 / (↑N + 1)N:ℕhN:2 < ↑N * ε⊢ 2 ≤ ε * (↑N + 1)
    grind [mul_comm]All goals completed! 🐙
  choose N hN using hNa:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)N:ℕhN:2 * 10 ^ (-↑N - 1) ≤ ε⊢ ∃ N, ∀ n ≥ N, |a n - b n| ≤ ε; use Nha:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)N:ℕhN:2 * 10 ^ (-↑N - 1) ≤ ε⊢ ∀ n ≥ N, |a n - b n| ≤ ε; intro n hnha:ℕ → ℚ := fun n ↦ 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n ↦ 1 - 10 ^ (-↑n - 1)ε:ℚhε:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)hab':∀ (N n : ℕ), n ≥ N → |a n - b n| ≤ 2 * 10 ^ (-↑N - 1)N:ℕhN:2 * 10 ^ (-↑N - 1) ≤ εn:ℕhn:n ≥ N⊢ |a n - b n| ≤ ε
  linarith [hab' N n hn]All goals completed! 🐙

Exercise 5.2.1

theorem declaration uses `sorry`Sequence.isCauchy_of_equiv {a b: ℕ → ℚ} (hab: Equiv a b) :
    (a:Sequence).IsCauchy ↔ (b:Sequence).IsCauchy := bya:ℕ → ℚb:ℕ → ℚhab:Equiv a b⊢ (↑a).IsCauchy ↔ (↑b).IsCauchy sorryAll goals completed! 🐙

Exercise 5.2.2

theorem declaration uses `sorry`Sequence.isBounded_of_eventuallyClose {ε:ℚ} {a b: ℕ → ℚ} (hab: ε.EventuallyClose a b) :
    (a:Sequence).IsBounded ↔ (b:Sequence).IsBounded := byε:ℚa:ℕ → ℚb:ℕ → ℚhab:ε.EventuallyClose ↑a ↑b⊢ (↑a).IsBounded ↔ (↑b).IsBounded sorryAll goals completed! 🐙

end Chapter5