Аналіз I, Глава 5.2

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

abbrev Rat.close_seq (ε: ℚ) (a b: Chapter5.Sequence) : Prop :=
  ∀ n, n ≥ a.n₀ → n ≥ b.n₀ → ε.close (a n) (b n)

abbrev Rat.eventually_close (ε: ℚ) (a b: Chapter5.Sequence) : Prop :=
  ∃ N, ε.close_seq (a.from N) (b.from N)

namespace Chapter5

Визначення 5.2.1 ($ε$-close sequences)

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

Приклад 5.2.2

declaration uses 'sorry'example : (0.1:ℚ).close_seq ((fun n:ℕ ↦ ((-1)^n:ℚ)):Sequence)
((fun n:ℕ ↦ ((1.1:ℚ) * (-1)^n)):Sequence) := by⊢ Rat.close_seq 0.1 { n₀ := 0, seq := fun n => if n ≥ 0 then (fun n => (-1) ^ n) n.toNat else 0, vanish := ⋯ }
  { n₀ := 0, seq := fun n => if n ≥ 0 then (fun n => 1.1 * (-1) ^ n) n.toNat else 0, vanish := ⋯ } sorryAll goals completed! 🐙

Приклад 5.2.2

declaration uses 'sorry'example : ¬ (0.1:ℚ).steady ((fun n:ℕ ↦ ((-1)^n:ℚ)):Sequence)
:= by⊢ ¬Rat.steady 0.1 { n₀ := 0, seq := fun n => if n ≥ 0 then (fun n => (-1) ^ n) n.toNat else 0, vanish := ⋯ } sorryAll goals completed! 🐙

Приклад 5.2.2

declaration uses 'sorry'example : ¬ (0.1:ℚ).steady ((fun n:ℕ ↦ ((1.1:ℚ) * (-1)^n)):Sequence)
:= by⊢ ¬Rat.steady 0.1 { n₀ := 0, seq := fun n => if n ≥ 0 then (fun n => 1.1 * (-1) ^ n) n.toNat else 0, vanish := ⋯ } sorryAll goals completed! 🐙

Визначення 5.2.3 (Eventually ε-close sequences)

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

Визначення 5.2.3 (Eventually ε-close sequences)

lemma declaration uses 'sorry'Rat.eventually_close_iff (ε: ℚ) (a b: ℕ → ℚ) :
    ε.eventually_close (a:Sequence) (b:Sequence) ↔  ∃ N, ∀ n ≥ N, |a n - b n| ≤ ε := byε:ℚa:ℕ → ℚb:ℕ → ℚ⊢ ε.eventually_close { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }
    { n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ } ↔
  ∃ N, ∀ n ≥ N, |a n - b n| ≤ ε sorryAll goals completed! 🐙

Приклад 5.2.5

declaration uses 'sorry'example : ¬ (0.1:ℚ).close_seq ((fun n:ℕ ↦ (1:ℚ)+10^(-(n:ℤ)-1)):Sequence)
  ((fun n:ℕ ↦ (1:ℚ)-10^(-(n:ℤ)-1)):Sequence) := by⊢ ¬Rat.close_seq 0.1 { n₀ := 0, seq := fun n => if n ≥ 0 then (fun n => 1 + 10 ^ (-↑n - 1)) n.toNat else 0, vanish := ⋯ }
    { n₀ := 0, seq := fun n => if n ≥ 0 then (fun n => 1 - 10 ^ (-↑n - 1)) n.toNat else 0, vanish := ⋯ } sorryAll goals completed! 🐙

declaration uses 'sorry'example : (0.1:ℚ).eventually_close ((fun n:ℕ ↦ (1:ℚ)+10^(-(n:ℤ)-1)):Sequence)
  ((fun n:ℕ ↦ (1:ℚ)-10^(-(n:ℤ)-1)):Sequence) := by⊢ Rat.eventually_close 0.1
  { n₀ := 0, seq := fun n => if n ≥ 0 then (fun n => 1 + 10 ^ (-↑n - 1)) n.toNat else 0, vanish := ⋯ }
  { n₀ := 0, seq := fun n => if n ≥ 0 then (fun n => 1 - 10 ^ (-↑n - 1)) n.toNat else 0, vanish := ⋯ } sorryAll goals completed! 🐙

declaration uses 'sorry'example : (0.01:ℚ).eventually_close ((fun n:ℕ ↦ (1:ℚ)+10^(-(n:ℤ)-1)):Sequence)
  ((fun n:ℕ ↦ (1:ℚ)-10^(-(n:ℤ)-1)):Sequence) := by⊢ Rat.eventually_close 1e-2
  { n₀ := 0, seq := fun n => if n ≥ 0 then (fun n => 1 + 10 ^ (-↑n - 1)) n.toNat else 0, vanish := ⋯ }
  { n₀ := 0, seq := fun n => if n ≥ 0 then (fun n => 1 - 10 ^ (-↑n - 1)) n.toNat else 0, vanish := ⋯ } sorryAll goals completed! 🐙

Визначення 5.2.6 (Equivalent sequences)

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

Визначення 5.2.6 (Equivalent sequences)

lemma Sequence.equiv_def (a b: ℕ → ℚ) :
    equiv a b ↔ ∀ (ε:ℚ), ε > 0 → ε.eventually_close (a:Sequence) (b:Sequence) := bya:ℕ → ℚb:ℕ → ℚ⊢ equiv a b ↔
  ∀ ε > 0,
    ε.eventually_close { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }
      { n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ } rflAll goals completed! 🐙

Визначення 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! 🐙

Твердження 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 ε εposa:ℕ → ℚ := fun n => 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n => 1 - 10 ^ (-↑n - 1)ε:ℚεpos:ε > 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))| := bya:ℕ → ℚ := fun n => 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n => 1 - 10 ^ (-↑n - 1)ε:ℚεpos:ε > 0n:ℕ⊢ |a n - b n| = |1 + 10 ^ (-↑n - 1) - (1 - 10 ^ (-↑n - 1))| rflAll goals completed! 🐙
    _ = |2 * (10:ℚ)^(-(n:ℤ)-1)| := bya:ℕ → ℚ := fun n => 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n => 1 - 10 ^ (-↑n - 1)ε:ℚεpos:ε > 0n:ℕ⊢ |1 + 10 ^ (-↑n - 1) - (1 - 10 ^ (-↑n - 1))| = |2 * 10 ^ (-↑n - 1)| ring_nfAll goals completed! 🐙
    _ = _ := bya:ℕ → ℚ := fun n => 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n => 1 - 10 ^ (-↑n - 1)ε:ℚεpos:ε > 0n:ℕ⊢ |2 * 10 ^ (-↑n - 1)| = 2 * 10 ^ (-↑n - 1) apply abs_of_nonnegha:ℕ → ℚ := fun n => 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n => 1 - 10 ^ (-↑n - 1)ε:ℚεpos:ε > 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)ε:ℚεpos:ε > 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)ε:ℚεpos:ε > 0hab:∀ (n : ℕ), |a n - b n| = 2 * 10 ^ (-↑n - 1)N:ℕn:ℕhn:n ≥ N⊢ 2 * 10 ^ (-↑n - 1) ≤ 2 * 10 ^ (-↑N - 1)
    gcongrh.haa:ℕ → ℚ := fun n => 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n => 1 - 10 ^ (-↑n - 1)ε:ℚεpos:ε > 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)ε:ℚεpos:ε > 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)ε:ℚεpos:ε > 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) * 10 ^ (N + 1) = 2
        rw [mul_assoc, ←Section_4_3.pow_eq_zpow, ←zpow_add₀ (by norm_num)]a:ℕ → ℚ := fun n => 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n => 1 - 10 ^ (-↑n - 1)ε:ℚεpos:ε > 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 + ↑(N + 1)) = 2
        simpAll goals completed! 🐙
      _ ≤ _ := bya:ℕ → ℚ := fun n => 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n => 1 - 10 ^ (-↑n - 1)ε:ℚεpos:ε > 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)
        gcongrha:ℕ → ℚ := fun n => 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n => 1 - 10 ^ (-↑n - 1)ε:ℚεpos:ε > 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)ε:ℚεpos:ε > 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)ε:ℚεpos:ε > 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)ε:ℚεpos:ε > 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)ε:ℚεpos:ε > 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)ε:ℚεpos:ε > 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)ε:ℚεpos:ε > 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)ε:ℚεpos:ε > 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)ε:ℚεpos:ε > 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)ε:ℚεpos:ε > 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) simpAll goals completed! 🐙
        .h.e'_4a:ℕ → ℚ := fun n => 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n => 1 - 10 ^ (-↑n - 1)ε:ℚεpos:ε > 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)) simpAll goals completed! 🐙
        all_goals infer_instanceAll goals completed! 🐙
    have : ∃ N:ℕ, N > 2/ε := exists_nat_gt (2 / ε)a:ℕ → ℚ := fun n => 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n => 1 - 10 ^ (-↑n - 1)ε:ℚεpos:ε > 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)this:∃ N, ↑N > 2 / ε⊢ ∃ N, 2 * 10 ^ (-↑N - 1) ≤ ε
    obtain ⟨ N, hN ⟩ := thisintroa:ℕ → ℚ := fun n => 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n => 1 - 10 ^ (-↑n - 1)ε:ℚεpos:ε > 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:↑N > 2 / ε⊢ ∃ N, 2 * 10 ^ (-↑N - 1) ≤ ε
    use Nha:ℕ → ℚ := fun n => 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n => 1 - 10 ^ (-↑n - 1)ε:ℚεpos:ε > 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:↑N > 2 / ε⊢ 2 * 10 ^ (-↑N - 1) ≤ ε
    apply (hN' N).transha:ℕ → ℚ := fun n => 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n => 1 - 10 ^ (-↑n - 1)ε:ℚεpos:ε > 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:↑N > 2 / ε⊢ 2 / (↑N + 1) ≤ ε
    rw [div_le_iff₀ (by positivity)]ha:ℕ → ℚ := fun n => 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n => 1 - 10 ^ (-↑n - 1)ε:ℚεpos:ε > 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:↑N > 2 / ε⊢ 2 ≤ ε * (↑N + 1)
    replace hN := (div_lt_iff₀ εpos).mp hNha:ℕ → ℚ := fun n => 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n => 1 - 10 ^ (-↑n - 1)ε:ℚεpos:ε > 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)
    apply le_of_lt (hN.trans _)a:ℕ → ℚ := fun n => 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n => 1 - 10 ^ (-↑n - 1)ε:ℚεpos:ε > 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 * ε < ε * (↑N + 1)
    rw [mul_comm]a:ℕ → ℚ := fun n => 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n => 1 - 10 ^ (-↑n - 1)ε:ℚεpos:ε > 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 < ε * (↑N + 1)
    gcongrbca:ℕ → ℚ := fun n => 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n => 1 - 10 ^ (-↑n - 1)ε:ℚεpos:ε > 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 < ↑N + 1; linarithAll goals completed! 🐙
  obtain ⟨ N, hN ⟩ := hNintroa:ℕ → ℚ := fun n => 1 + 10 ^ (-↑n - 1)b:ℕ → ℚ := fun n => 1 - 10 ^ (-↑n - 1)ε:ℚεpos:ε > 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)ε:ℚεpos:ε > 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)ε:ℚεpos:ε > 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| ≤ ε
  exact (hab' N n hn).trans hNAll goals completed! 🐙

Вправа 5.2.1

theorem declaration uses 'sorry'Sequence.equiv_of_cauchy {a b: ℕ → ℚ} (hab: Sequence.equiv a b) :
    (a:Sequence).isCauchy ↔ (b:Sequence).isCauchy := bya:ℕ → ℚb:ℕ → ℚhab:equiv a b⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ↔
  { n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchy sorryAll goals completed! 🐙

Вправа 5.2.2

theorem declaration uses 'sorry'Sequence.close_of_bounded {ε:ℚ} {a b: ℕ → ℚ} (hab: ε.eventually_close a b) :
    (a:Sequence).isBounded ↔ (b:Sequence).isBounded := byε:ℚa:ℕ → ℚb:ℕ → ℚhab:ε.eventually_close { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }
  { n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isBounded ↔
  { n₀ := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isBounded sorryAll goals completed! 🐙

end Chapter5