Analysis I, Section 6.5: Some standard limits

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:

• Some standard limits, including limits of sequences of the form 1/n^α, x^n, and 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