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

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

@[reducible, inline]

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

Equations

• ε.close_seq a b = ∀ n ≥ a.n₀, n ≥ b.n₀ → ε.close (a.seq n) (b.seq n)

@[reducible, inline]

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

Equations

• ε.eventually_close a b = ∃ (N : ℤ), ε.close_seq (a.from N) (b.from N)

theorem Chapter5.Rat.close_seq_def (ε : ℚ) (a b : Sequence) : ε.close_seq a b ↔ ∀ n ≥ a.n₀, n ≥ b.n₀ → ε.close (a.seq n) (b.seq n)

Визначення 5.2.1 ($ε$-close sequences)

theorem Chapter5.Rat.eventually_close_def (ε : ℚ) (a b : Sequence) : ε.eventually_close a b ↔ ∃ (N : ℤ), ε.close_seq (a.from N) (b.from N)

Визначення 5.2.3 (Eventually ε-close sequences)

theorem Chapter5.Rat.eventually_close_iff (ε : ℚ) (a b : ℕ → ℚ) : ε.eventually_close { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ } ↔ ∃ (N : ℕ), ∀ n ≥ N, |a n - b n| ≤ ε

Визначення 5.2.3 (Eventually ε-close sequences)

@[reducible, inline]

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

Визначення 5.2.6 (Equivalent sequences)

Equations

• One or more equations did not get rendered due to their size.

theorem Chapter5.Sequence.equiv_def (a b : ℕ → ℚ) : equiv a b ↔ ∀ ε > 0, ε.eventually_close { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }

Визначення 5.2.6 (Equivalent sequences)

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

Визначення 5.2.6 (Equivalent sequences)

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

Твердження 5.2.8

theorem Chapter5.Sequence.equiv_of_cauchy {a b : ℕ → ℚ} (hab : equiv a b) : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isCauchy ↔ { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isCauchy

Вправа 5.2.1

theorem Chapter5.Sequence.close_of_bounded {ε : ℚ} {a b : ℕ → ℚ} (hab : ε.eventually_close { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }) : { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.isBounded ↔ { n₀ := 0, seq := fun (n : ℤ) => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }.isBounded

Вправа 5.2.2