Аналіз I, Розділ 6.5: Деякі стандартні границі

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

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

• Деякі стандартні границі, включно з границями послідовностей виду 1/n^α, x^n та x^(1/n).

namespace Chapter6theorem declaration uses 'sorry'Sequence.lim_of_const (c:ℝ) : ((fun (_:ℕ) ↦ c):Sequence).TendsTo c := byc:ℝ⊢ (↑fun x => c).TendsTo c sorryAll goals completed! 🐙instance Sequence.inst_pow: Pow Sequence ℕ where pow a k := { m := a.m seq n := if n ≥ a.m then a n ^ k else 0 vanish := bya:Sequencek:ℕ⊢ ∀ n < a.m, (if n ≥ a.m then a.seq n ^ k else 0) = 0 grindAll goals completed! 🐙 }@[simp] lemma Sequence.pow_eval {a:Sequence} {k: ℕ} {n: ℤ} (hn : n ≥ a.m): (a ^ k) n = a n ^ k := bya:Sequencek:ℕn:ℤhn:n ≥ a.m⊢ (a ^ k).seq n = a.seq n ^ k rw [HPow.hPow, instHPow, Pow.pow, inst_pow]a:Sequencek:ℕn:ℤhn:n ≥ a.m⊢ ({ hPow := fun a b => { pow := fun a k => { m := a.m, seq := fun n => if n ≥ a.m then a.seq n ^ k else 0, vanish := ⋯ } }.1 a b }.1 a k).seq n = a.seq n ^ k grindAll goals completed! 🐙@[simp] lemma Sequence.pow_one (a:Sequence) : a^1 = a := bya:Sequence⊢ a ^ 1 = a ext nma:Sequence⊢ (a ^ 1).m = a.mseq.ha:Sequencen:ℤ⊢ (a ^ 1).seq n = a.seq n; rflseq.ha:Sequencen:ℤ⊢ (a ^ 1).seq n = a.seq n; simp only [HPow.hPow, Pow.pow]seq.ha:Sequencen:ℤ⊢ (if n ≥ a.m then Monoid.npow 1 (a.seq n) else 0) = a.seq n; split_ifs with hpos._@._hyg.208a:Sequencen:ℤh:n ≥ a.m⊢ Monoid.npow 1 (a.seq n) = a.seq nneg._@._hyg.208a:Sequencen:ℤh:¬n ≥ a.m⊢ 0 = a.seq n; simpneg._@._hyg.208a:Sequencen:ℤh:¬n ≥ a.m⊢ 0 = a.seq n; simp [a.vanish n (by grind)]All goals completed! 🐙lemma Sequence.pow_succ (a:Sequence) (k:ℕ): a^(k+1) = a^k * a := bya:Sequencek:ℕ⊢ a ^ (k + 1) = a ^ k * a ext xma:Sequencek:ℕ⊢ (a ^ (k + 1)).m = (a ^ k * a).mseq.ha:Sequencek:ℕx:ℤ⊢ (a ^ (k + 1)).seq x = (a ^ k * a).seq x .ma:Sequencek:ℕ⊢ (a ^ (k + 1)).m = (a ^ k * a).m symmma:Sequencek:ℕ⊢ (a ^ k * a).m = (a ^ (k + 1)).m; exact Int.min_self a.mAll goals completed! 🐙 .seq.ha:Sequencek:ℕx:ℤ⊢ (a ^ (k + 1)).seq x = (a ^ k * a).seq x simp only [mul_eval]seq.ha:Sequencek:ℕx:ℤ⊢ (a ^ (k + 1)).seq x = (a ^ k).seq x * a.seq x by_cases h: x ≥ a.mpos._@._hyg.292a:Sequencek:ℕx:ℤh:x ≥ a.m⊢ (a ^ (k + 1)).seq x = (a ^ k).seq x * a.seq xneg._@._hyg.292a:Sequencek:ℕx:ℤh:¬x ≥ a.m⊢ (a ^ (k + 1)).seq x = (a ^ k).seq x * a.seq x ·pos._@._hyg.292a:Sequencek:ℕx:ℤh:x ≥ a.m⊢ (a ^ (k + 1)).seq x = (a ^ k).seq x * a.seq x simp [pow_eval h]pos._@._hyg.292a:Sequencek:ℕx:ℤh:x ≥ a.m⊢ a.seq x ^ (k + 1) = a.seq x ^ k * a.seq x rflAll goals completed! 🐙 ·neg._@._hyg.292a:Sequencek:ℕx:ℤh:¬x ≥ a.m⊢ (a ^ (k + 1)).seq x = (a ^ k).seq x * a.seq x rw [a.vanish x (by grind), mul_zero]neg._@._hyg.292a:Sequencek:ℕx:ℤh:¬x ≥ a.m⊢ (a ^ (k + 1)).seq x = 0 exact vanish _ _ (bya:Sequencek:ℕx:ℤh:¬x ≥ a.m⊢ x < (a ^ (k + 1)).m simp at ha:Sequencek:ℕx:ℤh:x < a.m⊢ x < (a ^ (k + 1)).m; exact hAll goals completed! 🐙) end Chapter6