Аналіз I, Розділ 5.2: Еквівалентні послідовності Коші

Я (пр.перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним рішенням Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підбуцнути", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні конструкції та результати цього розділу:

• Поняття ε-близьких та з часом ε-близьких послідовностей раціональних чисел.
• Поняття еквівалентної послідовності Коші раціональних чисел.

Підказки від попередніх користувачів

Користувачі супровідного матеріалу, які виконали вправи в цьому розділі, можуть надсилати свої поради майбутнім користувачам цього розділу як PRи.

• (Додайте підказку тут)

@[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)

Визначення 5.2.1 ($ε$-близькі послідовності)

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

Визначення 5.2.3 (З часом ε-близькі послідовності)

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

Визначення 5.2.3 (З часом ε-близькі послідовності)

@[reducible, inline]

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

Визначення 5.2.6 (Еквівалентні послідовності)

Equations

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

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

Визначення 5.2.6 (Еквівалентні послідовності)

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

Визначення 5.2.6 (Еквівалентні послідовності)

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

Твердження 5.2.8

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

Вправа 5.2.1

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

Вправа 5.2.2