Аналіз I, Розділ 5.1: Послідовності Коші

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

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

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

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

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

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

structure Chapter5.Sequence : Type

Визначення 5.1.1 (Послідовність). Щоб уникнути деяких технічних питань, пов’язаних із залежними типами, ми розширюємо послідовності нулями ліворуч від початкової точки 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) => ℤ → ℚ

Послідовності можна розглядати як функції з ℤ у ℚ.

Equations

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

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

Функції з ℕ у ℚ можна розглядати як послідовності, що починаються з 0; ofNatFun виконує це перетворення.

Атрибут coe дозволяє делаборатору виводити Sequence.ofNatFun f як ↑f, що є більш стислим; ви можете безпечно видалити його, якщо віддаєте перевагу більш явному позначенню.

Equations

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

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

Якщо a : ℕ → ℚ використовується в контексті, де очікується Sequence, автоматично перетворюйте a на Sequence.ofNatFun a (що буде гарно виведено як ↑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

Приклад 5.1.2

Equations

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

@[reducible, inline]

abbrev Chapter5.Sequence.three : Sequence

Приклад 5.1.2

Equations

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

@[reducible, inline]

abbrev Chapter5.Sequence.squares_from_three : Sequence

Приклад 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

Невелике узагальнення Визначення 5.1.3 — визначення ε-сталості для послідовності з довільною початковою точкою 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)

Визначення 5.1.3 — визначення ε-сталості для послідовності, що починається з 0.

@[reducible, inline]

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

a.Від n₁ починається a:Sequence з n₁. Його призначено для використання, коли n₁ ≥ n₀, але в іншому випадку воно повертає "сміттєве" значення оригінальної послідовності a.

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

Визначення 5.1.6 (ε-стійка з часом)

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)⁻¹

Приклад 5.1.7: Послідовність 1, 1/2, 1/3, ... не є 0,1-стійкою.

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

Приклад 5.1.7: Послідовність a_10, a_11, a_12, ... є 0.1-стійкою

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

Приклад 5.1.7: Послідовність 1, 1/2, 1/3, ... з часом є 0,1-стійкою.

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

Приклад 5.1.7

Послідовність 10, 0, 0, ... з часом є ε-стійкою для будь-якого ε > 0. Залишено як вправу.

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

Визначення послідовностей Коші для послідовності, що починається з 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

Приклад 5.1.10. (Це вимагає ґрунтовного знайомства з API Mathlib для дійсних чисел.)

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

Приклад 5.1.10. (Це вимагає ґрунтовного знайомства з API Mathlib для дійсних чисел.)

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

Твердження 5.1.11. Гармонічна послідовність, визначена як a₁ = 1, a₂ = 1/2, ... є послідовністю Коші.

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

Визначення 5.1.12 (обмежені послідовності). Тут ми починаємо послідовності з 0 замість 1, щоб краще узгоджуватись із конвенціями Mathlib.

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

Визначення 5.1.12 (обмежені послідовності)

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

Визначення 5.1.12 (обмежені послідовності)

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

Лема 5.1.14

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

Лема 5.1.15 (Послідовності Коші є обмеженими) / Вправа 5.1.1

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

Вправа 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