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 ε-steadiness, eventual ε-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)

structure Chapter5.Sequence : Type

Definition 5.1.1 (Sequence). To avoid some technicalities involving dependent types, we extend sequences by zero to the left of the starting point n₀.

• n₀ : ℤ
• seq : ℤ → ℚ
• vanish (n : ℤ) : n < self.n₀ → self.seq n = 0

theorem Chapter5.Sequence.ext_iff {x y : Sequence} : x = y ↔ x.n₀ = y.n₀ ∧ x.seq = y.seq

theorem Chapter5.Sequence.ext {x y : Sequence} (n₀ : x.n₀ = y.n₀) (seq : x.seq = y.seq) : x = y

instance Chapter5.Sequence.instCoeFun : CoeFun Sequence fun (x : Sequence) => ℤ → ℚ

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

Equations

• Chapter5.Sequence.instCoeFun = { coe := fun (a : Chapter5.Sequence) => a.seq }

def Chapter5.Sequence.ofNatFun (a : ℕ → ℚ) : Sequence

Functions from ℕ to ℚ can be thought of as sequences starting from 0; ofNatFun performs this conversion.

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

Equations

• ↑a = { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }

instance Chapter5.instCoeForallNatRatSequence : Coe (ℕ → ℚ) Sequence

If a : ℕ → ℚ is used in a context where a Sequence is expected, automatically coerce a to Sequence.ofNatFun a (which will be pretty-printed as ↑a)

Equations

• Chapter5.instCoeForallNatRatSequence = { coe := Chapter5.Sequence.ofNatFun }

@[reducible, inline]

abbrev Chapter5.Sequence.mk' (n₀ : ℤ) (a : { n : ℤ // n ≥ n₀ } → ℚ) : Sequence

Equations

• Chapter5.Sequence.mk' n₀ a = { n₀ := n₀, seq := fun (n : ℤ) => if h : n ≥ n₀ then a ⟨n, h⟩ else 0, vanish := ⋯ }

theorem Chapter5.Sequence.eval_mk {n n₀ : ℤ} (a : { n : ℤ // n ≥ n₀ } → ℚ) (h : n ≥ n₀) : (mk' n₀ a).seq n = a ⟨n, h⟩

@[simp]

theorem Chapter5.Sequence.eval_coe (n : ℕ) (a : ℕ → ℚ) : (↑a).seq ↑n = a n

@[simp]

theorem Chapter5.Sequence.eval_coe_at_int (n : ℤ) (a : ℕ → ℚ) : (↑a).seq n = if n ≥ 0 then a n.toNat else 0

@[simp]

theorem Chapter5.Sequence.n0_coe (a : ℕ → ℚ) : (↑a).n₀ = 0

@[reducible, inline]

abbrev Chapter5.Sequence.squares : Sequence

Example 5.1.2

Equations

• Chapter5.Sequence.squares = ↑fun (n : ℕ) => ↑n ^ 2

@[reducible, inline]

abbrev Chapter5.Sequence.three : Sequence

Example 5.1.2

Equations

• Chapter5.Sequence.three = ↑fun (x : ℕ) => 3

@[reducible, inline]

abbrev Chapter5.Sequence.squares_from_three : Sequence

Example 5.1.2

Equations

• Chapter5.Sequence.squares_from_three = Chapter5.Sequence.mk' 3 fun (x : { n : ℤ // n ≥ 3 }) => ↑↑x ^ 2

@[reducible, inline]

abbrev Rat.Steady (ε : ℚ) (a : Chapter5.Sequence) : Prop

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

Equations

• ε.Steady a = ∀ n ≥ a.n₀, ∀ m ≥ a.n₀, ε.Close (a.seq n) (a.seq m)

theorem Rat.steady_def (ε : ℚ) (a : Chapter5.Sequence) : ε.Steady a ↔ ∀ n ≥ a.n₀, ∀ m ≥ a.n₀, ε.Close (a.seq n) (a.seq m)

theorem Chapter5.Rat.Steady.coe (ε : ℚ) (a : ℕ → ℚ) : ε.Steady ↑a ↔ ∀ (n m : ℕ), ε.Close (a n) (a m)

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

@[reducible, inline]

abbrev Chapter5.Sequence.from (a : Sequence) (n₁ : ℤ) : Sequence

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

Equations

• a.from n₁ = Chapter5.Sequence.mk' (max a.n₀ n₁) fun (n : { n : ℤ // n ≥ max a.n₀ n₁ }) => a.seq ↑n

theorem Chapter5.Sequence.from_eval (a : Sequence) {n₁ n : ℤ} (hn : n ≥ n₁) : (a.from n₁).seq n = a.seq n

@[reducible, inline]

abbrev Rat.EventuallySteady (ε : ℚ) (a : Chapter5.Sequence) : Prop

Definition 5.1.6 (Eventually ε-steady)

Equations

• ε.EventuallySteady a = ∃ N ≥ a.n₀, ε.Steady (a.from N)

theorem Rat.eventuallySteady_def (ε : ℚ) (a : Chapter5.Sequence) : ε.EventuallySteady a ↔ ∃ N ≥ a.n₀, ε.Steady (a.from N)

theorem Chapter5.Sequence.ex_5_1_7_a : ¬Rat.Steady 0.1 ↑fun (n : ℕ) => (↑n + 1)⁻¹

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

theorem Chapter5.Sequence.ex_5_1_7_b : Rat.Steady 0.1 ((↑fun (n : ℕ) => (↑n + 1)⁻¹).from 10)

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

theorem Chapter5.Sequence.ex_5_1_7_c : Rat.EventuallySteady 0.1 ↑fun (n : ℕ) => (↑n + 1)⁻¹

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

theorem Chapter5.Sequence.ex_5_1_7_d {ε : ℚ} (hε : ε > 0) : ε.EventuallySteady ↑fun (n : ℕ) => if n = 0 then 10 else 0

Example 5.1.7

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

@[reducible, inline]

abbrev Chapter5.Sequence.IsCauchy (a : Sequence) : Prop

Equations

• a.IsCauchy = ∀ ε > 0, ε.EventuallySteady a

theorem Chapter5.Sequence.isCauchy_def (a : Sequence) : a.IsCauchy ↔ ∀ ε > 0, ε.EventuallySteady a

theorem Chapter5.Sequence.IsCauchy.coe (a : ℕ → ℚ) : (↑a).IsCauchy ↔ ∀ ε > 0, ∃ (N : ℕ), ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε

Definition of Cauchy sequences, for a sequence starting at 0

theorem Chapter5.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).seq j) ((mk' n₀ a).seq k) ≤ ε

noncomputable def Chapter5.Sequence.sqrt_two : Sequence

Equations

• Chapter5.Sequence.sqrt_two = ↑fun (n : ℕ) => ↑⌊√2 * 10 ^ n⌋ / 10 ^ n

theorem Chapter5.Sequence.ex_5_1_10_a : Rat.Steady 1 sqrt_two

Example 5.1.10. (This requires extensive familiarity with Mathlib's API for the real numbers.)

theorem Chapter5.Sequence.ex_5_1_10_b : Rat.Steady 0.1 (sqrt_two.from 1)

Example 5.1.10. (This requires extensive familiarity with Mathlib's API for the real numbers.)

theorem Chapter5.Sequence.ex_5_1_10_c : Rat.EventuallySteady 0.1 sqrt_two

theorem Chapter5.Sequence.IsCauchy.harmonic : (mk' 1 fun (n : { n : ℤ // n ≥ 1 }) => 1 / ↑↑n).IsCauchy

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

@[reducible, inline]

abbrev Chapter5.BoundedBy {n : ℕ} (a : Fin n → ℚ) (M : ℚ) : Prop

Equations

• Chapter5.BoundedBy a M = ∀ (i : Fin n), |a i| ≤ M

theorem Chapter5.boundedBy_def {n : ℕ} (a : Fin n → ℚ) (M : ℚ) : BoundedBy a M ↔ ∀ (i : Fin n), |a i| ≤ M

Definition 5.1.12 (bounded sequences). Here we start sequences from 0 rather than 1 to align better with Mathlib conventions.

@[reducible, inline]

abbrev Chapter5.Sequence.BoundedBy (a : Sequence) (M : ℚ) : Prop

Equations

• a.BoundedBy M = ∀ (n : ℤ), |a.seq n| ≤ M

theorem Chapter5.Sequence.boundedBy_def (a : Sequence) (M : ℚ) : a.BoundedBy M ↔ ∀ (n : ℤ), |a.seq n| ≤ M

Definition 5.1.12 (bounded sequences)

@[reducible, inline]

abbrev Chapter5.Sequence.IsBounded (a : Sequence) : Prop

Equations

• a.IsBounded = ∃ M ≥ 0, a.BoundedBy M

theorem Chapter5.Sequence.isBounded_def (a : Sequence) : a.IsBounded ↔ ∃ M ≥ 0, a.BoundedBy M

Definition 5.1.12 (bounded sequences)

theorem Chapter5.IsBounded.finite {n : ℕ} (a : Fin n → ℚ) : ∃ M ≥ 0, BoundedBy a M

Lemma 5.1.14

theorem Chapter5.Sequence.isBounded_of_isCauchy {a : Sequence} (h : a.IsCauchy) : a.IsBounded

Lemma 5.1.15 (Cauchy sequences are bounded) / Exercise 5.1.1

theorem Chapter5.Sequence.isBounded_add {a b : ℕ → ℚ} (ha : (↑a).IsBounded) (hb : (↑b).IsBounded) : (↑(a + b)).IsBounded

Exercise 5.1.2

theorem Chapter5.Sequence.isBounded_sub {a b : ℕ → ℚ} (ha : (↑a).IsBounded) (hb : (↑b).IsBounded) : (↑(a - b)).IsBounded

theorem Chapter5.Sequence.isBounded_mul {a b : ℕ → ℚ} (ha : (↑a).IsBounded) (hb : (↑b).IsBounded) : (↑(a * b)).IsBounded