Analysis I, Section 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 ε-steadiness, eventual ε-steadiness, and Cauchy sequences

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 {x y : Sequence} (n₀ : x.n₀ = y.n₀) (seq : x.seq = y.seq) : x = y

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

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

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

Equations

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

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

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

Equations

• Chapter5.Sequence.instCoe = { coe := fun (a : ℕ → ℚ) => { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } }

@[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 : ℕ → ℚ) : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq ↑n = a n

@[reducible, inline]

abbrev Chapter5.Sequence.squares : Sequence

Example 5.1.2

Equations

• Chapter5.Sequence.squares = { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => ↑n ^ 2) n.toNat else 0, vanish := Chapter5.Sequence.squares._proof_3 }

@[reducible, inline]

abbrev Chapter5.Sequence.three : Sequence

Example 5.1.2

Equations

• Chapter5.Sequence.three = { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (x : ℕ) => 3) n.toNat else 0, vanish := Chapter5.Sequence.three._proof_4 }

@[reducible, inline]

abbrev Chapter5.Sequence.squares_from_three : Sequence

Example 5.1.2

Equations

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

@[reducible, inline]

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

Equations

• ε.steady a = ∀ (n m : ℤ), ε.close (a.seq n) (a.seq m)

theorem Chapter5.Rat.steady_def (ε : ℚ) (a : Sequence) : ε.steady a ↔ ∀ (n m : ℤ), ε.close (a.seq n) (a.seq m)

theorem Chapter5.Rat.steady_def' (ε : ℚ) (a : Sequence) : ε.steady a ↔ ∀ (n m : ℤ), n ≥ a.n₀ ∧ m ≥ a.n₀ → ε.close (a.seq n) (a.seq m)

@[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 Chapter5.Rat.eventuallySteady_def (ε : ℚ) (a : Sequence) : ε.eventuallySteady a ↔ ∃ N ≥ a.n₀, ε.steady (a.from N)

theorem Chapter5.Sequence.ex_5_1_7_a : ¬Rat.steady 0.1 { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => (↑n + 1)⁻¹) n.toNat else 0, vanish := ⋯ }

Example 5.1.7

theorem Chapter5.Sequence.ex_5_1_7_b : Rat.steady 0.1 ({ n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => (↑n + 1)⁻¹) n.toNat else 0, vanish := ⋯ }.from 10)

theorem Chapter5.Sequence.ex_5_1_7_c : Rat.eventuallySteady 0.1 { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => (↑n + 1)⁻¹) n.toNat else 0, vanish := ⋯ }

theorem Chapter5.Sequence.ex_5_1_7_d {ε : ℚ} (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 := ⋯ }

@[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_of_coe (a : ℕ → ℚ) : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ↔ ∀ ε > 0, ∃ (N : ℕ), ∀ (j k : ℕ), j ≥ N ∧ k ≥ N → Section_4_3.dist (a j) (a k) ≤ ε

theorem Chapter5.Sequence.isCauchy_of_mk {n₀ : ℤ} (a : { n : ℤ // n ≥ n₀ } → ℚ) : (mk' n₀ a).isCauchy ↔ ∀ ε > 0, ∃ N ≥ n₀, ∀ (j k : ℤ), 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 = { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => ↑⌊√2 * 10 ^ n⌋ / 10 ^ n) n.toNat else 0, vanish := Chapter5.Sequence.sqrt_two._proof_7 }

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.harmonic_steady : (mk' 1 fun (n : { n : ℤ // n ≥ 1 }) => 1 / ↑↑n).isCauchy

Proposition 5.1.11

@[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.bounded_of_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