Cauchy sequences

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

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

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

  • Поняття послідовності раціональних чисел

  • Поняття Unknown identifier `ε`ε-сталість, кінцевої Unknown identifier `ε`ε-сталість та послідовностей Коші

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

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

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

namespace Chapter5

Визначення 5.1.1 (Послідовність). Щоб уникнути деяких технічних питань, пов’язаних із залежними типами, ми розширюємо послідовності нулями ліворуч від початкової точки Unknown identifier `n₀`n₀.

@[ext] structure Sequence where n₀ : ℤ seq : ℤ → ℚ vanish : ∀ n < n₀, seq n = 0

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

instance Sequence.instCoeFun : CoeFun Sequence (fun _ ↦ ℤ → ℚ) where coe := fun a ↦ a.seq

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

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

@[coe] def Sequence.ofNatFun (a : ℕ → ℚ) : Sequence where n₀ := 0 seq n := if n ≥ 0 then a n.toNat else 0 vanish := a:ℕ → ℚ⊢ ∀ n < 0, (if n ≥ 0 then a n.toNat else 0) = 0 All goals completed! 🐙
↑fun x => ↑x ^ 2 : Sequence

Якщо використовується в контексті, де очікується Chapter5.Sequence : TypeSequence, автоматично перетворюйте Unknown identifier `a`a на ↑sorry : SequenceSequence.ofNatFun Unknown identifier `a`a (що буде гарно виведено як ↑Unknown identifier `a`a).

instance : Coe (ℕ → ℚ) Sequence where coe := Sequence.ofNatFun
abbrev Sequence.mk' (n₀:ℤ) (a: { n // n ≥ n₀ } → ℚ) : Sequence where n₀ := n₀ seq n := if h : n ≥ n₀ then a ⟨n, h⟩ else 0 vanish := n₀:ℤa:{ n // n ≥ n₀ } → ℚ⊢ ∀ n < n₀, (if h : n ≥ n₀ then a ⟨n, h⟩ else 0) = 0 All goals completed! 🐙lemma Sequence.eval_mk {n n₀:ℤ} (a: { n // n ≥ n₀ } → ℚ) (h: n ≥ n₀) : (Sequence.mk' n₀ a) n = a ⟨ n, h ⟩ := n:ℤn₀:ℤa:{ n // n ≥ n₀ } → ℚh:n ≥ n₀⊢ (mk' n₀ a).seq n = a ⟨n, h⟩ All goals completed! 🐙@[simp] lemma Sequence.eval_coe (n:ℕ) (a: ℕ → ℚ) : (a:Sequence) n = a n := n:ℕa:ℕ → ℚ⊢ (↑a).seq ↑n = a n All goals completed! 🐙@[simp] lemma Sequence.eval_coe_at_int (n:ℤ) (a: ℕ → ℚ) : (a:Sequence) n = if n ≥ 0 then a n.toNat else 0 := n:ℤa:ℕ → ℚ⊢ (↑a).seq n = if n ≥ 0 then a n.toNat else 0 All goals completed! 🐙@[simp] lemma Sequence.n0_coe (a: ℕ → ℚ) : (a:Sequence).n₀ = 0 := a:ℕ → ℚ⊢ (↑a).n₀ = 0 All goals completed! 🐙

Приклад 5.1.2

abbrev Sequence.squares : Sequence := ((fun n:ℕ ↦ (n^2:ℚ)):Sequence)

Приклад 5.1.2

example (n:ℕ) : Sequence.squares n = n^2 := Sequence.eval_coe _ _

Приклад 5.1.2

abbrev Sequence.three : Sequence := ((fun (_:ℕ) ↦ (3:ℚ)):Sequence)

Приклад 5.1.2

example (n:ℕ) : Sequence.three n = 3 := Sequence.eval_coe _ (fun (_:ℕ) ↦ (3:ℚ))

Приклад 5.1.2

abbrev Sequence.squares_from_three : Sequence := mk' 3 (·^2)

Приклад 5.1.2

example (n:ℤ) (hn: n ≥ 3) : Sequence.squares_from_three n = n^2 := Sequence.eval_mk _ hn
-- потрібно тимчасово вийти з простору імен `Chapter5`, щоб ввести наступне позначення end Chapter5

Невелике узагальнення Визначення 5.1.3 — визначення Unknown identifier `ε`ε-сталості для послідовності з довільною початковою точкою Unknown identifier `n₀`n₀.

abbrev Rat.Steady (ε: ℚ) (a: Chapter5.Sequence) : Prop := ∀ n ≥ a.n₀, ∀ m ≥ a.n₀, ε.Close (a n) (a m)
lemma Rat.steady_def (ε: ℚ) (a: Chapter5.Sequence) : ε.Steady a ↔ ∀ n ≥ a.n₀, ∀ m ≥ a.n₀, ε.Close (a n) (a m) := ε:ℚa:Chapter5.Sequence⊢ ε.Steady a ↔ ∀ n ≥ a.n₀, ∀ m ≥ a.n₀, ε.Close (a.seq n) (a.seq m) All goals completed! 🐙namespace Chapter5

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

lemma Rat.Steady.coe (ε : ℚ) (a:ℕ → ℚ) : ε.Steady a ↔ ∀ n m : ℕ, ε.Close (a n) (a m) := ε:ℚa:ℕ → ℚ⊢ ε.Steady ↑a ↔ ∀ (n m : ℕ), ε.Close (a n) (a m) ε:ℚa:ℕ → ℚ⊢ ε.Steady ↑a → ∀ (n m : ℕ), ε.Close (a n) (a m)ε:ℚa:ℕ → ℚ⊢ (∀ (n m : ℕ), ε.Close (a n) (a m)) → ε.Steady ↑a ε:ℚa:ℕ → ℚ⊢ ε.Steady ↑a → ∀ (n m : ℕ), ε.Close (a n) (a m) ε:ℚa:ℕ → ℚh:ε.Steady ↑an:ℕm:ℕ⊢ ε.Close (a n) (a m); ε:ℚa:ℕ → ℚh:ε.Steady ↑an:ℕm:ℕ⊢ ↑n ≥ (↑a).n₀ε:ℚa:ℕ → ℚh:ε.Steady ↑an:ℕm:ℕ⊢ ↑m ≥ (↑a).n₀ε:ℚa:ℕ → ℚn:ℕm:ℕh:ε.Close ((↑a).seq ↑n) ((↑a).seq ↑m)⊢ ε.Close (a n) (a m) ε:ℚa:ℕ → ℚh:ε.Steady ↑an:ℕm:ℕ⊢ ↑n ≥ (↑a).n₀ε:ℚa:ℕ → ℚh:ε.Steady ↑an:ℕm:ℕ⊢ ↑m ≥ (↑a).n₀ε:ℚa:ℕ → ℚn:ℕm:ℕh:ε.Close ((↑a).seq ↑n) ((↑a).seq ↑m)⊢ ε.Close (a n) (a m) All goals completed! 🐙 ε:ℚa:ℕ → ℚh:∀ (n m : ℕ), ε.Close (a n) (a m)n:ℤhn:n ≥ (↑a).n₀m:ℤhm:m ≥ (↑a).n₀⊢ ε.Close ((↑a).seq n) ((↑a).seq m) ε:ℚa:ℕ → ℚh:∀ (n m : ℕ), ε.Close (a n) (a m)m:ℤhm:m ≥ (↑a).n₀n:ℕ⊢ ε.Close ((↑a).seq ↑n) ((↑a).seq m) ε:ℚa:ℕ → ℚh:∀ (n m : ℕ), ε.Close (a n) (a m)n:ℕm:ℕ⊢ ε.Close ((↑a).seq ↑n) ((↑a).seq ↑m) All goals completed! 🐙

Не в підручнику: послідовність 3, 3, ... є 1-сталою Призначено для демонстрації Chapter5.Rat.Steady.coe (ε : ℚ) (a : ℕ → ℚ) : ε.Steady ↑a ↔ ∀ (n m : ℕ), ε.Close (a n) (a m)Rat.Steady.coe

example : (1:ℚ).Steady ((fun _:ℕ ↦ (3:ℚ)):Sequence) := ⊢ Rat.Steady 1 ↑fun x => 3 All goals completed! 🐙

Порівняйте: якщо потрібно працювати з Rat.Steady (ε : ℚ) (a : Sequence) : PropRat.Steady безпосередньо через перетворення типу, з’являться додаткові умови та , які доведеться враховувати.

example : (1:ℚ).Steady ((fun _:ℕ ↦ (3:ℚ)):Sequence) := ⊢ Rat.Steady 1 ↑fun x => 3 n:ℤa✝¹:n ≥ (↑fun x => 3).n₀m:ℤa✝:m ≥ (↑fun x => 3).n₀⊢ Rat.Close 1 ((↑fun x => 3).seq n) ((↑fun x => 3).seq m); All goals completed! 🐙

Приклад 5.1.5: Послідовність є 1-сталою.

example : (1:ℚ).Steady ((fun n:ℕ ↦ if Even n then (1:ℚ) else (0:ℚ)):Sequence) := ⊢ Rat.Steady 1 ↑fun n => if Even n then 1 else 0 ⊢ ∀ (n m : ℕ), Rat.Close 1 (if Even n then 1 else 0) (if Even m then 1 else 0) n:ℕm:ℕ⊢ Rat.Close 1 (if Even n then 1 else 0) (if Even m then 1 else 0) -- Розділіть на чотири випадки залежно від того, чи є n та m парними або непарними -- У кожному випадку ми знаємо точне значення a n та a m n:ℕm:ℕh✝¹:Even nh✝:Even m⊢ Rat.Close 1 1 1n:ℕm:ℕh✝¹:Even nh✝:¬Even m⊢ Rat.Close 1 1 0n:ℕm:ℕh✝¹:¬Even nh✝:Even m⊢ Rat.Close 1 0 1n:ℕm:ℕh✝¹:¬Even nh✝:¬Even m⊢ Rat.Close 1 0 0 n:ℕm:ℕh✝¹:Even nh✝:Even m⊢ Rat.Close 1 1 1n:ℕm:ℕh✝¹:Even nh✝:¬Even m⊢ Rat.Close 1 1 0n:ℕm:ℕh✝¹:¬Even nh✝:Even m⊢ Rat.Close 1 0 1n:ℕm:ℕh✝¹:¬Even nh✝:¬Even m⊢ Rat.Close 1 0 0 All goals completed! 🐙

Приклад 5.1.5: Послідовність не є ½-сталою.

example : ¬ (0.5:ℚ).Steady ((fun n:ℕ ↦ if Even n then (1:ℚ) else (0:ℚ)):Sequence) := ⊢ ¬Rat.Steady 0.5 ↑fun n => if Even n then 1 else 0 ⊢ ¬∀ (n m : ℕ), Rat.Close 0.5 (if Even n then 1 else 0) (if Even m then 1 else 0) h:∀ (n m : ℕ), Rat.Close 0.5 (if Even n then 1 else 0) (if Even m then 1 else 0)⊢ False; h:Rat.Close 0.5 (if Even 0 then 1 else 0) (if Even 1 then 1 else 0)⊢ False; h:1 ≤ 0.5⊢ False All goals completed! 🐙

Приклад 5.1.5: Послідовність 0.1, 0.01, 0.001, ... є 0.1-сталою.

example : (0.1:ℚ).Steady ((fun n:ℕ ↦ (10:ℚ) ^ (-(n:ℤ)-1) ):Sequence) := ⊢ Rat.Steady 0.1 ↑fun n => 10 ^ (-↑n - 1) ⊢ ∀ (n m : ℕ), Rat.Close 0.1 (10 ^ (-↑n - 1)) (10 ^ (-↑m - 1)) n:ℕm:ℕ⊢ Rat.Close 0.1 (10 ^ (-↑n - 1)) (10 ^ (-↑m - 1)); n:ℕm:ℕ⊢ |10 ^ (-↑n - 1) - 10 ^ (-↑m - 1)| ≤ 0.1 n:ℕm:ℕthis:∀ (n m : ℕ), m ≤ n → |10 ^ (-↑n - 1) - 10 ^ (-↑m - 1)| ≤ 0.1h:¬m ≤ n⊢ |10 ^ (-↑n - 1) - 10 ^ (-↑m - 1)| ≤ 0.1n:ℕm:ℕh:m ≤ n⊢ |10 ^ (-↑n - 1) - 10 ^ (-↑m - 1)| ≤ 0.1 n:ℕm:ℕthis:∀ (n m : ℕ), m ≤ n → |10 ^ (-↑n - 1) - 10 ^ (-↑m - 1)| ≤ 0.1h:¬m ≤ n⊢ |10 ^ (-↑n - 1) - 10 ^ (-↑m - 1)| ≤ 0.1 specialize this m n (n:ℕm:ℕthis:∀ (n m : ℕ), m ≤ n → |10 ^ (-↑n - 1) - 10 ^ (-↑m - 1)| ≤ 0.1h:¬m ≤ n⊢ n ≤ m All goals completed! 🐙); rwa [abs_sub_commn:ℕm:ℕh:¬m ≤ nthis:|10 ^ (-↑m - 1) - 10 ^ (-↑n - 1)| ≤ 0.1⊢ |10 ^ (-↑m - 1) - 10 ^ (-↑n - 1)| ≤ 0.1 n:ℕm:ℕh:m ≤ n⊢ 10 ^ (-↑m - 1) - 10 ^ (-↑n - 1) ≤ 0.1n:ℕm:ℕh:m ≤ n⊢ 0 ≤ 10 ^ (-↑m - 1) - 10 ^ (-↑n - 1) n:ℕm:ℕh:m ≤ n⊢ 10 ^ (-↑m - 1) - 10 ^ (-↑n - 1) ≤ 0.1 n:ℕm:ℕh:m ≤ n⊢ 10 ^ (-↑m - 1) - 10 ^ (-↑n - 1) ≤ 10 ^ (-1) - 0 n:ℕm:ℕh:m ≤ n⊢ 1 ≤ 10n:ℕm:ℕh:m ≤ n⊢ -↑m - 1 ≤ -1n:ℕm:ℕh:m ≤ n⊢ 0 ≤ 10 ^ (-↑n - 1) n:ℕm:ℕh:m ≤ n⊢ 1 ≤ 10n:ℕm:ℕh:m ≤ n⊢ -↑m - 1 ≤ -1n:ℕm:ℕh:m ≤ n⊢ 0 ≤ 10 ^ (-↑n - 1) try n:ℕm:ℕh:m ≤ n⊢ 0 ≤ 10 ^ (-↑n - 1) All goals completed! 🐙 linarith [show (10:ℚ) ^ (-(n:ℤ)-1) ≤ (10:ℚ) ^ (-(m:ℤ)-1) ⊢ Rat.Steady 0.1 ↑fun n => 10 ^ (-↑n - 1) n:ℕm:ℕh:m ≤ n⊢ 1 ≤ 10; All goals completed! 🐙]

Приклад 5.1.5: Послідовність 0.1, 0.01, 0.001, ... не є 0.01-сталою. Залишено як вправу.

declaration uses 'sorry'example : ¬(0.01:ℚ).Steady ((fun n:ℕ ↦ (10:ℚ) ^ (-(n:ℤ)-1) ):Sequence) := ⊢ ¬Rat.Steady 1e-2 ↑fun n => 10 ^ (-↑n - 1) All goals completed! 🐙

Приклад 5.1.5: Послідовність 1, 2, 4, 8, ... не є ε-сталою для жодного ε. Залишено як вправу.

declaration uses 'sorry'example (ε:ℚ) : ¬ ε.Steady ((fun n:ℕ ↦ (2 ^ (n+1):ℚ) ):Sequence) := ε:ℚ⊢ ¬ε.Steady ↑fun n => 2 ^ (n + 1) All goals completed! 🐙

Приклад 5.1.5:Послідовність 2, 2, 2, ... є ε-сталою для будь-якого ε > 0.

example (ε:ℚ) (hε: ε>0) : ε.Steady ((fun _:ℕ ↦ (2:ℚ) ):Sequence) := ε:ℚhε:ε > 0⊢ ε.Steady ↑fun x => 2 ε:ℚhε:ε > 0⊢ ∀ (n m : ℕ), ε.Close 2 2; ε:ℚhε:ε > 0⊢ 0 ≤ ε; All goals completed! 🐙

Послідовність 10, 0, 0, ... є 10-сталою.

example : (10:ℚ).Steady ((fun n:ℕ ↦ if n = 0 then (10:ℚ) else (0:ℚ)):Sequence) := ⊢ Rat.Steady 10 ↑fun n => if n = 0 then 10 else 0 ⊢ ∀ (n m : ℕ), Rat.Close 10 (if n = 0 then 10 else 0) (if m = 0 then 10 else 0); n:ℕm:ℕ⊢ Rat.Close 10 (if n = 0 then 10 else 0) (if m = 0 then 10 else 0) -- Розділіть на 4 випадки залежно від того, чи n та m дорівнюють 0, чи ні. n:ℕm:ℕh✝¹:n = 0h✝:m = 0⊢ Rat.Close 10 10 10n:ℕm:ℕh✝¹:n = 0h✝:¬m = 0⊢ Rat.Close 10 10 0n:ℕm:ℕh✝¹:¬n = 0h✝:m = 0⊢ Rat.Close 10 0 10n:ℕm:ℕh✝¹:¬n = 0h✝:¬m = 0⊢ Rat.Close 10 0 0 n:ℕm:ℕh✝¹:n = 0h✝:m = 0⊢ Rat.Close 10 10 10n:ℕm:ℕh✝¹:n = 0h✝:¬m = 0⊢ Rat.Close 10 10 0n:ℕm:ℕh✝¹:¬n = 0h✝:m = 0⊢ Rat.Close 10 0 10n:ℕm:ℕh✝¹:¬n = 0h✝:¬m = 0⊢ Rat.Close 10 0 0 All goals completed! 🐙

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

example (ε:ℚ) (hε:ε<10): ¬ ε.Steady ((fun n:ℕ ↦ if n = 0 then (10:ℚ) else (0:ℚ)):Sequence) := ε:ℚhε:ε < 10⊢ ¬ε.Steady ↑fun n => if n = 0 then 10 else 0 ε:ℚhε:ε.Steady ↑fun n => if n = 0 then 10 else 0⊢ 10 ≤ ε; ε:ℚhε:∀ (n m : ℕ), ε.Close (if n = 0 then 10 else 0) (if m = 0 then 10 else 0)⊢ 10 ≤ ε; ε:ℚhε:ε.Close (if 0 = 0 then 10 else 0) (if 1 = 0 then 10 else 0)⊢ 10 ≤ ε; All goals completed! 🐙

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

abbrev Sequence.from (a:Sequence) (n₁:ℤ) : Sequence := mk' (max a.n₀ n₁) (fun n ↦ a (n:ℤ))
lemma Sequence.from_eval (a:Sequence) {n₁ n:ℤ} (hn: n ≥ n₁) : (a.from n₁) n = a n := a:Sequencen₁:ℤn:ℤhn:n ≥ n₁⊢ (a.from n₁).seq n = a.seq n a:Sequencen₁:ℤn:ℤhn:n ≥ n₁⊢ n < a.n₀ → 0 = a.seq n; a:Sequencen₁:ℤn:ℤhn:n ≥ n₁h:n < a.n₀⊢ 0 = a.seq n; All goals completed! 🐙end Chapter5

Визначення 5.1.6 (Зрештою ε-стала)

abbrev Rat.EventuallySteady (ε: ℚ) (a: Chapter5.Sequence) : Prop := ∃ N ≥ a.n₀, ε.Steady (a.from N)
lemma Rat.eventuallySteady_def (ε: ℚ) (a: Chapter5.Sequence) : ε.EventuallySteady a ↔ ∃ N ≥ a.n₀, ε.Steady (a.from N) := ε:ℚa:Chapter5.Sequence⊢ ε.EventuallySteady a ↔ ∃ N ≥ a.n₀, ε.Steady (a.from N) All goals completed! 🐙namespace Chapter5

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

lemma Sequence.ex_5_1_7_a : ¬ (0.1:ℚ).Steady ((fun n:ℕ ↦ (n+1:ℚ)⁻¹ ):Sequence) := ⊢ ¬Rat.Steady 0.1 ↑fun n => (↑n + 1)⁻¹ h:Rat.Steady 0.1 ↑fun n => (↑n + 1)⁻¹⊢ False; h:∀ (n m : ℕ), Rat.Close 0.1 (↑n + 1)⁻¹ (↑m + 1)⁻¹⊢ False; h:Rat.Close 0.1 (↑0 + 1)⁻¹ (↑2 + 1)⁻¹⊢ False; h:|1 - (2 + 1)⁻¹| ≤ 0.1⊢ False; h:|2 / 3| ≤ 1 / 10⊢ False h:2 / 3 ≤ 1 / 10⊢ Falseh:|2 / 3| ≤ 1 / 10⊢ 0 ≤ 2 / 3 h:2 / 3 ≤ 1 / 10⊢ Falseh:|2 / 3| ≤ 1 / 10⊢ 0 ≤ 2 / 3 All goals completed! 🐙

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

lemma Sequence.ex_5_1_7_b : (0.1:ℚ).Steady (((fun n:ℕ ↦ (n+1:ℚ)⁻¹ ):Sequence).from 10) := ⊢ Rat.Steady 0.1 ((↑fun n => (↑n + 1)⁻¹).from 10) ⊢ ∀ n ≥ ((↑fun n => (↑n + 1)⁻¹).from 10).n₀, ∀ m ≥ ((↑fun n => (↑n + 1)⁻¹).from 10).n₀, Rat.Close 0.1 (((↑fun n => (↑n + 1)⁻¹).from 10).seq n) (((↑fun n => (↑n + 1)⁻¹).from 10).seq m) n:ℤhn:n ≥ ((↑fun n => (↑n + 1)⁻¹).from 10).n₀m:ℤhm:m ≥ ((↑fun n => (↑n + 1)⁻¹).from 10).n₀⊢ Rat.Close 0.1 (((↑fun n => (↑n + 1)⁻¹).from 10).seq n) (((↑fun n => (↑n + 1)⁻¹).from 10).seq m); n:ℤm:ℤhn:10 ≤ nhm:10 ≤ m⊢ Rat.Close 0.1 (((↑fun n => (↑n + 1)⁻¹).from 10).seq n) (((↑fun n => (↑n + 1)⁻¹).from 10).seq m) lift n to ℕ using (n:ℤm:ℤhn:10 ≤ nhm:10 ≤ m⊢ 0 ≤ n All goals completed! 🐙) lift m to ℕ using (m:ℤhm:10 ≤ mn:ℕhn:10 ≤ ↑n⊢ 0 ≤ m All goals completed! 🐙) n:ℕm:ℕhn:10 ≤ nhm:10 ≤ m⊢ |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1 n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mthis:∀ (n m : ℕ), 10 ≤ n → 10 ≤ m → m ≤ n → |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1h:¬m ≤ n⊢ |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:m ≤ n⊢ |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1 n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mthis:∀ (n m : ℕ), 10 ≤ n → 10 ≤ m → m ≤ n → |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1h:¬m ≤ n⊢ |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1 n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mthis:∀ (n m : ℕ), 10 ≤ n → 10 ≤ m → m ≤ n → |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1h:¬m ≤ n⊢ 10 ≤ mn:ℕm:ℕhn:10 ≤ nhm:10 ≤ mthis:∀ (n m : ℕ), 10 ≤ n → 10 ≤ m → m ≤ n → |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1h:¬m ≤ n⊢ 10 ≤ nn:ℕm:ℕhn:10 ≤ nhm:10 ≤ mthis:∀ (n m : ℕ), 10 ≤ n → 10 ≤ m → m ≤ n → |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1h:¬m ≤ n⊢ n ≤ mn:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:¬m ≤ nthis:|(↑m + 1)⁻¹ - (↑n + 1)⁻¹| ≤ 0.1⊢ |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1 n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mthis:∀ (n m : ℕ), 10 ≤ n → 10 ≤ m → m ≤ n → |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1h:¬m ≤ n⊢ 10 ≤ mn:ℕm:ℕhn:10 ≤ nhm:10 ≤ mthis:∀ (n m : ℕ), 10 ≤ n → 10 ≤ m → m ≤ n → |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1h:¬m ≤ n⊢ 10 ≤ nn:ℕm:ℕhn:10 ≤ nhm:10 ≤ mthis:∀ (n m : ℕ), 10 ≤ n → 10 ≤ m → m ≤ n → |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1h:¬m ≤ n⊢ n ≤ mn:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:¬m ≤ nthis:|(↑m + 1)⁻¹ - (↑n + 1)⁻¹| ≤ 0.1⊢ |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1 try All goals completed! 🐙 rwa [abs_sub_commn:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:¬m ≤ nthis:|(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1⊢ |(↑n + 1)⁻¹ - (↑m + 1)⁻¹| ≤ 0.1 at this n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:m ≤ n⊢ |(↑m + 1)⁻¹ - (↑n + 1)⁻¹| ≤ 0.1 have : ((n:ℚ) + 1)⁻¹ ≤ ((m:ℚ) + 1)⁻¹ := ⊢ Rat.Steady 0.1 ((↑fun n => (↑n + 1)⁻¹).from 10) All goals completed! 🐙 n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:m ≤ nthis:(↑_fvar.85687 + 1)⁻¹ ≤ (↑_fvar.85688 + 1)⁻¹ := ?_mvar.86752⊢ (↑m + 1)⁻¹ - (↑n + 1)⁻¹ ≤ 10⁻¹ - 0 n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:m ≤ nthis:(↑_fvar.85687 + 1)⁻¹ ≤ (↑_fvar.85688 + 1)⁻¹ := ?_mvar.86752⊢ 10 ≤ ↑m + 1n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:m ≤ nthis:(↑_fvar.85687 + 1)⁻¹ ≤ (↑_fvar.85688 + 1)⁻¹ := ?_mvar.86752⊢ 0 ≤ (↑n + 1)⁻¹ n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:m ≤ nthis:(↑_fvar.85687 + 1)⁻¹ ≤ (↑_fvar.85688 + 1)⁻¹ := ?_mvar.86752⊢ 10 ≤ ↑m + 1 n:ℕm:ℕhn:10 ≤ nhm:10 ≤ mh:m ≤ nthis:(↑_fvar.85687 + 1)⁻¹ ≤ (↑_fvar.85688 + 1)⁻¹ := ?_mvar.86752⊢ 10 ≤ m + 1; All goals completed! 🐙 All goals completed! 🐙

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

lemma Sequence.ex_5_1_7_c : (0.1:ℚ).EventuallySteady ((fun n:ℕ ↦ (n+1:ℚ)⁻¹ ):Sequence) := ⟨10, ⊢ 10 ≥ (↑fun n => (↑n + 1)⁻¹).n₀ All goals completed! 🐙, ex_5_1_7_b⟩

Приклад 5.1.7

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

lemma declaration uses 'sorry'Sequence.ex_5_1_7_d {ε:ℚ} (hε:ε>0) : ε.EventuallySteady ((fun n:ℕ ↦ if n=0 then (10:ℚ) else (0:ℚ) ):Sequence) := ε:ℚhε:ε > 0⊢ ε.EventuallySteady ↑fun n => if n = 0 then 10 else 0 All goals completed! 🐙
abbrev Sequence.IsCauchy (a:Sequence) : Prop := ∀ ε > (0:ℚ), ε.EventuallySteady alemma Sequence.isCauchy_def (a:Sequence) : a.IsCauchy ↔ ∀ ε > (0:ℚ), ε.EventuallySteady a := a:Sequence⊢ a.IsCauchy ↔ ∀ ε > 0, ε.EventuallySteady a All goals completed! 🐙

Визначення послідовностей Коші для послідовності, що починається з 0.

lemma Sequence.IsCauchy.coe (a:ℕ → ℚ) : (a:Sequence).IsCauchy ↔ ∀ ε > (0:ℚ), ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε := a:ℕ → ℚ⊢ (↑a).IsCauchy ↔ ∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε a:ℕ → ℚ⊢ (↑a).IsCauchy → ∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εa:ℕ → ℚ⊢ (∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε) → (↑a).IsCauchy a:ℕ → ℚ⊢ (↑a).IsCauchy → ∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εa:ℕ → ℚ⊢ (∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε) → (↑a).IsCauchy a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0⊢ ε.EventuallySteady ↑a a:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε a:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ (↑a).n₀h':ε.Steady ((↑a).from N)⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε a:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕh':ε.Steady ((↑a).from ↑N)⊢ ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε; a:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕh':ε.Steady ((↑a).from ↑N)⊢ ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε a:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕh':ε.Steady ((↑a).from ↑N)j:ℕa✝¹:j ≥ Nk:ℕa✝:k ≥ N⊢ Section_4_3.dist (a j) (a k) ≤ ε; a:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕj:ℕa✝¹:j ≥ Nk:ℕa✝:k ≥ Nh':∀ (n : ℤ), ↑N ≤ n → ∀ (m : ℤ), ↑N ≤ m → ε.Close (if ↑N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0) (if ↑N ≤ m then if 0 ≤ m then a m.toNat else 0 else 0)⊢ Section_4_3.dist (a j) (a k) ≤ ε; a:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕj:ℕa✝¹:j ≥ Nk:ℕa✝:k ≥ Nh':∀ (n : ℤ), ↑N ≤ n → ∀ (m : ℤ), ↑N ≤ m → ε.Close (if ↑N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0) (if ↑N ≤ m then if 0 ≤ m then a m.toNat else 0 else 0)⊢ ↑N ≤ ↑ja:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕj:ℕa✝¹:j ≥ Nk:ℕa✝:k ≥ Nh':∀ (n : ℤ), ↑N ≤ n → ∀ (m : ℤ), ↑N ≤ m → ε.Close (if ↑N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0) (if ↑N ≤ m then if 0 ≤ m then a m.toNat else 0 else 0)⊢ ↑N ≤ ↑ka:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕj:ℕa✝¹:j ≥ Nk:ℕa✝:k ≥ Nh':ε.Close (if ↑N ≤ ↑j then if 0 ≤ ↑j then a (↑j).toNat else 0 else 0) (if ↑N ≤ ↑k then if 0 ≤ ↑k then a (↑k).toNat else 0 else 0)⊢ Section_4_3.dist (a j) (a k) ≤ ε a:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕj:ℕa✝¹:j ≥ Nk:ℕa✝:k ≥ Nh':∀ (n : ℤ), ↑N ≤ n → ∀ (m : ℤ), ↑N ≤ m → ε.Close (if ↑N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0) (if ↑N ≤ m then if 0 ≤ m then a m.toNat else 0 else 0)⊢ ↑N ≤ ↑ja:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕj:ℕa✝¹:j ≥ Nk:ℕa✝:k ≥ Nh':∀ (n : ℤ), ↑N ≤ n → ∀ (m : ℤ), ↑N ≤ m → ε.Close (if ↑N ≤ n then if 0 ≤ n then a n.toNat else 0 else 0) (if ↑N ≤ m then if 0 ≤ m then a m.toNat else 0 else 0)⊢ ↑N ≤ ↑ka:ℕ → ℚh:(↑a).IsCauchyε:ℚhε:ε > 0N:ℕj:ℕa✝¹:j ≥ Nk:ℕa✝:k ≥ Nh':ε.Close (if ↑N ≤ ↑j then if 0 ≤ ↑j then a (↑j).toNat else 0 else 0) (if ↑N ≤ ↑k then if 0 ≤ ↑k then a (↑k).toNat else 0 else 0)⊢ Section_4_3.dist (a j) (a k) ≤ ε try All goals completed! 🐙 a:ℕ → ℚh:(↑a).IsCauchyε:ℚN:ℕj:ℕk:ℕhε:0 < εa✝¹:N ≤ ja✝:N ≤ kh':ε.Close (a j) (a k)⊢ Section_4_3.dist (a j) (a k) ≤ ε; All goals completed! 🐙 a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε⊢ ε.EventuallySteady ↑a refine ⟨ max N 0, a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ ε⊢ max (↑N) 0 ≥ (↑a).n₀ All goals completed! 🐙, ?_ ⟩ a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤhn:n ≥ ((↑a).from (max (↑N) 0)).n₀m:ℤhm:m ≥ ((↑a).from (max (↑N) 0)).n₀⊢ ε.Close (((↑a).from (max (↑N) 0)).seq n) (((↑a).from (max (↑N) 0)).seq m); a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ ε.Close (((↑a).from (max (↑N) 0)).seq n) (((↑a).from (max (↑N) 0)).seq m) a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ mnpos:0 ≤ _fvar.131394 := ?_mvar.137582⊢ ε.Close (((↑a).from (max (↑N) 0)).seq n) (((↑a).from (max (↑N) 0)).seq m)a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ 0 ≤ n a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ mnpos:0 ≤ _fvar.131394 := ?_mvar.137582mpos:0 ≤ _fvar.131400 := ?_mvar.137624⊢ ε.Close (((↑a).from (max (↑N) 0)).seq n) (((↑a).from (max (↑N) 0)).seq m)a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ mnpos:0 ≤ _fvar.131394 := ?_mvar.137582⊢ 0 ≤ ma:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ 0 ≤ n a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εm:ℤhm:↑N ≤ mmpos:0 ≤ _fvar.131400 := ?_mvar.137624n:ℕhn:↑N ≤ ↑n⊢ ε.Close (((↑a).from (max (↑N) 0)).seq ↑n) (((↑a).from (max (↑N) 0)).seq m)a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ mnpos:0 ≤ _fvar.131394 := ?_mvar.137582⊢ 0 ≤ ma:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ 0 ≤ n a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℕhn:↑N ≤ ↑nm:ℕhm:↑N ≤ ↑m⊢ ε.Close (((↑a).from (max (↑N) 0)).seq ↑n) (((↑a).from (max (↑N) 0)).seq ↑m)a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ mnpos:0 ≤ _fvar.131394 := ?_mvar.137582⊢ 0 ≤ ma:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ 0 ≤ n a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℕhn:↑N ≤ ↑nm:ℕhm:↑N ≤ ↑m⊢ ε.Close (a n) (a m)a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ mnpos:0 ≤ _fvar.131394 := ?_mvar.137582⊢ 0 ≤ ma:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ 0 ≤ n; a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℕhn:↑N ≤ ↑nm:ℕhm:↑N ≤ ↑m⊢ n ≥ Na:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℕhn:↑N ≤ ↑nm:ℕhm:↑N ≤ ↑m⊢ m ≥ Na:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕn:ℕhn:↑N ≤ ↑nm:ℕhm:↑N ≤ ↑mh':Section_4_3.dist (a n) (a m) ≤ ε⊢ ε.Close (a n) (a m)a:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ mnpos:0 ≤ _fvar.131394 := ?_mvar.137582⊢ 0 ≤ ma:ℕ → ℚh:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εε:ℚhε:ε > 0N:ℕh':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist (a j) (a k) ≤ εn:ℤm:ℤhn:↑N ≤ nhm:↑N ≤ m⊢ 0 ≤ n all_goals try All goals completed! 🐙 All goals completed! 🐙
lemma 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 j) (mk' n₀ a k) ≤ ε := 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) ≤ ε 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) ≤ εn₀:ℤa:{ n // n ≥ n₀ } → ℚ⊢ (∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε) → (mk' n₀ a).IsCauchy 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) ≤ εn₀:ℤa:{ n // n ≥ n₀ } → ℚ⊢ (∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε) → (mk' n₀ a).IsCauchy n₀:ℤa:{ n // n ≥ n₀ } → ℚh:∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εε:ℚhε:ε > 0⊢ ε.EventuallySteady (mk' n₀ a) n₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0⊢ ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εn₀:ℤa:{ n // n ≥ n₀ } → ℚh:∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εε:ℚhε:ε > 0⊢ ε.EventuallySteady (mk' n₀ a) n₀:ℤa:{ n // n ≥ n₀ } → ℚh:∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εε:ℚhε:ε > 0N:ℤhN:N ≥ n₀h':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε⊢ ε.EventuallySteady (mk' n₀ a) n₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ (mk' n₀ a).n₀h':ε.Steady ((mk' n₀ a).from N)⊢ ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε n₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ (mk' n₀ a).n₀h':ε.Steady ((mk' n₀ a).from N)⊢ ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε; n₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀h':ε.Steady ((mk' n₀ a).from N)⊢ ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε; n₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀h':ε.Steady ((mk' n₀ a).from N)j:ℤa✝¹:j ≥ Nk:ℤa✝:k ≥ N⊢ Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε n₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀j:ℤa✝¹:j ≥ Nk:ℤa✝:k ≥ Nh':∀ n ≥ N, ∀ m ≥ N, ε.Close (if h : n ≥ N then if h_1 : n ≥ n₀ then a ⟨n, ⋯⟩ else 0 else 0) (if h : m ≥ N then if h_1 : m ≥ n₀ then a ⟨m, ⋯⟩ else 0 else 0)⊢ Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε n₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀j:ℤa✝¹:j ≥ Nk:ℤa✝:k ≥ Nh':∀ n ≥ N, ∀ m ≥ N, ε.Close (if h : n ≥ N then if h_1 : n ≥ n₀ then a ⟨n, ⋯⟩ else 0 else 0) (if h : m ≥ N then if h_1 : m ≥ n₀ then a ⟨m, ⋯⟩ else 0 else 0)⊢ j ≥ Nn₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀j:ℤa✝¹:j ≥ Nk:ℤa✝:k ≥ Nh':∀ n ≥ N, ∀ m ≥ N, ε.Close (if h : n ≥ N then if h_1 : n ≥ n₀ then a ⟨n, ⋯⟩ else 0 else 0) (if h : m ≥ N then if h_1 : m ≥ n₀ then a ⟨m, ⋯⟩ else 0 else 0)⊢ k ≥ Nn₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀j:ℤa✝¹:j ≥ Nk:ℤa✝:k ≥ Nh':ε.Close (if h : j ≥ N then if h_1 : j ≥ n₀ then a ⟨j, ⋯⟩ else 0 else 0) (if h : k ≥ N then if h_1 : k ≥ n₀ then a ⟨k, ⋯⟩ else 0 else 0)⊢ Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε n₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀j:ℤa✝¹:j ≥ Nk:ℤa✝:k ≥ Nh':∀ n ≥ N, ∀ m ≥ N, ε.Close (if h : n ≥ N then if h_1 : n ≥ n₀ then a ⟨n, ⋯⟩ else 0 else 0) (if h : m ≥ N then if h_1 : m ≥ n₀ then a ⟨m, ⋯⟩ else 0 else 0)⊢ j ≥ Nn₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀j:ℤa✝¹:j ≥ Nk:ℤa✝:k ≥ Nh':∀ n ≥ N, ∀ m ≥ N, ε.Close (if h : n ≥ N then if h_1 : n ≥ n₀ then a ⟨n, ⋯⟩ else 0 else 0) (if h : m ≥ N then if h_1 : m ≥ n₀ then a ⟨m, ⋯⟩ else 0 else 0)⊢ k ≥ Nn₀:ℤa:{ n // n ≥ n₀ } → ℚh:(mk' n₀ a).IsCauchyε:ℚhε:ε > 0N:ℤhN:N ≥ n₀j:ℤa✝¹:j ≥ Nk:ℤa✝:k ≥ Nh':ε.Close (if h : j ≥ N then if h_1 : j ≥ n₀ then a ⟨j, ⋯⟩ else 0 else 0) (if h : k ≥ N then if h_1 : k ≥ n₀ then a ⟨k, ⋯⟩ else 0 else 0)⊢ Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε try All goals completed! 🐙 simp_all [show n₀ ≤ j 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) ≤ ε All goals completed! 🐙, show n₀ ≤ k 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) ≤ ε All goals completed! 🐙] All goals completed! 🐙 refine ⟨ max n₀ N, n₀:ℤa:{ n // n ≥ n₀ } → ℚh:∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εε:ℚhε:ε > 0N:ℤhN:N ≥ n₀h':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ ε⊢ max n₀ N ≥ (mk' n₀ a).n₀ All goals completed! 🐙, ?_ ⟩ n₀:ℤa:{ n // n ≥ n₀ } → ℚh:∀ ε > 0, ∃ N ≥ n₀, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εε:ℚhε:ε > 0N:ℤhN:N ≥ n₀h':∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' n₀ a).seq j) ((mk' n₀ a).seq k) ≤ εn:ℤa✝¹:n ≥ ((mk' n₀ a).from (max n₀ N)).n₀m:ℤa✝:m ≥ ((mk' n₀ a).from (max n₀ N)).n₀⊢ ε.Close (((mk' n₀ a).from (max n₀ N)).seq n) (((mk' n₀ a).from (max n₀ N)).seq m); n₀:ℤa:{ n // n ≥ n₀ } → ℚε:ℚN:ℤhN✝:N ≥ n₀n:ℤa✝³:n ≥ ((mk' n₀ a).from (max n₀ N)).n₀m:ℤa✝²:m ≥ ((mk' n₀ a).from (max n₀ N)).n₀h:∀ (ε : ℚ), 0 < ε → ∃ N, n₀ ≤ N ∧ ∀ (j : ℤ), N ≤ j → ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εhε:0 < εhN:n₀ ≤ Nh':∀ (j : ℤ), N ≤ j → ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εa✝¹:N ≤ na✝:N ≤ m⊢ ε.Close (if h : n₀ ≤ n then a ⟨n, ⋯⟩ else 0) (if h : n₀ ≤ m then a ⟨m, ⋯⟩ else 0) n₀:ℤa:{ n // n ≥ n₀ } → ℚε:ℚN:ℤhN✝:N ≥ n₀n:ℤa✝³:n ≥ ((mk' n₀ a).from (max n₀ N)).n₀m:ℤa✝²:m ≥ ((mk' n₀ a).from (max n₀ N)).n₀h:∀ (ε : ℚ), 0 < ε → ∃ N, n₀ ≤ N ∧ ∀ (j : ℤ), N ≤ j → ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εhε:0 < εhN:n₀ ≤ Nh':∀ (j : ℤ), N ≤ j → ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εa✝¹:N ≤ na✝:N ≤ m⊢ N ≤ mn₀:ℤa:{ n // n ≥ n₀ } → ℚε:ℚN:ℤhN✝:N ≥ n₀n:ℤa✝³:n ≥ ((mk' n₀ a).from (max n₀ N)).n₀m:ℤa✝²:m ≥ ((mk' n₀ a).from (max n₀ N)).n₀h:∀ (ε : ℚ), 0 < ε → ∃ N, n₀ ≤ N ∧ ∀ (j : ℤ), N ≤ j → ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εhε:0 < εhN:n₀ ≤ Nh':∀ (j : ℤ), N ≤ j → ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εa✝¹:N ≤ na✝:N ≤ m⊢ N ≤ n n₀:ℤa:{ n // n ≥ n₀ } → ℚε:ℚN:ℤhN✝:N ≥ n₀n:ℤa✝³:n ≥ ((mk' n₀ a).from (max n₀ N)).n₀m:ℤa✝²:m ≥ ((mk' n₀ a).from (max n₀ N)).n₀h:∀ (ε : ℚ), 0 < ε → ∃ N, n₀ ≤ N ∧ ∀ (j : ℤ), N ≤ j → ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εhε:0 < εhN:n₀ ≤ Nh':∀ (j : ℤ), N ≤ j → ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εa✝¹:N ≤ na✝:N ≤ m⊢ N ≤ mn₀:ℤa:{ n // n ≥ n₀ } → ℚε:ℚN:ℤhN✝:N ≥ n₀n:ℤa✝³:n ≥ ((mk' n₀ a).from (max n₀ N)).n₀m:ℤa✝²:m ≥ ((mk' n₀ a).from (max n₀ N)).n₀h:∀ (ε : ℚ), 0 < ε → ∃ N, n₀ ≤ N ∧ ∀ (j : ℤ), N ≤ j → ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εhε:0 < εhN:n₀ ≤ Nh':∀ (j : ℤ), N ≤ j → ∀ (k : ℤ), N ≤ k → Section_4_3.dist (if h : n₀ ≤ j then a ⟨j, ⋯⟩ else 0) (if h : n₀ ≤ k then a ⟨k, ⋯⟩ else 0) ≤ εa✝¹:N ≤ na✝:N ≤ m⊢ N ≤ n All goals completed! 🐙noncomputable def Sequence.sqrt_two : Sequence := (fun n:ℕ ↦ ((⌊ (Real.sqrt 2)*10^n ⌋ / 10^n):ℚ))

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

theorem declaration uses 'sorry'Sequence.ex_5_1_10_a : (1:ℚ).Steady sqrt_two := ⊢ Rat.Steady 1 sqrt_two All goals completed! 🐙

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

theorem declaration uses 'sorry'Sequence.ex_5_1_10_b : (0.1:ℚ).Steady (sqrt_two.from 1) := ⊢ Rat.Steady 0.1 (sqrt_two.from 1) All goals completed! 🐙
theorem declaration uses 'sorry'Sequence.ex_5_1_10_c : (0.1:ℚ).EventuallySteady sqrt_two := ⊢ Rat.EventuallySteady 0.1 sqrt_two All goals completed! 🐙

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

theorem Sequence.IsCauchy.harmonic : (mk' 1 (fun n ↦ (1:ℚ)/n)).IsCauchy := ⊢ (mk' 1 fun n => 1 / ↑↑n).IsCauchy ⊢ ∀ ε > 0, ∃ N ≥ 1, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' 1 fun n => 1 / ↑↑n).seq j) ((mk' 1 fun n => 1 / ↑↑n).seq k) ≤ ε ε:ℚhε:ε > 0⊢ ∃ N ≥ 1, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' 1 fun n => 1 / ↑↑n).seq j) ((mk' 1 fun n => 1 / ↑↑n).seq k) ≤ ε -- Ми йдемо у зворотному порядку від книги — спочатку обираємо N таке, що N > 1/ε. ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / ε⊢ ∃ N ≥ 1, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((mk' 1 fun n => 1 / ↑↑n).seq j) ((mk' 1 fun n => 1 / ↑↑n).seq k) ≤ ε have hN' : N > 0 := ⊢ (mk' 1 fun n => 1 / ↑↑n).IsCauchy ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εthis:0 < 1 / ε⊢ N > 0 ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εthis✝:0 < 1 / εthis:0 < ↑N⊢ N > 0 All goals completed! 🐙 refine ⟨ N, ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':_fvar.250039 > 0 := Eq.mp (Eq.trans (congrArg (fun x => x < ↑_fvar.250039) (Eq.symm Nat.cast_zero)) Nat.cast_lt._simp_1) (gt_trans _fvar.250040 (one_div_pos.mpr _fvar.249878))⊢ ↑N ≥ 1 All goals completed! 🐙, ?_ ⟩ ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':_fvar.250039 > 0 := ?_mvar.251160j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑N⊢ Section_4_3.dist ((mk' 1 fun n => 1 / ↑↑n).seq j) ((mk' 1 fun n => 1 / ↑↑n).seq k) ≤ ε lift j to ℕ using (ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':_fvar.250039 > 0 := Eq.mp (Eq.trans (congrArg (fun x => x < ↑_fvar.250039) (Eq.symm Nat.cast_zero)) Nat.cast_lt._simp_1) (gt_trans _fvar.250040 (one_div_pos.mpr _fvar.249878))j:ℤhj:j ≥ ↑Nk:ℤhk:k ≥ ↑N⊢ 0 ≤ j All goals completed! 🐙) lift k to ℕ using (ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':_fvar.250039 > 0 := Eq.mp (Eq.trans (congrArg (fun x => x < ↑_fvar.250039) (Eq.symm Nat.cast_zero)) Nat.cast_lt._simp_1) (gt_trans _fvar.250040 (one_div_pos.mpr _fvar.249878))k:ℤhk:k ≥ ↑Nj:ℕhj:↑j ≥ ↑N⊢ 0 ≤ k All goals completed! 🐙) ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':_fvar.250039 > 0 := ?_mvar.251160j:ℕk:ℕhj:N ≤ jhk:N ≤ k⊢ Section_4_3.dist ((mk' 1 fun n => 1 / ↑↑n).seq ↑j) ((mk' 1 fun n => 1 / ↑↑n).seq ↑k) ≤ ε ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':_fvar.250039 > 0 := ?_mvar.251160j:ℕk:ℕhj:N ≤ jhk:N ≤ k⊢ Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ ε have hdist : Section_4_3.dist ((1:ℚ)/j) ((1:ℚ)/k) ≤ (1:ℚ)/N := ⊢ (mk' 1 fun n => 1 / ↑↑n).IsCauchy ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':_fvar.250039 > 0 := ?_mvar.251160j:ℕk:ℕhj:N ≤ jhk:N ≤ k⊢ 1 / ↑j - 1 / ↑k ≤ 1 / ↑N ∧ -(1 / ↑j - 1 / ↑k) ≤ 1 / ↑N /- Ми встановлюємо такі межі: - 1/j ∈ [0, 1/N] - 1/k ∈ [0, 1/N] Це означає, що відстань між 1/j та 1/k не перевищує 1/N — коли вони максимально "рознесені". -/ have : 1/j ≤ (1:ℚ)/N := ⊢ (mk' 1 fun n => 1 / ↑↑n).IsCauchy All goals completed! 🐙 ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':_fvar.250039 > 0 := ?_mvar.251160j:ℕk:ℕhj:N ≤ jhk:N ≤ kthis✝:1 / ↑_fvar.497087 ≤ 1 / ↑_fvar.250039 := ?_mvar.514962this:0 ≤ 1 / ↑j⊢ 1 / ↑j - 1 / ↑k ≤ 1 / ↑N ∧ -(1 / ↑j - 1 / ↑k) ≤ 1 / ↑N have : 1/k ≤ (1:ℚ)/N := ⊢ (mk' 1 fun n => 1 / ↑↑n).IsCauchy All goals completed! 🐙 ε:ℚhε:ε > 0N:ℕhN:↑N > 1 / εhN':_fvar.250039 > 0 := ?_mvar.251160j:ℕk:ℕhj:N ≤ jhk:N ≤ kthis✝²:1 / ↑_fvar.497087 ≤ 1 / ↑_fvar.250039 := ?_mvar.514962this✝¹:0 ≤ 1 / ↑jthis✝:1 / ↑_fvar.499385 ≤ 1 / ↑_fvar.250039 := ?_mvar.529008this:0 ≤ 1 / ↑k⊢ 1 / ↑j - 1 / ↑k ≤ 1 / ↑N ∧ -(1 / ↑j - 1 / ↑k) ≤ 1 / ↑N All goals completed! 🐙 ε:ℚN:ℕj:ℕk:ℕhj:N ≤ jhk:N ≤ khε:0 < εhN:ε⁻¹ < ↑NhN':0 < Nhdist:Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ (↑N)⁻¹⊢ Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ ε; ε:ℚN:ℕj:ℕk:ℕhj:N ≤ jhk:N ≤ khε:0 < εhN:ε⁻¹ < ↑NhN':0 < Nhdist:Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ (↑N)⁻¹⊢ (↑N)⁻¹ ≤ ε ε:ℚN:ℕj:ℕk:ℕhj:N ≤ jhk:N ≤ khε:0 < εhN:ε⁻¹ < ↑NhN':0 < Nhdist:Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ (↑N)⁻¹⊢ ε⁻¹ ≤ ↑Nε:ℚN:ℕj:ℕk:ℕhj:N ≤ jhk:N ≤ khε:0 < εhN:ε⁻¹ < ↑NhN':0 < Nhdist:Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ (↑N)⁻¹⊢ 0 < ↑Nε:ℚN:ℕj:ℕk:ℕhj:N ≤ jhk:N ≤ khε:0 < εhN:ε⁻¹ < ↑NhN':0 < Nhdist:Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ (↑N)⁻¹⊢ 0 < ε ε:ℚN:ℕj:ℕk:ℕhj:N ≤ jhk:N ≤ khε:0 < εhN:ε⁻¹ < ↑NhN':0 < Nhdist:Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ (↑N)⁻¹⊢ ε⁻¹ ≤ ↑Nε:ℚN:ℕj:ℕk:ℕhj:N ≤ jhk:N ≤ khε:0 < εhN:ε⁻¹ < ↑NhN':0 < Nhdist:Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ (↑N)⁻¹⊢ 0 < ↑Nε:ℚN:ℕj:ℕk:ℕhj:N ≤ jhk:N ≤ khε:0 < εhN:ε⁻¹ < ↑NhN':0 < Nhdist:Section_4_3.dist (↑j)⁻¹ (↑k)⁻¹ ≤ (↑N)⁻¹⊢ 0 < ε try All goals completed! 🐙 All goals completed! 🐙
abbrev BoundedBy {n:ℕ} (a: Fin n → ℚ) (M:ℚ) : Prop := ∀ i, |a i| ≤ M

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

lemma boundedBy_def {n:ℕ} (a: Fin n → ℚ) (M:ℚ) : BoundedBy a M ↔ ∀ i, |a i| ≤ M := n:ℕa:Fin n → ℚM:ℚ⊢ BoundedBy a M ↔ ∀ (i : Fin n), |a i| ≤ M All goals completed! 🐙
abbrev Sequence.BoundedBy (a:Sequence) (M:ℚ) : Prop := ∀ n, |a n| ≤ M

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

lemma Sequence.boundedBy_def (a:Sequence) (M:ℚ) : a.BoundedBy M ↔ ∀ n, |a n| ≤ M := a:SequenceM:ℚ⊢ a.BoundedBy M ↔ ∀ (n : ℤ), |a.seq n| ≤ M All goals completed! 🐙
abbrev Sequence.IsBounded (a:Sequence) : Prop := ∃ M ≥ 0, a.BoundedBy M

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

lemma Sequence.isBounded_def (a:Sequence) : a.IsBounded ↔ ∃ M ≥ 0, a.BoundedBy M := a:Sequence⊢ a.IsBounded ↔ ∃ M ≥ 0, a.BoundedBy M All goals completed! 🐙

Приклад 5.1.13

example : BoundedBy ![1,-2,3,-4] 4 := ⊢ BoundedBy ![1, -2, 3, -4] 4 i:Fin (Nat.succ 0).succ.succ.succ⊢ |![1, -2, 3, -4] i| ≤ 4; ⊢ |![1, -2, 3, -4] ((fun i => i) ⟨0, ⋯⟩)| ≤ 4⊢ |![1, -2, 3, -4] ((fun i => i) ⟨1, ⋯⟩)| ≤ 4⊢ |![1, -2, 3, -4] ((fun i => i) ⟨2, ⋯⟩)| ≤ 4⊢ |![1, -2, 3, -4] ((fun i => i) ⟨3, ⋯⟩)| ≤ 4 ⊢ |![1, -2, 3, -4] ((fun i => i) ⟨0, ⋯⟩)| ≤ 4⊢ |![1, -2, 3, -4] ((fun i => i) ⟨1, ⋯⟩)| ≤ 4⊢ |![1, -2, 3, -4] ((fun i => i) ⟨2, ⋯⟩)| ≤ 4⊢ |![1, -2, 3, -4] ((fun i => i) ⟨3, ⋯⟩)| ≤ 4 All goals completed! 🐙

Приклад 5.1.13

declaration uses 'sorry'example : ¬((fun n:ℕ ↦ (-1)^n * (n+1:ℚ)):Sequence).IsBounded := ⊢ ¬(↑fun n => (-1) ^ n * (↑n + 1)).IsBounded All goals completed! 🐙

Приклад 5.1.13

example : ((fun n:ℕ ↦ (-1:ℚ)^n):Sequence).IsBounded := ⊢ (↑fun n => (-1) ^ n).IsBounded refine ⟨ 1, ⊢ 1 ≥ 0 All goals completed! 🐙, ?_ ⟩; i:ℤ⊢ |(↑fun n => (-1) ^ n).seq i| ≤ 1; i:ℤh:0 ≤ i⊢ |(↑fun n => (-1) ^ n).seq i| ≤ 1i:ℤh:¬0 ≤ i⊢ |(↑fun n => (-1) ^ n).seq i| ≤ 1 i:ℤh:0 ≤ i⊢ |(↑fun n => (-1) ^ n).seq i| ≤ 1i:ℤh:¬0 ≤ i⊢ |(↑fun n => (-1) ^ n).seq i| ≤ 1 All goals completed! 🐙

Приклад 5.1.13

example : ¬((fun n:ℕ ↦ (-1:ℚ)^n):Sequence).IsCauchy := ⊢ ¬(↑fun n => (-1) ^ n).IsCauchy ⊢ ¬∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((-1) ^ j) ((-1) ^ k) ≤ ε h:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((-1) ^ j) ((-1) ^ k) ≤ ε⊢ False; specialize h (1/2 : ℚ) (h:∀ ε > 0, ∃ N, ∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((-1) ^ j) ((-1) ^ k) ≤ ε⊢ 1 / 2 > 0 All goals completed! 🐙) N:ℕh:∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((-1) ^ j) ((-1) ^ k) ≤ 1 / 2⊢ False; N:ℕh:∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((-1) ^ j) ((-1) ^ k) ≤ 1 / 2⊢ N ≥ NN:ℕh:∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((-1) ^ j) ((-1) ^ k) ≤ 1 / 2⊢ N + 1 ≥ NN:ℕh:Section_4_3.dist ((-1) ^ N) ((-1) ^ (N + 1)) ≤ 1 / 2⊢ False N:ℕh:∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((-1) ^ j) ((-1) ^ k) ≤ 1 / 2⊢ N ≥ NN:ℕh:∀ j ≥ N, ∀ k ≥ N, Section_4_3.dist ((-1) ^ j) ((-1) ^ k) ≤ 1 / 2⊢ N + 1 ≥ NN:ℕh:Section_4_3.dist ((-1) ^ N) ((-1) ^ (N + 1)) ≤ 1 / 2⊢ False try N:ℕh:Section_4_3.dist ((-1) ^ N) ((-1) ^ (N + 1)) ≤ 1 / 2⊢ False N:ℕh:Section_4_3.dist ((-1) ^ N) ((-1) ^ (N + 1)) ≤ 1 / 2h':Even N⊢ FalseN:ℕh:Section_4_3.dist ((-1) ^ N) ((-1) ^ (N + 1)) ≤ 1 / 2h':¬Even N⊢ False N:ℕh:Section_4_3.dist ((-1) ^ N) ((-1) ^ (N + 1)) ≤ 1 / 2h':Even N⊢ False N:ℕh':Even Nh:|1 + 1| ≤ 2⁻¹⊢ False All goals completed! 🐙 N:ℕh:Section_4_3.dist ((-1) ^ N) ((-1) ^ (N + 1)) ≤ 1 / 2h':¬Even Nh₁:Odd N⊢ False N:ℕh:Section_4_3.dist ((-1) ^ N) ((-1) ^ (N + 1)) ≤ 1 / 2h':¬Even Nh₁:Odd Nh₂:Even (N + 1)⊢ False N:ℕh':¬Even Nh₁:Odd Nh₂:Even (N + 1)h:|-1 - 1| ≤ 2⁻¹⊢ False All goals completed! 🐙

Лема 5.1.14

lemma IsBounded.finite {n:ℕ} (a: Fin n → ℚ) : ∃ M ≥ 0, BoundedBy a M := n:ℕa:Fin n → ℚ⊢ ∃ M ≥ 0, BoundedBy a M -- цей доказ написан так, щоб співпадати із структурою оригінального тексту. a:Fin 0 → ℚ⊢ ∃ M ≥ 0, BoundedBy a Mn:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚ⊢ ∃ M ≥ 0, BoundedBy a M a:Fin 0 → ℚ⊢ ∃ M ≥ 0, BoundedBy a M a:Fin 0 → ℚ⊢ 0 ≥ 0 ∧ BoundedBy a 0; All goals completed! 🐙 n:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin _fvar.572699 → ℚ := fun m => @_fvar.572704 m.castSucc⊢ ∃ M ≥ 0, BoundedBy a M n:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin _fvar.572699 → ℚ := fun m => @_fvar.572704 m.castSuccM:ℚhpos:M ≥ 0hM:BoundedBy a' M⊢ ∃ M ≥ 0, BoundedBy a M have h1 : BoundedBy a' (M + |a (Fin.ofNat _ n)|) := fun m ↦ (hM m).trans (n:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin _fvar.572699 → ℚ := fun m => @_fvar.572704 m.castSuccM:ℚhpos:M ≥ 0hM:BoundedBy a' Mm:Fin n⊢ M ≤ M + |a (Fin.ofNat (n + 1) n)| All goals completed! 🐙) have h2 : |a (Fin.ofNat _ n)| ≤ M + |a (Fin.ofNat _ n)| := n:ℕa:Fin n → ℚ⊢ ∃ M ≥ 0, BoundedBy a M All goals completed! 🐙 refine ⟨ M + |a (Fin.ofNat _ n)|, n:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin _fvar.572699 → ℚ := fun m => @_fvar.572704 m.castSuccM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:Chapter5.BoundedBy _fvar.572972 (_fvar.573031 + |@_fvar.572704 (Fin.ofNat (_fvar.572699 + 1) _fvar.572699)|) := fun m => LE.le.trans (@_fvar.573043 m) (of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => _fvar.573031 ≤ _fvar.573031 + |@_fvar.572704 x|) (Fin.natCast_eq_last _fvar.572699)) (le_mul_iff_one_le_right'._simp_4 _fvar.573031)) (one_le_mabs._simp_4 (@_fvar.572704 (Fin.last _fvar.572699)))))h2:|@_fvar.572704 (Fin.ofNat (_fvar.572699 + 1) _fvar.572699)| ≤ _fvar.573031 + |@_fvar.572704 (Fin.ofNat (_fvar.572699 + 1) _fvar.572699)| := of_eq_true (Eq.trans (Eq.trans (congr (congrArg (fun x => LE.le |@_fvar.572704 x|) (Fin.natCast_eq_last _fvar.572699)) (congrArg (fun x => _fvar.573031 + |@_fvar.572704 x|) (Fin.natCast_eq_last _fvar.572699))) (le_mul_iff_one_le_left'._simp_4 |@_fvar.572704 (Fin.last _fvar.572699)|)) (eq_true _fvar.573039))⊢ M + |a (Fin.ofNat (n + 1) n)| ≥ 0 All goals completed! 🐙, ?_ ⟩ n:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin _fvar.572699 → ℚ := fun m => @_fvar.572704 m.castSuccM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:Chapter5.BoundedBy _fvar.572972 (_fvar.573031 + |@_fvar.572704 (Fin.ofNat ?_mvar.573059 _fvar.572699)|) := fun m => LE.le.trans (@_fvar.573043 m) (@?_mvar.573201 m)h2:|@_fvar.572704 (Fin.ofNat ?_mvar.575355 _fvar.572699)| ≤ _fvar.573031 + |@_fvar.572704 (Fin.ofNat ?_mvar.575438 _fvar.572699)| := ?_mvar.575521m:Fin (n + 1)⊢ |a m| ≤ M + |a (Fin.ofNat (n + 1) n)|; n:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin _fvar.572699 → ℚ := fun m => @_fvar.572704 m.castSuccM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:Chapter5.BoundedBy _fvar.572972 (_fvar.573031 + |@_fvar.572704 (Fin.ofNat ?_mvar.573059 _fvar.572699)|) := fun m => LE.le.trans (@_fvar.573043 m) (@?_mvar.573201 m)h2:|@_fvar.572704 (Fin.ofNat ?_mvar.575355 _fvar.572699)| ≤ _fvar.573031 + |@_fvar.572704 (Fin.ofNat ?_mvar.575438 _fvar.572699)| := ?_mvar.575521j:Fin n⊢ |a j.castSucc| ≤ M + |a (Fin.ofNat (n + 1) n)|n:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin _fvar.572699 → ℚ := fun m => @_fvar.572704 m.castSuccM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:Chapter5.BoundedBy _fvar.572972 (_fvar.573031 + |@_fvar.572704 (Fin.ofNat ?_mvar.573059 _fvar.572699)|) := fun m => LE.le.trans (@_fvar.573043 m) (@?_mvar.573201 m)h2:|@_fvar.572704 (Fin.ofNat ?_mvar.575355 _fvar.572699)| ≤ _fvar.573031 + |@_fvar.572704 (Fin.ofNat ?_mvar.575438 _fvar.572699)| := ?_mvar.575521⊢ |a (Fin.last n)| ≤ M + |a (Fin.ofNat (n + 1) n)| n:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin _fvar.572699 → ℚ := fun m => @_fvar.572704 m.castSuccM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:Chapter5.BoundedBy _fvar.572972 (_fvar.573031 + |@_fvar.572704 (Fin.ofNat ?_mvar.573059 _fvar.572699)|) := fun m => LE.le.trans (@_fvar.573043 m) (@?_mvar.573201 m)h2:|@_fvar.572704 (Fin.ofNat ?_mvar.575355 _fvar.572699)| ≤ _fvar.573031 + |@_fvar.572704 (Fin.ofNat ?_mvar.575438 _fvar.572699)| := ?_mvar.575521j:Fin n⊢ |a j.castSucc| ≤ M + |a (Fin.ofNat (n + 1) n)| All goals completed! 🐙 n:ℕhn:∀ (a : Fin n → ℚ), ∃ M ≥ 0, BoundedBy a Ma:Fin (n + 1) → ℚa':Fin _fvar.572699 → ℚ := fun m => @_fvar.572704 m.castSuccM:ℚhpos:M ≥ 0hM:BoundedBy a' Mh1:Chapter5.BoundedBy _fvar.572972 (_fvar.573031 + |@_fvar.572704 (Fin.ofNat ?_mvar.573059 _fvar.572699)|) := fun m => LE.le.trans (@_fvar.573043 m) (@?_mvar.573201 m)h2:|@_fvar.572704 (Fin.ofNat ?_mvar.575355 _fvar.572699)| ≤ _fvar.573031 + |@_fvar.572704 (Fin.ofNat ?_mvar.575438 _fvar.572699)| := ?_mvar.575521⊢ Fin.last n = Fin.ofNat (n + 1) n; All goals completed! 🐙

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

lemma declaration uses 'sorry'Sequence.isBounded_of_isCauchy {a:Sequence} (h: a.IsCauchy) : a.IsBounded := a:Sequenceh:a.IsCauchy⊢ a.IsBounded All goals completed! 🐙

Вправа 5.1.2

theorem declaration uses 'sorry'Sequence.isBounded_add {a b:ℕ → ℚ} (ha: (a:Sequence).IsBounded) (hb: (b:Sequence).IsBounded): (a + b:Sequence).IsBounded := a:ℕ → ℚb:ℕ → ℚha:(↑a).IsBoundedhb:(↑b).IsBounded⊢ (↑(a + b)).IsBounded All goals completed! 🐙
theorem declaration uses 'sorry'Sequence.isBounded_sub {a b:ℕ → ℚ} (ha: (a:Sequence).IsBounded) (hb: (b:Sequence).IsBounded): (a - b:Sequence).IsBounded := a:ℕ → ℚb:ℕ → ℚha:(↑a).IsBoundedhb:(↑b).IsBounded⊢ (↑(a - b)).IsBounded All goals completed! 🐙theorem declaration uses 'sorry'Sequence.isBounded_mul {a b:ℕ → ℚ} (ha: (a:Sequence).IsBounded) (hb: (b:Sequence).IsBounded): (a * b:Sequence).IsBounded := a:ℕ → ℚb:ℕ → ℚha:(↑a).IsBoundedhb:(↑b).IsBounded⊢ (↑(a * b)).IsBounded All goals completed! 🐙end Chapter5