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

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 a sequence of rationals
Notions of unknown identifier 'ε'ε-steadiness, eventual unknown identifier 'ε'ε-steadiness, and Cauchy sequences

namespace Chapter5

Визначення 5.1.1 (Sequence). To avoid some technicalities involving dependent types, we extend sequences by zero to the left of the starting point unknown identifier 'n₀'n₀.

@[ext]
structure Sequence where
  n₀ : ℤ
  seq : ℤ → ℚ
  vanish : ∀ n < n₀, seq n = 0

Sequences can be thought of as functions from ℤ to ℚ.

instance Sequence.instCoeFun : CoeFun Sequence (fun _ ↦ ℤ → ℚ) where
  coe := fun a ↦ a.seq

Functions from ℕ to ℚ can be thought of as sequences.

instance Sequence.instCoe : Coe (ℕ → ℚ) Sequence where
  coe := fun a ↦ {
    n₀ := 0
    seq := fun n ↦ if n ≥ 0 then a n.toNat else 0
    vanish := bya:ℕ → ℚ⊢ ∀ n < 0, (if n ≥ 0 then a n.toNat else 0) = 0
      intro n hna:ℕ → ℚn:ℤhn:n < 0⊢ (if n ≥ 0 then a n.toNat else 0) = 0
      simp [hn]All goals completed! 🐙
  }

abbrev Sequence.mk' (n₀:ℤ) (a: { n // n ≥ n₀ } → ℚ) : Sequence where
  n₀ := n₀
  seq := fun n ↦ if h : n ≥ n₀ then a ⟨n, h⟩ else 0
  vanish := byn₀:ℤa:{ n // n ≥ n₀ } → ℚ⊢ ∀ n < n₀, (if h : n ≥ n₀ then a ⟨n, h⟩ else 0) = 0
    intro n hnn₀:ℤa:{ n // n ≥ n₀ } → ℚn:ℤhn:n < n₀⊢ (if h : n ≥ n₀ then a ⟨n, h⟩ else 0) = 0
    simp [hn]All goals completed! 🐙

lemma Sequence.eval_mk {n n₀:ℤ} (a: { n // n ≥ n₀ } → ℚ) (h: n ≥ n₀) :
    (Sequence.mk' n₀ a) n = a ⟨ n, h ⟩ := byn:ℤn₀:ℤa:{ n // n ≥ n₀ } → ℚh:n ≥ n₀⊢ (mk' n₀ a).seq n = a ⟨n, h⟩ simp [seq, h]All goals completed! 🐙

@[simp]
lemma Sequence.eval_coe (n:ℕ) (a: ℕ → ℚ) : (a:Sequence) n = a n := byn:ℕa:ℕ → ℚ⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq ↑n = a n simp [seq]All goals completed! 🐙

Приклад 5.1.2

abbrev Sequence.squares : Sequence := ((fun n:ℕ ↦ (n^2:ℚ)):Sequence)

Приклад 5.1.2

example (n:ℕ) : Sequence.squares n = n^2 := Sequence.eval_coe _ _

Приклад 5.1.2

abbrev Sequence.three : Sequence := ((fun (_:ℕ) ↦ (3:ℚ)):Sequence)

Приклад 5.1.2

example (n:ℕ) : Sequence.three n = 3 := Sequence.eval_coe _ (fun (_:ℕ) ↦ (3:ℚ))

Приклад 5.1.2

abbrev Sequence.squares_from_three : Sequence := mk' 3 (fun n ↦ n^2)

Приклад 5.1.2

example (n:ℤ) (hn: n ≥ 3) : Sequence.squares_from_three n = n^2 := Sequence.eval_mk _ hn

-- need to temporarily leave the `Chapter5` namespace to introduce the following notation

end Chapter5

abbrev Rat.steady (ε: ℚ) (a: Chapter5.Sequence) : Prop :=
  ∀ n ≥ a.n₀, ∀ m ≥ a.n₀, ε.close (a n) (a m)

lemma Rat.steady_def (ε: ℚ) (a: Chapter5.Sequence) :
  ε.steady a ↔ ∀ n ≥ a.n₀, ∀ m ≥ a.n₀, ε.close (a n) (a m) := byε:ℚa:Chapter5.Sequence⊢ ε.steady a ↔ ∀ n ≥ a.n₀, ∀ m ≥ a.n₀, ε.close (a.seq n) (a.seq m) rflAll goals completed! 🐙

namespace Chapter5

Приклад 5.1.5

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

Приклад 5.1.5

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

Приклад 5.1.5

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

Приклад 5.1.5

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

Приклад 5.1.5

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

Приклад 5.1.5

declaration uses 'sorry'example (ε:ℚ) (hε: ε>0) : ε.steady ((fun _:ℕ ↦ (2:ℚ) ):Sequence) := byε:ℚhε:ε > 0⊢ ε.steady { n₀ := 0, seq := fun n => if n ≥ 0 then (fun x => 2) n.toNat else 0, vanish := ⋯ } sorryAll goals completed! 🐙

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

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

a.from n₁ starts from unknown identifier 'n₁'n₁. It is intended for use when unknown identifier 'n₁'sorry ≥ sorry : Propn₁ ≥ unknown identifier 'n₀'n₀, but returns the "junk" value of the original sequence unknown identifier 'a'a otherwise.

abbrev Sequence.from (a:Sequence) (n₁:ℤ) : Sequence :=
  mk' (max a.n₀ n₁) (fun n ↦ a (n:ℤ))

lemma Sequence.from_eval (a:Sequence) {n₁ n:ℤ} (hn: n ≥ n₁) :
  (a.from n₁) n = a n := bya:Sequencen₁:ℤn:ℤhn:n ≥ n₁⊢ (a.from n₁).seq n = a.seq n
  simp [Sequence.from, seq, hn]a:Sequencen₁:ℤn:ℤhn:n ≥ n₁⊢ n < a.n₀ → 0 = a.seq n
  intro ha:Sequencen₁:ℤn:ℤhn:n ≥ n₁h:n < a.n₀⊢ 0 = a.seq n
  exact (a.vanish n h).symmAll goals completed! 🐙

end Chapter5

Визначення 5.1.6 (Eventually ε-steady)

abbrev Rat.eventuallySteady (ε: ℚ) (a: Chapter5.Sequence) : Prop :=
  ∃ N ≥ a.n₀, ε.steady (a.from N)

lemma Rat.eventuallySteady_def (ε: ℚ) (a: Chapter5.Sequence) :
  ε.eventuallySteady a ↔ ∃ N ≥ a.n₀, ε.steady (a.from N) := byε:ℚa:Chapter5.Sequence⊢ ε.eventuallySteady a ↔ ∃ N ≥ a.n₀, ε.steady (a.from N) rflAll goals completed! 🐙

namespace Chapter5

Приклад 5.1.7

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

lemma declaration uses 'sorry'Sequence.ex_5_1_7_b : (0.1:ℚ).steady (((fun n:ℕ ↦ (n+1:ℚ)⁻¹ ):Sequence).from 10) := by⊢ Rat.steady 0.1 ({ n₀ := 0, seq := fun n => if n ≥ 0 then (fun n => (↑n + 1)⁻¹) n.toNat else 0, vanish := ⋯ }.from 10)
  sorryAll goals completed! 🐙

lemma declaration uses 'sorry'Sequence.ex_5_1_7_c : (0.1:ℚ).eventuallySteady ((fun n:ℕ ↦ (n+1:ℚ)⁻¹ ):Sequence) := by⊢ Rat.eventuallySteady 0.1 { n₀ := 0, seq := fun n => if n ≥ 0 then (fun n => (↑n + 1)⁻¹) n.toNat else 0, vanish := ⋯ }
  sorryAll goals completed! 🐙

lemma declaration uses 'sorry'Sequence.ex_5_1_7_d {ε:ℚ} (hε:ε>0) :
    ε.eventuallySteady ((fun n:ℕ ↦ if n=0 then (10:ℚ) else (0:ℚ) ):Sequence) := byε:ℚhε:ε > 0⊢ ε.eventuallySteady
  { n₀ := 0, seq := fun n => if n ≥ 0 then (fun n => if n = 0 then 10 else 0) n.toNat else 0, vanish := ⋯ } sorryAll goals completed! 🐙

abbrev Sequence.isCauchy (a:Sequence) : Prop := ∀ ε > (0:ℚ), ε.eventuallySteady a

lemma Sequence.isCauchy_def (a:Sequence) :
  a.isCauchy ↔ ∀ ε > (0:ℚ), ε.eventuallySteady a := bya:Sequence⊢ a.isCauchy ↔ ∀ ε > 0, ε.eventuallySteady a rflAll goals completed! 🐙

lemma declaration uses 'sorry'Sequence.isCauchy_of_coe (a:ℕ → ℚ) :
    (a:Sequence).isCauchy ↔ ∀ ε > (0:ℚ), ∃ N, ∀ j ≥ N, ∀ k ≥ N,
    Section_4_3.dist (a j) (a k) ≤ ε := bya:ℕ → ℚ⊢ { n₀ := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ↔
  ∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε sorryAll goals completed! 🐙

lemma declaration uses 'sorry'Sequence.isCauchy_of_mk {n₀:ℤ} (a: {n // n ≥ n₀} → ℚ) :
    (mk' n₀ a).isCauchy ↔ ∀ ε > (0:ℚ), ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N,
    Section_4_3.dist (mk' n₀ a j) (mk' n₀ a k) ≤ ε := byn₀:ℤa:{ n // n ≥ n₀ } → ℚ⊢ (mk' n₀ a).isCauchy ↔ ∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε sorryAll goals completed! 🐙

noncomputable def Sequence.sqrt_two : Sequence :=
  (fun n:ℕ ↦ ((⌊ (Real.sqrt 2)*10^n ⌋ / 10^n):ℚ))

Приклад 5.1.10. (This requires extensive familiarity with Mathlib's API for the real numbers.)

theorem declaration uses 'sorry'Sequence.ex_5_1_10_a : (1:ℚ).steady sqrt_two := by⊢ Rat.steady 1 sqrt_two sorryAll goals completed! 🐙

Приклад 5.1.10. (This requires extensive familiarity with Mathlib's API for the real numbers.)

theorem declaration uses 'sorry'Sequence.ex_5_1_10_b : (0.1:ℚ).steady (sqrt_two.from 1) := by⊢ Rat.steady 0.1 (sqrt_two.from 1) sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Sequence.ex_5_1_10_c : (0.1:ℚ).eventuallySteady sqrt_two := by⊢ Rat.eventuallySteady 0.1 sqrt_two sorryAll goals completed! 🐙

Твердження 5.1.11

theorem Sequence.harmonic_steady : (mk' 1 (fun n ↦ (1:ℚ)/n)).isCauchy := by⊢ (mk' 1 fun n => 1 / ↑↑n).isCauchy
  -- This is proof is probably longer than it needs to be; there should be a shorter proof that
  -- is still in the spirit of  the proof in the book.
  rw [isCauchy_of_mk (fun n ↦ (1:ℚ)/n)]⊢ ∀ ε > 0,
  ∃ N ≥ 1, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' 1 fun n => 1 / ↑↑n).seq j) ((mk' 1 fun n => 1 / ↑↑n).seq k) ≤ ε
  intro ε hεε:ℚhε:ε > 0⊢ ∃ N ≥ 1, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' 1 fun n => 1 / ↑↑n).seq j) ((mk' 1 fun n => 1 / ↑↑n).seq k) ≤ ε
  have : ∃ N:ℕ, N > 1/ε := exists_nat_gt (1 / ε)ε:ℚhε:ε > 0this:∃ N, ↑N > 1 / ε⊢ ∃ N ≥ 1, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' 1 fun n => 1 / ↑↑n).seq j) ((mk' 1 fun n => 1 / ↑↑n).seq k) ≤ ε
  obtain ⟨ N, hN ⟩ := thisintroε:ℚhε:ε > 0N:ℕhN:↑N > 1 / ε⊢ ∃ N ≥ 1, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' 1 fun n => 1 / ↑↑n).seq j) ((mk' 1 fun n => 1 / ↑↑n).seq k) ≤ ε
  use Nhε:ℚhε:ε > 0N:ℕhN:↑N > 1 / ε⊢ ↑N ≥ 1 ∧ ∀ j ≥ ↑N, ∀ k ≥ ↑N, Section_4_3.dist ((mk' 1 fun n => 1 / ↑↑n).seq j) ((mk' 1 fun n => 1 / ↑↑n).seq k) ≤ ε
  have hN' : (N:ℤ) > 0 := by⊢ (mk' 1 fun n => 1 / ↑↑n).isCauchy
    have : (1/ε) > 0 := by⊢ (mk' 1 fun n => 1 / ↑↑n).isCauchy positivityAll goals completed! 🐙
    replace hN := this.trans hNε:ℚhε:ε > 0N:ℕthis:1 / ε > 0hN:0 < ↑N⊢ ↑N > 0
    simp at hN ⊢ε:ℚhε:ε > 0N:ℕthis:1 / ε > 0hN:0 < N⊢ 0 < N; assumptionAll goals completed! 🐙
  constructorh.leftε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0⊢ ↑N ≥ 1h.rightε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0⊢ ∀ j ≥ ↑N, ∀ k ≥ ↑N, Section_4_3.dist ((mk' 1 fun n => 1 / ↑↑n).seq j) ((mk' 1 fun n => 1 / ↑↑n).seq k) ≤ ε
  .h.leftε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0⊢ ↑N ≥ 1 simp at hN' ⊢h.leftε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':0 < N⊢ 1 ≤ N; linarithAll goals completed! 🐙
  intro j hj k hkh.rightε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑N⊢ Section_4_3.dist ((mk' 1 fun n => 1 / ↑↑n).seq j) ((mk' 1 fun n => 1 / ↑↑n).seq k) ≤ ε
  have hj' : (j:ℚ) ≥ 0 := by⊢ (mk' 1 fun n => 1 / ↑↑n).isCauchy simpε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑N⊢ 0 ≤ j; linarithAll goals completed! 🐙
  have hj'' : (1:ℚ)/j ≤ (1:ℚ)/N := by⊢ (mk' 1 fun n => 1 / ↑↑n).isCauchy
    gcongrhcε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0⊢ 0 < ↑Nhε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0⊢ ↑N ≤ ↑j
    .hcε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0⊢ 0 < ↑N simp at hN' ⊢hcε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εj:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hN':0 < N⊢ 0 < N; assumptionAll goals completed! 🐙
    .hε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0⊢ ↑N ≤ ↑j simp at hj ⊢hε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hj:↑N ≤ j⊢ ↑N ≤ ↑j; qify at hjhε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hj:↑N ≤ ↑j⊢ ↑N ≤ ↑j; assumptionAll goals completed! 🐙
  have hj''' : (1:ℚ)/j ≥ 0 := by⊢ (mk' 1 fun n => 1 / ↑↑n).isCauchy positivityAll goals completed! 🐙
  have hj'''' : j ≥ 1 := by⊢ (mk' 1 fun n => 1 / ↑↑n).isCauchy simp at hj'ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj':0 ≤ j⊢ j ≥ 1; linarithAll goals completed! 🐙
  have hk' : (k:ℚ) ≥ 0 := by⊢ (mk' 1 fun n => 1 / ↑↑n).isCauchy simpε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj'''':j ≥ 1⊢ 0 ≤ k; linarithAll goals completed! 🐙
  have hk'' : (1:ℚ)/k ≤ (1:ℚ)/N := by⊢ (mk' 1 fun n => 1 / ↑↑n).isCauchy
    gcongrhcε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj'''':j ≥ 1hk':↑k ≥ 0⊢ 0 < ↑Nhε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj'''':j ≥ 1hk':↑k ≥ 0⊢ ↑N ≤ ↑k
    .hcε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj'''':j ≥ 1hk':↑k ≥ 0⊢ 0 < ↑N simp at hN' ⊢hcε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εj:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj'''':j ≥ 1hk':↑k ≥ 0hN':0 < N⊢ 0 < N; assumptionAll goals completed! 🐙
    .hε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj'''':j ≥ 1hk':↑k ≥ 0⊢ ↑N ≤ ↑k simp at hk ⊢hε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhj':↑j ≥ 0hj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj'''':j ≥ 1hk':↑k ≥ 0hk:↑N ≤ k⊢ ↑N ≤ ↑k; qify at hkhε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhj':↑j ≥ 0hj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj'''':j ≥ 1hk':↑k ≥ 0hk:↑N ≤ ↑k⊢ ↑N ≤ ↑k; assumptionAll goals completed! 🐙
  have hk''' : (1:ℚ)/k ≥ 0 := by⊢ (mk' 1 fun n => 1 / ↑↑n).isCauchy positivityAll goals completed! 🐙
  have hk'''' : k ≥ 1 := by⊢ (mk' 1 fun n => 1 / ↑↑n).isCauchy simp at hk'ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj'''':j ≥ 1hk'':1 / ↑k ≤ 1 / ↑Nhk''':1 / ↑k ≥ 0hk':0 ≤ k⊢ k ≥ 1; linarithAll goals completed! 🐙
  have hdist : Section_4_3.dist ((1:ℚ)/j) ((1:ℚ)/k) ≤ (1:ℚ)/N := by⊢ (mk' 1 fun n => 1 / ↑↑n).isCauchy
    rw [Section_4_3.dist_eq, abs_le']ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj'''':j ≥ 1hk':↑k ≥ 0hk'':1 / ↑k ≤ 1 / ↑Nhk''':1 / ↑k ≥ 0hk'''':k ≥ 1⊢ 1 / ↑j - 1 / ↑k ≤ 1 / ↑N ∧ -(1 / ↑j - 1 / ↑k) ≤ 1 / ↑N
    constructorleftε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj'''':j ≥ 1hk':↑k ≥ 0hk'':1 / ↑k ≤ 1 / ↑Nhk''':1 / ↑k ≥ 0hk'''':k ≥ 1⊢ 1 / ↑j - 1 / ↑k ≤ 1 / ↑Nrightε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj'''':j ≥ 1hk':↑k ≥ 0hk'':1 / ↑k ≤ 1 / ↑Nhk''':1 / ↑k ≥ 0hk'''':k ≥ 1⊢ -(1 / ↑j - 1 / ↑k) ≤ 1 / ↑N <;>leftε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj'''':j ≥ 1hk':↑k ≥ 0hk'':1 / ↑k ≤ 1 / ↑Nhk''':1 / ↑k ≥ 0hk'''':k ≥ 1⊢ 1 / ↑j - 1 / ↑k ≤ 1 / ↑Nrightε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj'''':j ≥ 1hk':↑k ≥ 0hk'':1 / ↑k ≤ 1 / ↑Nhk''':1 / ↑k ≥ 0hk'''':k ≥ 1⊢ -(1 / ↑j - 1 / ↑k) ≤ 1 / ↑N linarithAll goals completed! 🐙
  simp [seq, hj'''', hk'''']h.rightε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj'''':j ≥ 1hk':↑k ≥ 0hk'':1 / ↑k ≤ 1 / ↑Nhk''':1 / ↑k ≥ 0hk'''':k ≥ 1hdist:Section_4_3.dist (1 / ↑j) (1 / ↑k) ≤ 1 / ↑N⊢ Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ ε
  convert hdist.trans _ using 2h.e'_3.h.e'_1ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj'''':j ≥ 1hk':↑k ≥ 0hk'':1 / ↑k ≤ 1 / ↑Nhk''':1 / ↑k ≥ 0hk'''':k ≥ 1hdist:Section_4_3.dist (1 / ↑j) (1 / ↑k) ≤ 1 / ↑N⊢ (↑j)⁻¹ = 1 / ↑jh.e'_3.h.e'_2ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj'''':j ≥ 1hk':↑k ≥ 0hk'':1 / ↑k ≤ 1 / ↑Nhk''':1 / ↑k ≥ 0hk'''':k ≥ 1hdist:Section_4_3.dist (1 / ↑j) (1 / ↑k) ≤ 1 / ↑N⊢ (↑k)⁻¹ = 1 / ↑kh.right.convert_2ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj'''':j ≥ 1hk':↑k ≥ 0hk'':1 / ↑k ≤ 1 / ↑Nhk''':1 / ↑k ≥ 0hk'''':k ≥ 1hdist:Section_4_3.dist (1 / ↑j) (1 / ↑k) ≤ 1 / ↑N⊢ 1 / ↑N ≤ ε
  .h.e'_3.h.e'_1ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj'''':j ≥ 1hk':↑k ≥ 0hk'':1 / ↑k ≤ 1 / ↑Nhk''':1 / ↑k ≥ 0hk'''':k ≥ 1hdist:Section_4_3.dist (1 / ↑j) (1 / ↑k) ≤ 1 / ↑N⊢ (↑j)⁻¹ = 1 / ↑j simpAll goals completed! 🐙
  .h.e'_3.h.e'_2ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj'''':j ≥ 1hk':↑k ≥ 0hk'':1 / ↑k ≤ 1 / ↑Nhk''':1 / ↑k ≥ 0hk'''':k ≥ 1hdist:Section_4_3.dist (1 / ↑j) (1 / ↑k) ≤ 1 / ↑N⊢ (↑k)⁻¹ = 1 / ↑k simpAll goals completed! 🐙
  rw [div_le_iff₀, mul_comm, ←div_le_iff₀ hε]h.right.convert_2ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj'''':j ≥ 1hk':↑k ≥ 0hk'':1 / ↑k ≤ 1 / ↑Nhk''':1 / ↑k ≥ 0hk'''':k ≥ 1hdist:Section_4_3.dist (1 / ↑j) (1 / ↑k) ≤ 1 / ↑N⊢ 1 / ε ≤ ↑Nh.right.convert_2ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj'''':j ≥ 1hk':↑k ≥ 0hk'':1 / ↑k ≤ 1 / ↑Nhk''':1 / ↑k ≥ 0hk'''':k ≥ 1hdist:Section_4_3.dist (1 / ↑j) (1 / ↑k) ≤ 1 / ↑N⊢ 0 < ↑N
  .h.right.convert_2ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':↑N > 0j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj'''':j ≥ 1hk':↑k ≥ 0hk'':1 / ↑k ≤ 1 / ↑Nhk''':1 / ↑k ≥ 0hk'''':k ≥ 1hdist:Section_4_3.dist (1 / ↑j) (1 / ↑k) ≤ 1 / ↑N⊢ 1 / ε ≤ ↑N exact le_of_lt hNAll goals completed! 🐙
  simp at hN' ⊢h.right.convert_2ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εj:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑Nhj':↑j ≥ 0hj'':1 / ↑j ≤ 1 / ↑Nhj''':1 / ↑j ≥ 0hj'''':j ≥ 1hk':↑k ≥ 0hk'':1 / ↑k ≤ 1 / ↑Nhk''':1 / ↑k ≥ 0hk'''':k ≥ 1hdist:Section_4_3.dist (1 / ↑j) (1 / ↑k) ≤ 1 / ↑NhN':0 < N⊢ 0 < N; assumptionAll goals completed! 🐙

abbrev BoundedBy {n:ℕ} (a: Fin n → ℚ) (M:ℚ) : Prop :=
  ∀ i, |a i| ≤ M

Визначення 5.1.12 (bounded sequences). Here we start sequences from 0 rather than 1 to align better with Mathlib conventions.

lemma BoundedBy_def {n:ℕ} (a: Fin n → ℚ) (M:ℚ) :
  BoundedBy a M ↔ ∀ i, |a i| ≤ M := byn:ℕa:Fin n → ℚM:ℚ⊢ BoundedBy a M ↔ ∀ (i : Fin n), |a i| ≤ M rflAll goals completed! 🐙

abbrev Sequence.BoundedBy (a:Sequence) (M:ℚ) : Prop :=
  ∀ n, |a n| ≤ M

Визначення 5.1.12 (bounded sequences)

lemma Sequence.BoundedBy_def (a:Sequence) (M:ℚ) :
  a.BoundedBy M ↔ ∀ n, |a n| ≤ M := bya:SequenceM:ℚ⊢ a.BoundedBy M ↔ ∀ (n : ℤ), |a.seq n| ≤ M rflAll goals completed! 🐙

abbrev Sequence.isBounded (a:Sequence) : Prop := ∃ M ≥ 0, a.BoundedBy M

Визначення 5.1.12 (bounded sequences)

lemma Sequence.isBounded_def (a:Sequence) :
  a.isBounded ↔ ∃ M ≥ 0, a.BoundedBy M := bya:Sequence⊢ a.isBounded ↔ ∃ M ≥ 0, a.BoundedBy M rflAll goals completed! 🐙

Приклад 5.1.13

declaration uses 'sorry'example : BoundedBy ![1,-2,3,-4] 4 := by⊢ BoundedBy ![1, -2, 3, -4] 4 sorryAll goals completed! 🐙

Приклад 5.1.13

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

Приклад 5.1.13

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

Приклад 5.1.13

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

Лема 5.1.14

lemma bounded_of_finite {n:ℕ} (a: Fin n → ℚ) : ∃ M ≥ 0,  BoundedBy a M := byn:ℕa:Fin n → ℚ⊢ ∃ M ≥ 0, BoundedBy a M
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  induction' n with n hnzeroa:Fin 0 → ℚ⊢ ∃ M ≥ 0, BoundedBy a Msuccn:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚ⊢ ∃ M ≥ 0, BoundedBy a M
  .zeroa:Fin 0 → ℚ⊢ ∃ M ≥ 0, BoundedBy a M use 0ha:Fin 0 → ℚ⊢ 0 ≥ 0 ∧ BoundedBy a 0
    simp [BoundedBy_def]All goals completed! 🐙
  set a' : Fin n → ℚ := fun m ↦ a msuccn:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin n → ℚ := fun m => a ↑↑m⊢ ∃ M ≥ 0, BoundedBy a M
  obtain ⟨ M, hpos, hM ⟩ := hn a'succ.intro.intron:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin n → ℚ := fun m => a ↑↑mM:ℚhpos:M ≥ 0hM:BoundedBy a' M⊢ ∃ M ≥ 0, BoundedBy a M
  have h1 : BoundedBy a' (M + |a n|) := byn:ℕa:Fin n → ℚ⊢ ∃ M ≥ 0, BoundedBy a M
    intro mn:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin n → ℚ := fun m => a ↑↑mM:ℚhpos:M ≥ 0hM:BoundedBy a' Mm:Fin n⊢ |a' m| ≤ M + |a ↑n|
    apply (hM m).transn:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin n → ℚ := fun m => a ↑↑mM:ℚhpos:M ≥ 0hM:BoundedBy a' Mm:Fin n⊢ M ≤ M + |a ↑n|
    simpAll goals completed! 🐙
  have h2 : |a n| ≤ M + |a n| := byn:ℕa:Fin n → ℚ⊢ ∃ M ≥ 0, BoundedBy a M simp [hpos]All goals completed! 🐙
  use M + |a n|hn:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin n → ℚ := fun m => a ↑↑mM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:BoundedBy a' (M + |a ↑n|)h2:|a ↑n| ≤ M + |a ↑n|⊢ M + |a ↑n| ≥ 0 ∧ BoundedBy a (M + |a ↑n|)
  constructorh.leftn:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin n → ℚ := fun m => a ↑↑mM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:BoundedBy a' (M + |a ↑n|)h2:|a ↑n| ≤ M + |a ↑n|⊢ M + |a ↑n| ≥ 0h.rightn:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin n → ℚ := fun m => a ↑↑mM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:BoundedBy a' (M + |a ↑n|)h2:|a ↑n| ≤ M + |a ↑n|⊢ BoundedBy a (M + |a ↑n|)
  .h.leftn:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin n → ℚ := fun m => a ↑↑mM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:BoundedBy a' (M + |a ↑n|)h2:|a ↑n| ≤ M + |a ↑n|⊢ M + |a ↑n| ≥ 0 positivityAll goals completed! 🐙
  intro mh.rightn:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin n → ℚ := fun m => a ↑↑mM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:BoundedBy a' (M + |a ↑n|)h2:|a ↑n| ≤ M + |a ↑n|m:Fin (n + 1)⊢ |a m| ≤ M + |a ↑n|
  rcases Fin.eq_castSucc_or_eq_last m with hm | hmh.right.inln:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin n → ℚ := fun m => a ↑↑mM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:BoundedBy a' (M + |a ↑n|)h2:|a ↑n| ≤ M + |a ↑n|m:Fin (n + 1)hm:∃ j, m = j.castSucc⊢ |a m| ≤ M + |a ↑n|h.right.inrn:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin n → ℚ := fun m => a ↑↑mM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:BoundedBy a' (M + |a ↑n|)h2:|a ↑n| ≤ M + |a ↑n|m:Fin (n + 1)hm:m = Fin.last n⊢ |a m| ≤ M + |a ↑n|
  .h.right.inln:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin n → ℚ := fun m => a ↑↑mM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:BoundedBy a' (M + |a ↑n|)h2:|a ↑n| ≤ M + |a ↑n|m:Fin (n + 1)hm:∃ j, m = j.castSucc⊢ |a m| ≤ M + |a ↑n| obtain ⟨ j, hj ⟩ := hmh.right.inl.intron:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin n → ℚ := fun m => a ↑↑mM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:BoundedBy a' (M + |a ↑n|)h2:|a ↑n| ≤ M + |a ↑n|m:Fin (n + 1)j:Fin nhj:m = j.castSucc⊢ |a m| ≤ M + |a ↑n|
    convert h1 jh.e'_3.h.e'_4.h.e'_1n:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin n → ℚ := fun m => a ↑↑mM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:BoundedBy a' (M + |a ↑n|)h2:|a ↑n| ≤ M + |a ↑n|m:Fin (n + 1)j:Fin nhj:m = j.castSucc⊢ m = ↑↑j
    simp [hj]All goals completed! 🐙
  convert h2h.e'_3.h.e'_4.h.e'_1n:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin n → ℚ := fun m => a ↑↑mM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:BoundedBy a' (M + |a ↑n|)h2:|a ↑n| ≤ M + |a ↑n|m:Fin (n + 1)hm:m = Fin.last n⊢ m = ↑n
  simp [hm]All goals completed! 🐙

Лема 5.1.15 (Cauchy sequences are bounded) / Вправа 5.1.1

lemma declaration uses 'sorry'Sequence.isBounded_of_isCauchy {a:Sequence} (h: a.isCauchy) : a.isBounded := bya:Sequenceh:a.isCauchy⊢ a.isBounded
  sorryAll goals completed! 🐙

end Chapter5