Cauchy sequences

Analysis I, Section 5.1: 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 a sequence of rationals

  • Notions of Unknown identifier `ε`ε-steadiness, eventual Unknown identifier `ε`ε-steadiness, and Cauchy sequences

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)

namespace Chapter5

Definition 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 starting from 0; Unknown identifier `ofNatFun`ofNatFun performs this conversion.

The Unknown identifier `coe`coe attribute allows the delaborator to print ↑sorry : SequenceSequence.ofNatFun Unknown identifier `f`f as ↑Unknown identifier `f`f, which is more concise; you may safely remove this if you prefer the more explicit notation.

@[coe] def Sequence.ofNatFun (a : ℕ → ℚ) : Sequence where n₀ := 0 seq n := if n ≥ 0 then a n.toNat else 0 vanish := a:ℕ → ℚ⊢ ∀ n < 0, (if n ≥ 0 then a n.toNat else 0) = 0 All goals completed! 🐙
↑fun x => ↑x ^ 2 : Sequence

If is used in a context where a Chapter5.Sequence : TypeSequence is expected, automatically coerce Unknown identifier `a`a to ↑sorry : SequenceSequence.ofNatFun Unknown identifier `a`a (which will be pretty-printed as ↑Unknown identifier `a`a)

instance : Coe (ℕ → ℚ) Sequence where coe := Sequence.ofNatFun
abbrev Sequence.mk' (n₀:ℤ) (a: { n // n ≥ n₀ } → ℚ) : Sequence where n₀ := n₀ seq n := if h : n ≥ n₀ then a ⟨n, h⟩ else 0 vanish := n₀:ℤa:{ n // n ≥ n₀ } → ℚ⊢ ∀ n < n₀, (if h : n ≥ n₀ then a ⟨n, h⟩ else 0) = 0 All goals completed! 🐙lemma Sequence.eval_mk {n n₀:ℤ} (a: { n // n ≥ n₀ } → ℚ) (h: n ≥ n₀) : (Sequence.mk' n₀ a) n = a ⟨ n, h ⟩ := n:ℤn₀:ℤa:{ n // n ≥ n₀ } → ℚh:n ≥ n₀⊢ (mk' n₀ a).seq n = a ⟨n, h⟩ All goals completed! 🐙@[simp] lemma Sequence.eval_coe (n:ℕ) (a: ℕ → ℚ) : (a:Sequence) n = a n := n:ℕa:ℕ → ℚ⊢ (↑a).seq ↑n = a n All goals completed! 🐙@[simp] lemma Sequence.eval_coe_at_int (n:ℤ) (a: ℕ → ℚ) : (a:Sequence) n = if n ≥ 0 then a n.toNat else 0 := n:ℤa:ℕ → ℚ⊢ (↑a).seq n = if n ≥ 0 then a n.toNat else 0 All goals completed! 🐙@[simp] lemma Sequence.n0_coe (a: ℕ → ℚ) : (a:Sequence).n₀ = 0 := a:ℕ → ℚ⊢ (↑a).n₀ = 0 All goals completed! 🐙

Example 5.1.2

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

Example 5.1.2

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

Example 5.1.2

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

Example 5.1.2

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

Example 5.1.2

abbrev Sequence.squares_from_three : Sequence := mk' 3 (·^2)

Example 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

A slight generalization of Definition 5.1.3 - definition of ε-steadiness for a sequence with an arbitrary starting point n₀

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) := ε:ℚa:Chapter5.Sequence⊢ ε.Steady a ↔ ∀ n ≥ a.n₀, ∀ m ≥ a.n₀, ε.Close (a.seq n) (a.seq m) All goals completed! 🐙namespace Chapter5

Definition 5.1.3 - definition of ε-steadiness for a sequence starting at 0

lemma Rat.Steady.coe (ε : ℚ) (a:ℕ → ℚ) : ε.Steady a ↔ ∀ n m : ℕ, ε.Close (a n) (a m) := ε:ℚa:ℕ → ℚ⊢ ε.Steady ↑a ↔ ∀ (n m : ℕ), ε.Close (a n) (a m) ε:ℚa:ℕ → ℚ⊢ ε.Steady ↑a → ∀ (n m : ℕ), ε.Close (a n) (a m)ε:ℚa:ℕ → ℚ⊢ (∀ (n m : ℕ), ε.Close (a n) (a m)) → ε.Steady ↑a ε:ℚa:ℕ → ℚ⊢ ε.Steady ↑a → ∀ (n m : ℕ), ε.Close (a n) (a m) ε:ℚa:ℕ → ℚh:ε.Steady ↑an:ℕm:ℕ⊢ ε.Close (a n) (a m); ε:ℚa:ℕ → ℚh:ε.Steady ↑an:ℕm:ℕ⊢ ↑n ≥ (↑a).n₀ε:ℚa:ℕ → ℚh:ε.Steady ↑an:ℕm:ℕ⊢ ↑m ≥ (↑a).n₀ε:ℚa:ℕ → ℚn:ℕm:ℕh:ε.Close ((↑a).seq ↑n) ((↑a).seq ↑m)⊢ ε.Close (a n) (a m) ε:ℚa:ℕ → ℚh:ε.Steady ↑an:ℕm:ℕ⊢ ↑n ≥ (↑a).n₀ε:ℚa:ℕ → ℚh:ε.Steady ↑an:ℕm:ℕ⊢ ↑m ≥ (↑a).n₀ε:ℚa:ℕ → ℚn:ℕm:ℕh:ε.Close ((↑a).seq ↑n) ((↑a).seq ↑m)⊢ ε.Close (a n) (a m) All goals completed! 🐙 ε:ℚa:ℕ → ℚh:∀ (n m : ℕ), ε.Close (a n) (a m)n:ℤhn:n ≥ (↑a).n₀m:ℤhm:m ≥ (↑a).n₀⊢ ε.Close ((↑a).seq n) ((↑a).seq m) ε:ℚa:ℕ → ℚh:∀ (n m : ℕ), ε.Close (a n) (a m)m:ℤhm:m ≥ (↑a).n₀n:ℕ⊢ ε.Close ((↑a).seq ↑n) ((↑a).seq m) ε:ℚa:ℕ → ℚh:∀ (n m : ℕ), ε.Close (a n) (a m)n:ℕm:ℕ⊢ ε.Close ((↑a).seq ↑n) ((↑a).seq ↑m) All goals completed! 🐙

Not in textbook: the sequence 3, 3 ... is 1-steady Intended as a demonstration of Chapter5.Rat.Steady.coe (ε : ℚ) (a : ℕ → ℚ) : ε.Steady ↑a ↔ ∀ (n m : ℕ), ε.Close (a n) (a m)Rat.Steady.coe

example : (1:ℚ).Steady ((fun _:ℕ ↦ (3:ℚ)):Sequence) := ⊢ Rat.Steady 1 ↑fun x => 3 All goals completed! 🐙

Compare: if you need to work with Rat.Steady (ε : ℚ) (a : Sequence) : PropRat.Steady on the coercion directly, there will be side conditions and that you will need to deal with.

example : (1:ℚ).Steady ((fun _:ℕ ↦ (3:ℚ)):Sequence) := ⊢ Rat.Steady 1 ↑fun x => 3 n:ℤa✝¹:n ≥ (↑fun x => 3).n₀m:ℤa✝:m ≥ (↑fun x => 3).n₀⊢ Rat.Close 1 ((↑fun x => 3).seq n) ((↑fun x => 3).seq m); All goals completed! 🐙

Example 5.1.5: The sequence is 1-steady.

example : (1:ℚ).Steady ((fun n:ℕ ↦ if Even n then (1:ℚ) else (0:ℚ)):Sequence) := ⊢ Rat.Steady 1 ↑fun n => if Even n then 1 else 0 ⊢ ∀ (n m : ℕ), Rat.Close 1 (if Even n then 1 else 0) (if Even m then 1 else 0) n:ℕm:ℕ⊢ Rat.Close 1 (if Even n then 1 else 0) (if Even m then 1 else 0) -- Split into four cases based on whether n and m are even or odd -- In each case, we know the exact value of a n and a m n:ℕm:ℕh✝¹:Even nh✝:Even m⊢ Rat.Close 1 1 1n:ℕm:ℕh✝¹:Even nh✝:¬Even m⊢ Rat.Close 1 1 0n:ℕm:ℕh✝¹:¬Even nh✝:Even m⊢ Rat.Close 1 0 1n:ℕm:ℕh✝¹:¬Even nh✝:¬Even m⊢ Rat.Close 1 0 0 n:ℕm:ℕh✝¹:Even nh✝:Even m⊢ Rat.Close 1 1 1n:ℕm:ℕh✝¹:Even nh✝:¬Even m⊢ Rat.Close 1 1 0n:ℕm:ℕh✝¹:¬Even nh✝:Even m⊢ Rat.Close 1 0 1n:ℕm:ℕh✝¹:¬Even nh✝:¬Even m⊢ Rat.Close 1 0 0 All goals completed! 🐙

Example 5.1.5: The sequence is not ½-steady.

example : ¬ (0.5:ℚ).Steady ((fun n:ℕ ↦ if Even n then (1:ℚ) else (0:ℚ)):Sequence) := ⊢ ¬Rat.Steady 0.5 ↑fun n => if Even n then 1 else 0 ⊢ ¬∀ (n m : ℕ), Rat.Close 0.5 (if Even n then 1 else 0) (if Even m then 1 else 0) h:∀ (n m : ℕ), Rat.Close 0.5 (if Even n then 1 else 0) (if Even m then 1 else 0)⊢ False; h:Rat.Close 0.5 (if Even 0 then 1 else 0) (if Even 1 then 1 else 0)⊢ False; h:1 ≤ 0.5⊢ False All goals completed! 🐙

Example 5.1.5: The sequence 0.1, 0.01, 0.001, ... is 0.1-steady.

example : (0.1:ℚ).Steady ((fun n:ℕ ↦ (10:ℚ) ^ (-(n:ℤ)-1) ):Sequence) := ⊢ Rat.Steady 0.1 ↑fun n => 10 ^ (-↑n - 1) ⊢ ∀ (n m : ℕ), Rat.Close 0.1 (10 ^ (-↑n - 1)) (10 ^ (-↑m - 1)) n:ℕm:ℕ⊢ Rat.Close 0.1 (10 ^ (-↑n - 1)) (10 ^ (-↑m - 1)); n:ℕm:ℕ⊢ |10 ^ (-↑n - 1) - 10 ^ (-↑m - 1)| ≤ 0.1 n:ℕm:ℕthis:∀ (n m : ℕ), m ≤ n → |10 ^ (-↑n - 1) - 10 ^ (-↑m - 1)| ≤ 0.1h:¬m ≤ n⊢ |10 ^ (-↑n - 1) - 10 ^ (-↑m - 1)| ≤ 0.1n:ℕm:ℕh:m ≤ n⊢ |10 ^ (-↑n - 1) - 10 ^ (-↑m - 1)| ≤ 0.1 n:ℕm:ℕthis:∀ (n m : ℕ), m ≤ n → |10 ^ (-↑n - 1) - 10 ^ (-↑m - 1)| ≤ 0.1h:¬m ≤ n⊢ |10 ^ (-↑n - 1) - 10 ^ (-↑m - 1)| ≤ 0.1 specialize this m n (n:ℕm:ℕthis:∀ (n m : ℕ), m ≤ n → |10 ^ (-↑n - 1) - 10 ^ (-↑m - 1)| ≤ 0.1h:¬m ≤ n⊢ n ≤ m All goals completed! 🐙); rwa [abs_sub_commn:ℕm:ℕh:¬m ≤ nthis:|10 ^ (-↑m - 1) - 10 ^ (-↑n - 1)| ≤ 0.1⊢ |10 ^ (-↑m - 1) - 10 ^ (-↑n - 1)| ≤ 0.1 n:ℕm:ℕh:m ≤ n⊢ 10 ^ (-↑m - 1) - 10 ^ (-↑n - 1) ≤ 0.1n:ℕm:ℕh:m ≤ n⊢ 0 ≤ 10 ^ (-↑m - 1) - 10 ^ (-↑n - 1) n:ℕm:ℕh:m ≤ n⊢ 10 ^ (-↑m - 1) - 10 ^ (-↑n - 1) ≤ 0.1 n:ℕm:ℕh:m ≤ n⊢ 10 ^ (-↑m - 1) - 10 ^ (-↑n - 1) ≤ 10 ^ (-1) - 0 n:ℕm:ℕh:m ≤ n⊢ 1 ≤ 10n:ℕm:ℕh:m ≤ n⊢ -↑m - 1 ≤ -1n:ℕm:ℕh:m ≤ n⊢ 0 ≤ 10 ^ (-↑n - 1) n:ℕm:ℕh:m ≤ n⊢ 1 ≤ 10n:ℕm:ℕh:m ≤ n⊢ -↑m - 1 ≤ -1n:ℕm:ℕh:m ≤ n⊢ 0 ≤ 10 ^ (-↑n - 1) try n:ℕm:ℕh:m ≤ n⊢ 0 ≤ 10 ^ (-↑n - 1) All goals completed! 🐙 linarith [show (10:ℚ) ^ (-(n:ℤ)-1) ≤ (10:ℚ) ^ (-(m:ℤ)-1) ⊢ Rat.Steady 0.1 ↑fun n => 10 ^ (-↑n - 1) n:ℕm:ℕh:m ≤ n⊢ 1 ≤ 10; All goals completed! 🐙]

Example 5.1.5: The sequence 0.1, 0.01, 0.001, ... is not 0.01-steady. Left as an exercise.

declaration uses 'sorry'example : ¬(0.01:ℚ).Steady ((fun n:ℕ ↦ (10:ℚ) ^ (-(n:ℤ)-1) ):Sequence) := ⊢ ¬Rat.Steady 1e-2 ↑fun n => 10 ^ (-↑n - 1) All goals completed! 🐙

Example 5.1.5: The sequence 1, 2, 4, 8, ... is not ε-steady for any ε. Left as an exercise.

declaration uses 'sorry'example (ε:ℚ) : ¬ ε.Steady ((fun n:ℕ ↦ (2 ^ (n+1):ℚ) ):Sequence) := ε:ℚ⊢ ¬ε.Steady ↑fun n => 2 ^ (n + 1) All goals completed! 🐙

Example 5.1.5:The sequence 2, 2, 2, ... is ε-steady for any ε > 0.

example (ε:ℚ) (hε: ε>0) : ε.Steady ((fun _:ℕ ↦ (2:ℚ) ):Sequence) := ε:ℚhε:ε > 0⊢ ε.Steady ↑fun x => 2 ε:ℚhε:ε > 0⊢ ∀ (n m : ℕ), ε.Close 2 2; ε:ℚhε:ε > 0⊢ 0 ≤ ε; All goals completed! 🐙

The sequence 10, 0, 0, ... is 10-steady.

example : (10:ℚ).Steady ((fun n:ℕ ↦ if n = 0 then (10:ℚ) else (0:ℚ)):Sequence) := ⊢ Rat.Steady 10 ↑fun n => if n = 0 then 10 else 0 ⊢ ∀ (n m : ℕ), Rat.Close 10 (if n = 0 then 10 else 0) (if m = 0 then 10 else 0); n:ℕm:ℕ⊢ Rat.Close 10 (if n = 0 then 10 else 0) (if m = 0 then 10 else 0) -- Split into 4 cases based on whether n and m are 0 or not n:ℕm:ℕh✝¹:n = 0h✝:m = 0⊢ Rat.Close 10 10 10n:ℕm:ℕh✝¹:n = 0h✝:¬m = 0⊢ Rat.Close 10 10 0n:ℕm:ℕh✝¹:¬n = 0h✝:m = 0⊢ Rat.Close 10 0 10n:ℕm:ℕh✝¹:¬n = 0h✝:¬m = 0⊢ Rat.Close 10 0 0 n:ℕm:ℕh✝¹:n = 0h✝:m = 0⊢ Rat.Close 10 10 10n:ℕm:ℕh✝¹:n = 0h✝:¬m = 0⊢ Rat.Close 10 10 0n:ℕm:ℕh✝¹:¬n = 0h✝:m = 0⊢ Rat.Close 10 0 10n:ℕm:ℕh✝¹:¬n = 0h✝:¬m = 0⊢ Rat.Close 10 0 0 All goals completed! 🐙

The sequence 10, 0, 0, ... is not ε-steady for any smaller value of ε.

example (ε:ℚ) (hε:ε<10): ¬ ε.Steady ((fun n:ℕ ↦ if n = 0 then (10:ℚ) else (0:ℚ)):Sequence) := ε:ℚhε:ε < 10⊢ ¬ε.Steady ↑fun n => if n = 0 then 10 else 0 ε:ℚhε:ε.Steady ↑fun n => if n = 0 then 10 else 0⊢ 10 ≤ ε; ε:ℚhε:∀ (n m : ℕ), ε.Close (if n = 0 then 10 else 0) (if m = 0 then 10 else 0)⊢ 10 ≤ ε; ε:ℚhε:ε.Close (if 0 = 0 then 10 else 0) (if 1 = 0 then 10 else 0)⊢ 10 ≤ ε; All 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 := a:Sequencen₁:ℤn:ℤhn:n ≥ n₁⊢ (a.from n₁).seq n = a.seq n a:Sequencen₁:ℤn:ℤhn:n ≥ n₁⊢ n < a.n₀ → 0 = a.seq n; a:Sequencen₁:ℤn:ℤhn:n ≥ n₁h:n < a.n₀⊢ 0 = a.seq n; All goals completed! 🐙end Chapter5

Definition 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) := ε:ℚa:Chapter5.Sequence⊢ ε.EventuallySteady a ↔ ∃ N ≥ a.n₀, ε.Steady (a.from N) All goals completed! 🐙namespace Chapter5

Example 5.1.7: The sequence 1, 1/2, 1/3, ... is not 0.1-steady

lemma Sequence.ex_5_1_7_a : ¬ (0.1:ℚ).Steady ((fun n:ℕ ↦ (n+1:ℚ)⁻¹ ):Sequence) := ⊢ ¬Rat.Steady 0.1 ↑fun n => (↑n + 1)⁻¹ h:Rat.Steady 0.1 ↑fun n => (↑n + 1)⁻¹⊢ False; h:∀ (n m : ℕ), Rat.Close 0.1 (↑n + 1)⁻¹ (↑m + 1)⁻¹⊢ False; h:Rat.Close 0.1 (↑0 + 1)⁻¹ (↑2 + 1)⁻¹⊢ False; h:|1 - (2 + 1)⁻¹| ≤ 0.1⊢ False; h:|2 / 3| ≤ 1 / 10⊢ False h:2 / 3 ≤ 1 / 10⊢ Falseh:|2 / 3| ≤ 1 / 10⊢ 0 ≤ 2 / 3 h:2 / 3 ≤ 1 / 10⊢ Falseh:|2 / 3| ≤ 1 / 10⊢ 0 ≤ 2 / 3 All goals completed! 🐙

Example 5.1.7: The sequence a_10, a_11, a_12, ... is 0.1-steady

lemma Sequence.ex_5_1_7_b : (0.1:ℚ).Steady (((fun n:ℕ ↦ (n+1:ℚ)⁻¹ ):Sequence).from 10) := ⊢ Rat.Steady 0.1 ((↑fun n => (↑n + 1)⁻¹).from 10) ⊢ ∀ n ≥ ((↑fun n => (↑n + 1)⁻¹).from 10).n₀, ∀ m ≥ ((↑fun n => (↑n + 1)⁻¹).from 10).n₀, Rat.Close 0.1 (((↑fun n => (↑n + 1)⁻¹).from 10).seq n) (((↑fun n => (↑n + 1)⁻¹).from 10).seq m) n:ℤhn:n ≥ ((↑fun n => (↑n + 1)⁻¹).from 10).n₀m:ℤhm:m ≥ ((↑fun n => (↑n + 1)⁻¹).from 10).n₀⊢ Rat.Close 0.1 (((↑fun n => (↑n + 1)⁻¹).from 10).seq n) (((↑fun n => (↑n + 1)⁻¹).from 10).seq m); n:ℤm:ℤhn:10 ≤ nhm:10 ≤ m⊢ Rat.Close 0.1 (((↑fun n => (↑n + 1)⁻¹).from 10).seq n) (((↑fun n => (↑n + 1)⁻¹).from 10).seq m) lift n to ℕ using (n:ℤm:ℤhn:10 ≤ nhm:10 ≤ m⊢ 0 ≤ n All goals completed! 🐙) lift m to ℕ using (m:ℤhm:10 ≤ mn:ℕhn:10 ≤ ↑n⊢ 0 ≤ m All goals completed! 🐙) n:ℕm:ℕhn:10 ≤ nhm:10 ≤ m⊢ |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1 n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mthis:∀ (n m : ℕ), 10 ≤ n → 10 ≤ m → m ≤ n → |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1h:¬m ≤ n⊢ |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:m ≤ n⊢ |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1 n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mthis:∀ (n m : ℕ), 10 ≤ n → 10 ≤ m → m ≤ n → |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1h:¬m ≤ n⊢ |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1 n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mthis:∀ (n m : ℕ), 10 ≤ n → 10 ≤ m → m ≤ n → |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1h:¬m ≤ n⊢ 10 ≤ mn:ℕm:ℕhn:10 ≤ nhm:10 ≤ mthis:∀ (n m : ℕ), 10 ≤ n → 10 ≤ m → m ≤ n → |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1h:¬m ≤ n⊢ 10 ≤ nn:ℕm:ℕhn:10 ≤ nhm:10 ≤ mthis:∀ (n m : ℕ), 10 ≤ n → 10 ≤ m → m ≤ n → |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1h:¬m ≤ n⊢ n ≤ mn:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:¬m ≤ nthis:|(↑m + 1)⁻¹ - (↑n + 1)⁻¹| ≤ 0.1⊢ |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1 n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mthis:∀ (n m : ℕ), 10 ≤ n → 10 ≤ m → m ≤ n → |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1h:¬m ≤ n⊢ 10 ≤ mn:ℕm:ℕhn:10 ≤ nhm:10 ≤ mthis:∀ (n m : ℕ), 10 ≤ n → 10 ≤ m → m ≤ n → |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1h:¬m ≤ n⊢ 10 ≤ nn:ℕm:ℕhn:10 ≤ nhm:10 ≤ mthis:∀ (n m : ℕ), 10 ≤ n → 10 ≤ m → m ≤ n → |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1h:¬m ≤ n⊢ n ≤ mn:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:¬m ≤ nthis:|(↑m + 1)⁻¹ - (↑n + 1)⁻¹| ≤ 0.1⊢ |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1 try All goals completed! 🐙 rwa [abs_sub_commn:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:¬m ≤ nthis:|(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1⊢ |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1 at this n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:m ≤ n⊢ |(↑m + 1)⁻¹ - (↑n + 1)⁻¹| ≤ 0.1 have : ((n:ℚ) + 1)⁻¹ ≤ ((m:ℚ) + 1)⁻¹ := ⊢ Rat.Steady 0.1 ((↑fun n => (↑n + 1)⁻¹).from 10) All goals completed! 🐙 n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:m ≤ nthis:(↑_fvar.85687 + 1)⁻¹ ≤ (↑_fvar.85688 + 1)⁻¹ := ?_mvar.86752⊢ (↑m + 1)⁻¹ - (↑n + 1)⁻¹ ≤ 10⁻¹ - 0 n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:m ≤ nthis:(↑_fvar.85687 + 1)⁻¹ ≤ (↑_fvar.85688 + 1)⁻¹ := ?_mvar.86752⊢ 10 ≤ ↑m + 1n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:m ≤ nthis:(↑_fvar.85687 + 1)⁻¹ ≤ (↑_fvar.85688 + 1)⁻¹ := ?_mvar.86752⊢ 0 ≤ (↑n + 1)⁻¹ n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:m ≤ nthis:(↑_fvar.85687 + 1)⁻¹ ≤ (↑_fvar.85688 + 1)⁻¹ := ?_mvar.86752⊢ 10 ≤ ↑m + 1 n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:m ≤ nthis:(↑_fvar.85687 + 1)⁻¹ ≤ (↑_fvar.85688 + 1)⁻¹ := ?_mvar.86752⊢ 10 ≤ m + 1; All goals completed! 🐙 All goals completed! 🐙

Example 5.1.7: The sequence 1, 1/2, 1/3, ... is eventually 0.1-steady

lemma Sequence.ex_5_1_7_c : (0.1:ℚ).EventuallySteady ((fun n:ℕ ↦ (n+1:ℚ)⁻¹ ):Sequence) := ⟨10, ⊢ 10 ≥ (↑fun n => (↑n + 1)⁻¹).n₀ All goals completed! 🐙, ex_5_1_7_b⟩

Example 5.1.7

The sequence 10, 0, 0, ... is eventually ε-steady for every ε > 0. Left as an exercise.

lemma declaration uses 'sorry'Sequence.ex_5_1_7_d {ε:ℚ} (hε:ε>0) : ε.EventuallySteady ((fun n:ℕ ↦ if n=0 then (10:ℚ) else (0:ℚ) ):Sequence) := ε:ℚhε:ε > 0⊢ ε.EventuallySteady ↑fun n => if n = 0 then 10 else 0 All goals completed! 🐙
abbrev Sequence.IsCauchy (a:Sequence) : Prop := ∀ ε > (0:ℚ), ε.EventuallySteady alemma Sequence.isCauchy_def (a:Sequence) : a.IsCauchy ↔ ∀ ε > (0:ℚ), ε.EventuallySteady a := a:Sequence⊢ a.IsCauchy ↔ ∀ ε > 0, ε.EventuallySteady a All goals completed! 🐙

Definition of Cauchy sequences, for a sequence starting at 0

lemma Sequence.IsCauchy.coe (a:ℕ → ℚ) : (a:Sequence).IsCauchy ↔ ∀ ε > (0:ℚ), ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε := a:ℕ → ℚ⊢ (↑a).IsCauchy ↔ ∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε a:ℕ → ℚ⊢ (↑a).IsCauchy → ∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εa:ℕ → ℚ⊢ (∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε) → (↑a).IsCauchy a:ℕ → ℚ⊢ (↑a).IsCauchy → ∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εa:ℕ → ℚ⊢ (∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε) → (↑a).IsCauchy a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0⊢ ε.EventuallySteady ↑a a:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε a:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ (↑a).n₀h':ε.Steady ((↑a).from N)⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε a:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕh':ε.Steady ((↑a).from ↑N)⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε; a:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕh':ε.Steady ((↑a).from ↑N)⊢ ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε a:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕh':ε.Steady ((↑a).from ↑N)j:ℕa✝¹:j ≥ Nk:ℕa✝:k ≥ N⊢ Section_4_3.dist (a j) (a k) ≤ ε; a:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕj:ℕa✝¹:j ≥ Nk:ℕa✝:k ≥ Nh':∀ (n : ℤ), ↑N ≤ n → ∀ (m : ℤ), ↑N ≤ m → ε.Close (if ↑N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0) (if ↑N ≤ m then if 0 ≤ m then a m.toNat else 0 else 0)⊢ Section_4_3.dist (a j) (a k) ≤ ε; a:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕj:ℕa✝¹:j ≥ Nk:ℕa✝:k ≥ Nh':∀ (n : ℤ), ↑N ≤ n → ∀ (m : ℤ), ↑N ≤ m → ε.Close (if ↑N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0) (if ↑N ≤ m then if 0 ≤ m then a m.toNat else 0 else 0)⊢ ↑N ≤ ↑ja:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕj:ℕa✝¹:j ≥ Nk:ℕa✝:k ≥ Nh':∀ (n : ℤ), ↑N ≤ n → ∀ (m : ℤ), ↑N ≤ m → ε.Close (if ↑N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0) (if ↑N ≤ m then if 0 ≤ m then a m.toNat else 0 else 0)⊢ ↑N ≤ ↑ka:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕj:ℕa✝¹:j ≥ Nk:ℕa✝:k ≥ Nh':ε.Close (if ↑N ≤ ↑j then if 0 ≤ ↑j then a (↑j).toNat else 0 else 0) (if ↑N ≤ ↑k then if 0 ≤ ↑k then a (↑k).toNat else 0 else 0)⊢ Section_4_3.dist (a j) (a k) ≤ ε a:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕj:ℕa✝¹:j ≥ Nk:ℕa✝:k ≥ Nh':∀ (n : ℤ), ↑N ≤ n → ∀ (m : ℤ), ↑N ≤ m → ε.Close (if ↑N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0) (if ↑N ≤ m then if 0 ≤ m then a m.toNat else 0 else 0)⊢ ↑N ≤ ↑ja:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕj:ℕa✝¹:j ≥ Nk:ℕa✝:k ≥ Nh':∀ (n : ℤ), ↑N ≤ n → ∀ (m : ℤ), ↑N ≤ m → ε.Close (if ↑N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0) (if ↑N ≤ m then if 0 ≤ m then a m.toNat else 0 else 0)⊢ ↑N ≤ ↑ka:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕj:ℕa✝¹:j ≥ Nk:ℕa✝:k ≥ Nh':ε.Close (if ↑N ≤ ↑j then if 0 ≤ ↑j then a (↑j).toNat else 0 else 0) (if ↑N ≤ ↑k then if 0 ≤ ↑k then a (↑k).toNat else 0 else 0)⊢ Section_4_3.dist (a j) (a k) ≤ ε try All goals completed! 🐙 a:ℕ → ℚh:(↑a).IsCauchyε:ℚN:ℕj:ℕk:ℕhε:0 < εa✝¹:N ≤ ja✝:N ≤ kh':ε.Close (a j) (a k)⊢ Section_4_3.dist (a j) (a k) ≤ ε; All goals completed! 🐙 a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε⊢ ε.EventuallySteady ↑a refine ⟨ max N 0, a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε⊢ max (↑N) 0 ≥ (↑a).n₀ All goals completed! 🐙, ?_ ⟩ a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤhn:n ≥ ((↑a).from (max (↑N) 0)).n₀m:ℤhm:m ≥ ((↑a).from (max (↑N) 0)).n₀⊢ ε.Close (((↑a).from (max (↑N) 0)).seq n) (((↑a).from (max (↑N) 0)).seq m); a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ ε.Close (((↑a).from (max (↑N) 0)).seq n) (((↑a).from (max (↑N) 0)).seq m) a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ mnpos:0 ≤ _fvar.131394 := ?_mvar.137582⊢ ε.Close (((↑a).from (max (↑N) 0)).seq n) (((↑a).from (max (↑N) 0)).seq m)a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ 0 ≤ n a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ mnpos:0 ≤ _fvar.131394 := ?_mvar.137582mpos:0 ≤ _fvar.131400 := ?_mvar.137624⊢ ε.Close (((↑a).from (max (↑N) 0)).seq n) (((↑a).from (max (↑N) 0)).seq m)a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ mnpos:0 ≤ _fvar.131394 := ?_mvar.137582⊢ 0 ≤ ma:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ 0 ≤ n a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εm:ℤhm:↑N ≤ mmpos:0 ≤ _fvar.131400 := ?_mvar.137624n:ℕhn:↑N ≤ ↑n⊢ ε.Close (((↑a).from (max (↑N) 0)).seq ↑n) (((↑a).from (max (↑N) 0)).seq m)a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ mnpos:0 ≤ _fvar.131394 := ?_mvar.137582⊢ 0 ≤ ma:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ 0 ≤ n a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℕhn:↑N ≤ ↑nm:ℕhm:↑N ≤ ↑m⊢ ε.Close (((↑a).from (max (↑N) 0)).seq ↑n) (((↑a).from (max (↑N) 0)).seq ↑m)a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ mnpos:0 ≤ _fvar.131394 := ?_mvar.137582⊢ 0 ≤ ma:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ 0 ≤ n a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℕhn:↑N ≤ ↑nm:ℕhm:↑N ≤ ↑m⊢ ε.Close (a n) (a m)a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ mnpos:0 ≤ _fvar.131394 := ?_mvar.137582⊢ 0 ≤ ma:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ 0 ≤ n; a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℕhn:↑N ≤ ↑nm:ℕhm:↑N ≤ ↑m⊢ n ≥ Na:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℕhn:↑N ≤ ↑nm:ℕhm:↑N ≤ ↑m⊢ m ≥ Na:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕn:ℕhn:↑N ≤ ↑nm:ℕhm:↑N ≤ ↑mh':Section_4_3.dist (a n) (a m) ≤ ε⊢ ε.Close (a n) (a m)a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ mnpos:0 ≤ _fvar.131394 := ?_mvar.137582⊢ 0 ≤ ma:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ 0 ≤ n all_goals try All goals completed! 🐙 All goals completed! 🐙
lemma Sequence.IsCauchy.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) ≤ ε := n₀:ℤ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) ≤ ε n₀:ℤ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) ≤ εn₀:ℤa:{ n // n ≥ n₀ } → ℚ⊢ (∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε) → (mk' n₀ a).IsCauchy n₀:ℤ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) ≤ εn₀:ℤa:{ n // n ≥ n₀ } → ℚ⊢ (∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε) → (mk' n₀ a).IsCauchy n₀:ℤa:{ n // n ≥ n₀ } → ℚh:∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εε:ℚhε:ε > 0⊢ ε.EventuallySteady (mk' n₀ a) n₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0⊢ ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εn₀:ℤa:{ n // n ≥ n₀ } → ℚh:∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εε:ℚhε:ε > 0⊢ ε.EventuallySteady (mk' n₀ a) n₀:ℤa:{ n // n ≥ n₀ } → ℚh:∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εε:ℚhε:ε > 0N:ℤhN:N ≥ n₀h':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε⊢ ε.EventuallySteady (mk' n₀ a) n₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ (mk' n₀ a).n₀h':ε.Steady ((mk' n₀ a).from N)⊢ ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε n₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ (mk' n₀ a).n₀h':ε.Steady ((mk' n₀ a).from N)⊢ ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε; n₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀h':ε.Steady ((mk' n₀ a).from N)⊢ ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε; n₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀h':ε.Steady ((mk' n₀ a).from N)j:ℤa✝¹:j ≥ Nk:ℤa✝:k ≥ N⊢ Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε n₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀j:ℤa✝¹:j ≥ Nk:ℤa✝:k ≥ Nh':∀ n ≥ N, ∀ m ≥ N, ε.Close (if h : n ≥ N then if h_1 : n ≥ n₀ then a ⟨n, ⋯⟩ else 0 else 0) (if h : m ≥ N then if h_1 : m ≥ n₀ then a ⟨m, ⋯⟩ else 0 else 0)⊢ Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε n₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀j:ℤa✝¹:j ≥ Nk:ℤa✝:k ≥ Nh':∀ n ≥ N, ∀ m ≥ N, ε.Close (if h : n ≥ N then if h_1 : n ≥ n₀ then a ⟨n, ⋯⟩ else 0 else 0) (if h : m ≥ N then if h_1 : m ≥ n₀ then a ⟨m, ⋯⟩ else 0 else 0)⊢ j ≥ Nn₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀j:ℤa✝¹:j ≥ Nk:ℤa✝:k ≥ Nh':∀ n ≥ N, ∀ m ≥ N, ε.Close (if h : n ≥ N then if h_1 : n ≥ n₀ then a ⟨n, ⋯⟩ else 0 else 0) (if h : m ≥ N then if h_1 : m ≥ n₀ then a ⟨m, ⋯⟩ else 0 else 0)⊢ k ≥ Nn₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀j:ℤa✝¹:j ≥ Nk:ℤa✝:k ≥ Nh':ε.Close (if h : j ≥ N then if h_1 : j ≥ n₀ then a ⟨j, ⋯⟩ else 0 else 0) (if h : k ≥ N then if h_1 : k ≥ n₀ then a ⟨k, ⋯⟩ else 0 else 0)⊢ Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε n₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀j:ℤa✝¹:j ≥ Nk:ℤa✝:k ≥ Nh':∀ n ≥ N, ∀ m ≥ N, ε.Close (if h : n ≥ N then if h_1 : n ≥ n₀ then a ⟨n, ⋯⟩ else 0 else 0) (if h : m ≥ N then if h_1 : m ≥ n₀ then a ⟨m, ⋯⟩ else 0 else 0)⊢ j ≥ Nn₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀j:ℤa✝¹:j ≥ Nk:ℤa✝:k ≥ Nh':∀ n ≥ N, ∀ m ≥ N, ε.Close (if h : n ≥ N then if h_1 : n ≥ n₀ then a ⟨n, ⋯⟩ else 0 else 0) (if h : m ≥ N then if h_1 : m ≥ n₀ then a ⟨m, ⋯⟩ else 0 else 0)⊢ k ≥ Nn₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀j:ℤa✝¹:j ≥ Nk:ℤa✝:k ≥ Nh':ε.Close (if h : j ≥ N then if h_1 : j ≥ n₀ then a ⟨j, ⋯⟩ else 0 else 0) (if h : k ≥ N then if h_1 : k ≥ n₀ then a ⟨k, ⋯⟩ else 0 else 0)⊢ Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε try All goals completed! 🐙 simp_all [show n₀ ≤ j n₀:ℤ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) ≤ ε All goals completed! 🐙, show n₀ ≤ k n₀:ℤ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) ≤ ε All goals completed! 🐙] All goals completed! 🐙 refine ⟨ max n₀ N, n₀:ℤa:{ n // n ≥ n₀ } → ℚh:∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εε:ℚhε:ε > 0N:ℤhN:N ≥ n₀h':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε⊢ max n₀ N ≥ (mk' n₀ a).n₀ All goals completed! 🐙, ?_ ⟩ n₀:ℤa:{ n // n ≥ n₀ } → ℚh:∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εε:ℚhε:ε > 0N:ℤhN:N ≥ n₀h':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εn:ℤa✝¹:n ≥ ((mk' n₀ a).from (max n₀ N)).n₀m:ℤa✝:m ≥ ((mk' n₀ a).from (max n₀ N)).n₀⊢ ε.Close (((mk' n₀ a).from (max n₀ N)).seq n) (((mk' n₀ a).from (max n₀ N)).seq m); n₀:ℤa:{ n // n ≥ n₀ } → ℚε:ℚN:ℤhN✝:N ≥ n₀n:ℤa✝³:n ≥ ((mk' n₀ a).from (max n₀ N)).n₀m:ℤa✝²:m ≥ ((mk' n₀ a).from (max n₀ N)).n₀h:∀ (ε : ℚ), 0 < ε → ∃ N, n₀ ≤ N ∧ ∀ (j : ℤ), N ≤ j → ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εhε:0 < εhN:n₀ ≤ Nh':∀ (j : ℤ), N ≤ j → ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εa✝¹:N ≤ na✝:N ≤ m⊢ ε.Close (if h : n₀ ≤ n then a ⟨n, ⋯⟩ else 0) (if h : n₀ ≤ m then a ⟨m, ⋯⟩ else 0) n₀:ℤa:{ n // n ≥ n₀ } → ℚε:ℚN:ℤhN✝:N ≥ n₀n:ℤa✝³:n ≥ ((mk' n₀ a).from (max n₀ N)).n₀m:ℤa✝²:m ≥ ((mk' n₀ a).from (max n₀ N)).n₀h:∀ (ε : ℚ), 0 < ε → ∃ N, n₀ ≤ N ∧ ∀ (j : ℤ), N ≤ j → ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εhε:0 < εhN:n₀ ≤ Nh':∀ (j : ℤ), N ≤ j → ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εa✝¹:N ≤ na✝:N ≤ m⊢ N ≤ mn₀:ℤa:{ n // n ≥ n₀ } → ℚε:ℚN:ℤhN✝:N ≥ n₀n:ℤa✝³:n ≥ ((mk' n₀ a).from (max n₀ N)).n₀m:ℤa✝²:m ≥ ((mk' n₀ a).from (max n₀ N)).n₀h:∀ (ε : ℚ), 0 < ε → ∃ N, n₀ ≤ N ∧ ∀ (j : ℤ), N ≤ j → ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εhε:0 < εhN:n₀ ≤ Nh':∀ (j : ℤ), N ≤ j → ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εa✝¹:N ≤ na✝:N ≤ m⊢ N ≤ n n₀:ℤa:{ n // n ≥ n₀ } → ℚε:ℚN:ℤhN✝:N ≥ n₀n:ℤa✝³:n ≥ ((mk' n₀ a).from (max n₀ N)).n₀m:ℤa✝²:m ≥ ((mk' n₀ a).from (max n₀ N)).n₀h:∀ (ε : ℚ), 0 < ε → ∃ N, n₀ ≤ N ∧ ∀ (j : ℤ), N ≤ j → ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εhε:0 < εhN:n₀ ≤ Nh':∀ (j : ℤ), N ≤ j → ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εa✝¹:N ≤ na✝:N ≤ m⊢ N ≤ mn₀:ℤa:{ n // n ≥ n₀ } → ℚε:ℚN:ℤhN✝:N ≥ n₀n:ℤa✝³:n ≥ ((mk' n₀ a).from (max n₀ N)).n₀m:ℤa✝²:m ≥ ((mk' n₀ a).from (max n₀ N)).n₀h:∀ (ε : ℚ), 0 < ε → ∃ N, n₀ ≤ N ∧ ∀ (j : ℤ), N ≤ j → ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εhε:0 < εhN:n₀ ≤ Nh':∀ (j : ℤ), N ≤ j → ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εa✝¹:N ≤ na✝:N ≤ m⊢ N ≤ n All goals completed! 🐙noncomputable def Sequence.sqrt_two : Sequence := (fun n:ℕ ↦ ((⌊ (Real.sqrt 2)*10^n ⌋ / 10^n):ℚ))

Example 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 := ⊢ Rat.Steady 1 sqrt_two All goals completed! 🐙

Example 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) := ⊢ Rat.Steady 0.1 (sqrt_two.from 1) All goals completed! 🐙
theorem declaration uses 'sorry'Sequence.ex_5_1_10_c : (0.1:ℚ).EventuallySteady sqrt_two := ⊢ Rat.EventuallySteady 0.1 sqrt_two All goals completed! 🐙

Proposition 5.1.11. The harmonic sequence, defined as a₁ = 1, a₂ = 1/2, ... is a Cauchy sequence.

theorem Sequence.IsCauchy.harmonic : (mk' 1 (fun n ↦ (1:ℚ)/n)).IsCauchy := ⊢ (mk' 1 fun n => 1 / ↑↑n).IsCauchy ⊢ ∀ ε > 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) ≤ ε ε:ℚ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) ≤ ε -- We go by reverse from the book - first choose N such that N > 1/ε ε:ℚ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 := ⊢ (mk' 1 fun n => 1 / ↑↑n).IsCauchy ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εthis:0 < 1 / ε⊢ N > 0 ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εthis✝:0 < 1 / εthis:0 < ↑N⊢ N > 0 All goals completed! 🐙 refine ⟨ N, ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':_fvar.250039 > 0 := Eq.mp (Eq.trans (congrArg (fun x => x < ↑_fvar.250039) (Eq.symm Nat.cast_zero)) Nat.cast_lt._simp_1) (gt_trans _fvar.250040 (one_div_pos.mpr _fvar.249878))⊢ ↑N ≥ 1 All goals completed! 🐙, ?_ ⟩ ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':_fvar.250039 > 0 := ?_mvar.251160j:ℤ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) ≤ ε lift j to ℕ using (ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':_fvar.250039 > 0 := Eq.mp (Eq.trans (congrArg (fun x => x < ↑_fvar.250039) (Eq.symm Nat.cast_zero)) Nat.cast_lt._simp_1) (gt_trans _fvar.250040 (one_div_pos.mpr _fvar.249878))j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑N⊢ 0 ≤ j All goals completed! 🐙) lift k to ℕ using (ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':_fvar.250039 > 0 := Eq.mp (Eq.trans (congrArg (fun x => x < ↑_fvar.250039) (Eq.symm Nat.cast_zero)) Nat.cast_lt._simp_1) (gt_trans _fvar.250040 (one_div_pos.mpr _fvar.249878))k:ℤhk:k ≥ ↑Nj:ℕhj:↑j ≥ ↑N⊢ 0 ≤ k All goals completed! 🐙) ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':_fvar.250039 > 0 := ?_mvar.251160j:ℕk:ℕhj:N ≤ jhk:N ≤ k⊢ Section_4_3.dist ((mk' 1 fun n => 1 / ↑↑n).seq ↑j) ((mk' 1 fun n => 1 / ↑↑n).seq ↑k) ≤ ε ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':_fvar.250039 > 0 := ?_mvar.251160j:ℕk:ℕhj:N ≤ jhk:N ≤ k⊢ Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ ε have hdist : Section_4_3.dist ((1:ℚ)/j) ((1:ℚ)/k) ≤ (1:ℚ)/N := ⊢ (mk' 1 fun n => 1 / ↑↑n).IsCauchy ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':_fvar.250039 > 0 := ?_mvar.251160j:ℕk:ℕhj:N ≤ jhk:N ≤ k⊢ 1 / ↑j - 1 / ↑k ≤ 1 / ↑N ∧ -(1 / ↑j - 1 / ↑k) ≤ 1 / ↑N /- We establish the following bounds: - 1/j ∈ [0, 1/N] - 1/k ∈ [0, 1/N] These imply that the distance between 1/j and 1/k is at most 1/N - when they are as "far apart" as possible. -/ have : 1/j ≤ (1:ℚ)/N := ⊢ (mk' 1 fun n => 1 / ↑↑n).IsCauchy All goals completed! 🐙 ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':_fvar.250039 > 0 := ?_mvar.251160j:ℕk:ℕhj:N ≤ jhk:N ≤ kthis✝:1 / ↑_fvar.497087 ≤ 1 / ↑_fvar.250039 := ?_mvar.514962this:0 ≤ 1 / ↑j⊢ 1 / ↑j - 1 / ↑k ≤ 1 / ↑N ∧ -(1 / ↑j - 1 / ↑k) ≤ 1 / ↑N have : 1/k ≤ (1:ℚ)/N := ⊢ (mk' 1 fun n => 1 / ↑↑n).IsCauchy All goals completed! 🐙 ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':_fvar.250039 > 0 := ?_mvar.251160j:ℕk:ℕhj:N ≤ jhk:N ≤ kthis✝²:1 / ↑_fvar.497087 ≤ 1 / ↑_fvar.250039 := ?_mvar.514962this✝¹:0 ≤ 1 / ↑jthis✝:1 / ↑_fvar.499385 ≤ 1 / ↑_fvar.250039 := ?_mvar.529008this:0 ≤ 1 / ↑k⊢ 1 / ↑j - 1 / ↑k ≤ 1 / ↑N ∧ -(1 / ↑j - 1 / ↑k) ≤ 1 / ↑N All goals completed! 🐙 ε:ℚN:ℕj:ℕk:ℕhj:N ≤ jhk:N ≤ khε:0 < εhN:ε⁻¹ < ↑NhN':0 < Nhdist:Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ (↑N)⁻¹⊢ Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ ε; ε:ℚN:ℕj:ℕk:ℕhj:N ≤ jhk:N ≤ khε:0 < εhN:ε⁻¹ < ↑NhN':0 < Nhdist:Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ (↑N)⁻¹⊢ (↑N)⁻¹ ≤ ε ε:ℚN:ℕj:ℕk:ℕhj:N ≤ jhk:N ≤ khε:0 < εhN:ε⁻¹ < ↑NhN':0 < Nhdist:Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ (↑N)⁻¹⊢ ε⁻¹ ≤ ↑Nε:ℚN:ℕj:ℕk:ℕhj:N ≤ jhk:N ≤ khε:0 < εhN:ε⁻¹ < ↑NhN':0 < Nhdist:Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ (↑N)⁻¹⊢ 0 < ↑Nε:ℚN:ℕj:ℕk:ℕhj:N ≤ jhk:N ≤ khε:0 < εhN:ε⁻¹ < ↑NhN':0 < Nhdist:Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ (↑N)⁻¹⊢ 0 < ε ε:ℚN:ℕj:ℕk:ℕhj:N ≤ jhk:N ≤ khε:0 < εhN:ε⁻¹ < ↑NhN':0 < Nhdist:Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ (↑N)⁻¹⊢ ε⁻¹ ≤ ↑Nε:ℚN:ℕj:ℕk:ℕhj:N ≤ jhk:N ≤ khε:0 < εhN:ε⁻¹ < ↑NhN':0 < Nhdist:Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ (↑N)⁻¹⊢ 0 < ↑Nε:ℚN:ℕj:ℕk:ℕhj:N ≤ jhk:N ≤ khε:0 < εhN:ε⁻¹ < ↑NhN':0 < Nhdist:Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ (↑N)⁻¹⊢ 0 < ε try All goals completed! 🐙 All goals completed! 🐙
abbrev BoundedBy {n:ℕ} (a: Fin n → ℚ) (M:ℚ) : Prop := ∀ i, |a i| ≤ M

Definition 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 := n:ℕa:Fin n → ℚM:ℚ⊢ BoundedBy a M ↔ ∀ (i : Fin n), |a i| ≤ M All goals completed! 🐙
abbrev Sequence.BoundedBy (a:Sequence) (M:ℚ) : Prop := ∀ n, |a n| ≤ M

Definition 5.1.12 (bounded sequences)

lemma Sequence.boundedBy_def (a:Sequence) (M:ℚ) : a.BoundedBy M ↔ ∀ n, |a n| ≤ M := a:SequenceM:ℚ⊢ a.BoundedBy M ↔ ∀ (n : ℤ), |a.seq n| ≤ M All goals completed! 🐙
abbrev Sequence.IsBounded (a:Sequence) : Prop := ∃ M ≥ 0, a.BoundedBy M

Definition 5.1.12 (bounded sequences)

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

Example 5.1.13

example : BoundedBy ![1,-2,3,-4] 4 := ⊢ BoundedBy ![1, -2, 3, -4] 4 i:Fin (Nat.succ 0).succ.succ.succ⊢ |![1, -2, 3, -4] i| ≤ 4; ⊢ |![1, -2, 3, -4] ((fun i => i) ⟨0, ⋯⟩)| ≤ 4⊢ |![1, -2, 3, -4] ((fun i => i) ⟨1, ⋯⟩)| ≤ 4⊢ |![1, -2, 3, -4] ((fun i => i) ⟨2, ⋯⟩)| ≤ 4⊢ |![1, -2, 3, -4] ((fun i => i) ⟨3, ⋯⟩)| ≤ 4 ⊢ |![1, -2, 3, -4] ((fun i => i) ⟨0, ⋯⟩)| ≤ 4⊢ |![1, -2, 3, -4] ((fun i => i) ⟨1, ⋯⟩)| ≤ 4⊢ |![1, -2, 3, -4] ((fun i => i) ⟨2, ⋯⟩)| ≤ 4⊢ |![1, -2, 3, -4] ((fun i => i) ⟨3, ⋯⟩)| ≤ 4 All goals completed! 🐙

Example 5.1.13

declaration uses 'sorry'example : ¬((fun n:ℕ ↦ (-1)^n * (n+1:ℚ)):Sequence).IsBounded := ⊢ ¬(↑fun n => (-1) ^ n * (↑n + 1)).IsBounded All goals completed! 🐙

Example 5.1.13

example : ((fun n:ℕ ↦ (-1:ℚ)^n):Sequence).IsBounded := ⊢ (↑fun n => (-1) ^ n).IsBounded refine ⟨ 1, ⊢ 1 ≥ 0 All goals completed! 🐙, ?_ ⟩; i:ℤ⊢ |(↑fun n => (-1) ^ n).seq i| ≤ 1; i:ℤh:0 ≤ i⊢ |(↑fun n => (-1) ^ n).seq i| ≤ 1i:ℤh:¬0 ≤ i⊢ |(↑fun n => (-1) ^ n).seq i| ≤ 1 i:ℤh:0 ≤ i⊢ |(↑fun n => (-1) ^ n).seq i| ≤ 1i:ℤh:¬0 ≤ i⊢ |(↑fun n => (-1) ^ n).seq i| ≤ 1 All goals completed! 🐙

Example 5.1.13

example : ¬((fun n:ℕ ↦ (-1:ℚ)^n):Sequence).IsCauchy := ⊢ ¬(↑fun n => (-1) ^ n).IsCauchy ⊢ ¬∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((-1) ^ j) ((-1) ^ k) ≤ ε h:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((-1) ^ j) ((-1) ^ k) ≤ ε⊢ False; specialize h (1/2 : ℚ) (h:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((-1) ^ j) ((-1) ^ k) ≤ ε⊢ 1 / 2 > 0 All goals completed! 🐙) N:ℕh:∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((-1) ^ j) ((-1) ^ k) ≤ 1 / 2⊢ False; N:ℕh:∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((-1) ^ j) ((-1) ^ k) ≤ 1 / 2⊢ N ≥ NN:ℕh:∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((-1) ^ j) ((-1) ^ k) ≤ 1 / 2⊢ N + 1 ≥ NN:ℕh:Section_4_3.dist ((-1) ^ N) ((-1) ^ (N + 1)) ≤ 1 / 2⊢ False N:ℕh:∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((-1) ^ j) ((-1) ^ k) ≤ 1 / 2⊢ N ≥ NN:ℕh:∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((-1) ^ j) ((-1) ^ k) ≤ 1 / 2⊢ N + 1 ≥ NN:ℕh:Section_4_3.dist ((-1) ^ N) ((-1) ^ (N + 1)) ≤ 1 / 2⊢ False try N:ℕh:Section_4_3.dist ((-1) ^ N) ((-1) ^ (N + 1)) ≤ 1 / 2⊢ False N:ℕh:Section_4_3.dist ((-1) ^ N) ((-1) ^ (N + 1)) ≤ 1 / 2h':Even N⊢ FalseN:ℕh:Section_4_3.dist ((-1) ^ N) ((-1) ^ (N + 1)) ≤ 1 / 2h':¬Even N⊢ False N:ℕh:Section_4_3.dist ((-1) ^ N) ((-1) ^ (N + 1)) ≤ 1 / 2h':Even N⊢ False N:ℕh':Even Nh:|1 + 1| ≤ 2⁻¹⊢ False All goals completed! 🐙 N:ℕh:Section_4_3.dist ((-1) ^ N) ((-1) ^ (N + 1)) ≤ 1 / 2h':¬Even Nh₁:Odd N⊢ False N:ℕh:Section_4_3.dist ((-1) ^ N) ((-1) ^ (N + 1)) ≤ 1 / 2h':¬Even Nh₁:Odd Nh₂:Even (N + 1)⊢ False N:ℕh':¬Even Nh₁:Odd Nh₂:Even (N + 1)h:|-1 - 1| ≤ 2⁻¹⊢ False All goals completed! 🐙

Lemma 5.1.14

lemma IsBounded.finite {n:ℕ} (a: Fin n → ℚ) : ∃ M ≥ 0, BoundedBy a M := n:ℕa:Fin n → ℚ⊢ ∃ M ≥ 0, BoundedBy a M -- this proof is written to follow the structure of the original text. a:Fin 0 → ℚ⊢ ∃ M ≥ 0, BoundedBy a Mn:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚ⊢ ∃ M ≥ 0, BoundedBy a M a:Fin 0 → ℚ⊢ ∃ M ≥ 0, BoundedBy a M a:Fin 0 → ℚ⊢ 0 ≥ 0 ∧ BoundedBy a 0; All goals completed! 🐙 n:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin _fvar.572699 → ℚ := fun m => @_fvar.572704 m.castSucc⊢ ∃ M ≥ 0, BoundedBy a M n:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin _fvar.572699 → ℚ := fun m => @_fvar.572704 m.castSuccM:ℚhpos:M ≥ 0hM:BoundedBy a' M⊢ ∃ M ≥ 0, BoundedBy a M have h1 : BoundedBy a' (M + |a (Fin.ofNat _ n)|) := fun m ↦ (hM m).trans (n:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin _fvar.572699 → ℚ := fun m => @_fvar.572704 m.castSuccM:ℚhpos:M ≥ 0hM:BoundedBy a' Mm:Fin n⊢ M ≤ M + |a (Fin.ofNat (n + 1) n)| All goals completed! 🐙) have h2 : |a (Fin.ofNat _ n)| ≤ M + |a (Fin.ofNat _ n)| := n:ℕa:Fin n → ℚ⊢ ∃ M ≥ 0, BoundedBy a M All goals completed! 🐙 refine ⟨ M + |a (Fin.ofNat _ n)|, n:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin _fvar.572699 → ℚ := fun m => @_fvar.572704 m.castSuccM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:Chapter5.BoundedBy _fvar.572972 (_fvar.573031 + |@_fvar.572704 (Fin.ofNat (_fvar.572699 + 1) _fvar.572699)|) := fun m => LE.le.trans (@_fvar.573043 m) (of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => _fvar.573031 ≤ _fvar.573031 + |@_fvar.572704 x|) (Fin.natCast_eq_last _fvar.572699)) (le_mul_iff_one_le_right'._simp_4 _fvar.573031)) (one_le_mabs._simp_4 (@_fvar.572704 (Fin.last _fvar.572699)))))h2:|@_fvar.572704 (Fin.ofNat (_fvar.572699 + 1) _fvar.572699)| ≤ _fvar.573031 + |@_fvar.572704 (Fin.ofNat (_fvar.572699 + 1) _fvar.572699)| := of_eq_true (Eq.trans (Eq.trans (congr (congrArg (fun x => LE.le |@_fvar.572704 x|) (Fin.natCast_eq_last _fvar.572699)) (congrArg (fun x => _fvar.573031 + |@_fvar.572704 x|) (Fin.natCast_eq_last _fvar.572699))) (le_mul_iff_one_le_left'._simp_4 |@_fvar.572704 (Fin.last _fvar.572699)|)) (eq_true _fvar.573039))⊢ M + |a (Fin.ofNat (n + 1) n)| ≥ 0 All goals completed! 🐙, ?_ ⟩ n:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin _fvar.572699 → ℚ := fun m => @_fvar.572704 m.castSuccM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:Chapter5.BoundedBy _fvar.572972 (_fvar.573031 + |@_fvar.572704 (Fin.ofNat ?_mvar.573059 _fvar.572699)|) := fun m => LE.le.trans (@_fvar.573043 m) (@?_mvar.573201 m)h2:|@_fvar.572704 (Fin.ofNat ?_mvar.575355 _fvar.572699)| ≤ _fvar.573031 + |@_fvar.572704 (Fin.ofNat ?_mvar.575438 _fvar.572699)| := ?_mvar.575521m:Fin (n + 1)⊢ |a m| ≤ M + |a (Fin.ofNat (n + 1) n)|; n:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin _fvar.572699 → ℚ := fun m => @_fvar.572704 m.castSuccM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:Chapter5.BoundedBy _fvar.572972 (_fvar.573031 + |@_fvar.572704 (Fin.ofNat ?_mvar.573059 _fvar.572699)|) := fun m => LE.le.trans (@_fvar.573043 m) (@?_mvar.573201 m)h2:|@_fvar.572704 (Fin.ofNat ?_mvar.575355 _fvar.572699)| ≤ _fvar.573031 + |@_fvar.572704 (Fin.ofNat ?_mvar.575438 _fvar.572699)| := ?_mvar.575521j:Fin n⊢ |a j.castSucc| ≤ M + |a (Fin.ofNat (n + 1) n)|n:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin _fvar.572699 → ℚ := fun m => @_fvar.572704 m.castSuccM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:Chapter5.BoundedBy _fvar.572972 (_fvar.573031 + |@_fvar.572704 (Fin.ofNat ?_mvar.573059 _fvar.572699)|) := fun m => LE.le.trans (@_fvar.573043 m) (@?_mvar.573201 m)h2:|@_fvar.572704 (Fin.ofNat ?_mvar.575355 _fvar.572699)| ≤ _fvar.573031 + |@_fvar.572704 (Fin.ofNat ?_mvar.575438 _fvar.572699)| := ?_mvar.575521⊢ |a (Fin.last n)| ≤ M + |a (Fin.ofNat (n + 1) n)| n:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin _fvar.572699 → ℚ := fun m => @_fvar.572704 m.castSuccM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:Chapter5.BoundedBy _fvar.572972 (_fvar.573031 + |@_fvar.572704 (Fin.ofNat ?_mvar.573059 _fvar.572699)|) := fun m => LE.le.trans (@_fvar.573043 m) (@?_mvar.573201 m)h2:|@_fvar.572704 (Fin.ofNat ?_mvar.575355 _fvar.572699)| ≤ _fvar.573031 + |@_fvar.572704 (Fin.ofNat ?_mvar.575438 _fvar.572699)| := ?_mvar.575521j:Fin n⊢ |a j.castSucc| ≤ M + |a (Fin.ofNat (n + 1) n)| All goals completed! 🐙 n:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin _fvar.572699 → ℚ := fun m => @_fvar.572704 m.castSuccM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:Chapter5.BoundedBy _fvar.572972 (_fvar.573031 + |@_fvar.572704 (Fin.ofNat ?_mvar.573059 _fvar.572699)|) := fun m => LE.le.trans (@_fvar.573043 m) (@?_mvar.573201 m)h2:|@_fvar.572704 (Fin.ofNat ?_mvar.575355 _fvar.572699)| ≤ _fvar.573031 + |@_fvar.572704 (Fin.ofNat ?_mvar.575438 _fvar.572699)| := ?_mvar.575521⊢ Fin.last n = Fin.ofNat (n + 1) n; All goals completed! 🐙

Lemma 5.1.15 (Cauchy sequences are bounded) / Exercise 5.1.1

lemma declaration uses 'sorry'Sequence.isBounded_of_isCauchy {a:Sequence} (h: a.IsCauchy) : a.IsBounded := a:Sequenceh:a.IsCauchy⊢ a.IsBounded All goals completed! 🐙

Exercise 5.1.2

theorem declaration uses 'sorry'Sequence.isBounded_add {a b:ℕ → ℚ} (ha: (a:Sequence).IsBounded) (hb: (b:Sequence).IsBounded): (a + b:Sequence).IsBounded := a:ℕ → ℚb:ℕ → ℚha:(↑a).IsBoundedhb:(↑b).IsBounded⊢ (↑(a + b)).IsBounded All goals completed! 🐙
theorem declaration uses 'sorry'Sequence.isBounded_sub {a b:ℕ → ℚ} (ha: (a:Sequence).IsBounded) (hb: (b:Sequence).IsBounded): (a - b:Sequence).IsBounded := a:ℕ → ℚb:ℕ → ℚha:(↑a).IsBoundedhb:(↑b).IsBounded⊢ (↑(a - b)).IsBounded All goals completed! 🐙theorem declaration uses 'sorry'Sequence.isBounded_mul {a b:ℕ → ℚ} (ha: (a:Sequence).IsBounded) (hb: (b:Sequence).IsBounded): (a * b:Sequence).IsBounded := a:ℕ → ℚb:ℕ → ℚha:(↑a).IsBoundedhb:(↑b).IsBounded⊢ (↑(a * b)).IsBounded All goals completed! 🐙end Chapter5