Analysis I, Section 5.2: Equivalent 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 an ε-close and eventually ε-close sequences of rationals.
• Notion of an equivalent Cauchy sequence of rationals.

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)

@[reducible, inline]

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

Equations

• ε.CloseSeq a b = ∀ n ≥ a.n₀, n ≥ b.n₀ → ε.Close (a.seq n) (b.seq n)

@[reducible, inline]

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

Equations

• ε.EventuallyClose a b = ∃ (N : ℤ), ε.CloseSeq (a.from N) (b.from N)

theorem Chapter5.Rat.closeSeq_def (ε : ℚ) (a b : Sequence) : ε.CloseSeq a b ↔ ∀ n ≥ a.n₀, n ≥ b.n₀ → ε.Close (a.seq n) (b.seq n)

Definition 5.2.1 ($ε$-close sequences)

theorem Chapter5.Rat.eventuallyClose_def (ε : ℚ) (a b : Sequence) : ε.EventuallyClose a b ↔ ∃ (N : ℤ), ε.CloseSeq (a.from N) (b.from N)

Definition 5.2.3 (Eventually ε-close sequences)

theorem Chapter5.Rat.eventuallyClose_iff (ε : ℚ) (a b : ℕ → ℚ) : ε.EventuallyClose ↑a ↑b ↔ ∃ (N : ℕ), ∀ n ≥ N, |a n - b n| ≤ ε

Definition 5.2.3 (Eventually ε-close sequences)

@[reducible, inline]

abbrev Chapter5.Sequence.Equiv (a b : ℕ → ℚ) : Prop

Definition 5.2.6 (Equivalent sequences)

Equations

• Chapter5.Sequence.Equiv a b = ∀ ε > 0, ε.EventuallyClose ↑a ↑b

theorem Chapter5.Sequence.equiv_def (a b : ℕ → ℚ) : Equiv a b ↔ ∀ ε > 0, ε.EventuallyClose ↑a ↑b

Definition 5.2.6 (Equivalent sequences)

theorem Chapter5.Sequence.equiv_iff (a b : ℕ → ℚ) : Equiv a b ↔ ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, |a n - b n| ≤ ε

Definition 5.2.6 (Equivalent sequences)

theorem Chapter5.Sequence.equiv_example : Equiv (fun (n : ℕ) => 1 + 10 ^ (-↑n - 1)) fun (n : ℕ) => 1 - 10 ^ (-↑n - 1)

Proposition 5.2.8

theorem Chapter5.Sequence.isCauchy_of_equiv {a b : ℕ → ℚ} (hab : Equiv a b) : (↑a).IsCauchy ↔ (↑b).IsCauchy

Exercise 5.2.1

theorem Chapter5.Sequence.isBounded_of_eventuallyClose {ε : ℚ} {a b : ℕ → ℚ} (hab : ε.EventuallyClose ↑a ↑b) : (↑a).IsBounded ↔ (↑b).IsBounded

Exercise 5.2.2