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).

theorem Chapter6.Sequence.lim_of_const (c : ℝ) : (↑fun (x : ℕ) => c).TendsTo c

instance Chapter6.Sequence.inst_pow : Pow Sequence ℕ

Equations

• Chapter6.Sequence.inst_pow = { pow := fun (a : Chapter6.Sequence) (k : ℕ) => { m := a.m, seq := fun (n : ℤ) => if n ≥ a.m then a.seq n ^ k else 0, vanish := ⋯ } }

@[simp]

theorem Chapter6.Sequence.pow_eval {a : Sequence} {k : ℕ} {n : ℤ} (hn : n ≥ a.m) : (a ^ k).seq n = a.seq n ^ k

@[simp]

theorem Chapter6.Sequence.pow_one (a : Sequence) : a ^ 1 = a

theorem Chapter6.Sequence.pow_succ (a : Sequence) (k : ℕ) : a ^ (k + 1) = a ^ k * a

theorem Chapter6.Sequence.lim_of_power_decay {k : ℕ} : (↑fun (n : ℕ) => 1 / (↑n + 1) ^ (1 / (↑k + 1))).TendsTo 0

Corollary 6.5.1

theorem Chapter6.Sequence.lim_of_geometric {x : ℝ} (hx : |x| < 1) : (↑fun (n : ℕ) => x ^ n).TendsTo 0

Lemma 6.5.2 / Exercise 6.5.2

theorem Chapter6.Sequence.lim_of_geometric' {x : ℝ} (hx : x = 1) : (↑fun (n : ℕ) => x ^ n).TendsTo 1

Lemma 6.5.2 / Exercise 6.5.2

theorem Chapter6.Sequence.lim_of_geometric'' {x : ℝ} (hx : x = -1 ∨ |x| > 1) : (↑fun (n : ℕ) => x ^ n).Divergent

Lemma 6.5.2 / Exercise 6.5.2

theorem Chapter6.Sequence.lim_of_roots {x : ℝ} (hx : x > 0) : (↑fun (n : ℕ) => x ^ (1 / (↑n + 1))).TendsTo 1

Lemma 6.5.3 / Exercise 6.5.3

theorem Chapter6.Sequence.lim_of_rat_power_decay {q : ℚ} (hq : q > 0) : (↑fun (n : ℕ) => 1 / (↑n + 1) ^ ↑q).TendsTo 0

Exercise 6.5.1

theorem Chapter6.Sequence.lim_of_rat_power_growth {q : ℚ} (hq : q > 0) : (↑fun (n : ℕ) => (↑n + 1) ^ ↑q).Divergent

Exercise 6.5.1