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

@[implicit_reducible]

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 (ratio of absolute value less than one) / Exercise 6.5.2

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

Lemma 6.5.2 (ratio one) / 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 (ratio minus one or of absolute value greater than one) / 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 (i)

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

Exercise 6.5.1 (ii)