theorem Chapter7.Series.root_test_pos {s : Series} (h : Filter.limsup (fun (n : ℤ) => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTop < 1) : s.absConverges

Theorem 7.5.1(a) (Root test). A technical condition is needed to ensure the limsup is finite.

theorem Chapter7.Series.root_test_neg {s : Series} (h : Filter.limsup (fun (n : ℤ) => ↑(|s.seq n| ^ (1 / ↑n))) Filter.atTop > 1) : s.diverges

Theorem 7.5.1(b) (Root test)

theorem Chapter7.Series.root_test_inconclusive : ∃ (s : Series), Filter.Tendsto (fun (n : ℤ) => |s.seq n| ^ (1 / ↑n)) Filter.atTop (nhds 1) ∧ s.diverges

Theorem 7.5.1(c) (Root test) / Exercise 7.5.3

theorem Chapter7.Series.root_test_inconclusive' : ∃ (s : Series), Filter.Tendsto (fun (n : ℤ) => |s.seq n| ^ (1 / ↑n)) Filter.atTop (nhds 1) ∧ s.absConverges

Theorem 7.5.1 (Root test) / Exercise 7.5.3

theorem Chapter7.Series.ratio_ineq {c : ℤ → ℝ} (m : ℤ) (hpos : ∀ n ≥ m, c n > 0) : Filter.liminf (fun (n : ℤ) => ↑(c (n + 1) / c n)) Filter.atTop ≤ Filter.liminf (fun (n : ℤ) => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧ Filter.liminf (fun (n : ℤ) => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun (n : ℤ) => ↑(c n ^ (1 / ↑n))) Filter.atTop ∧ Filter.limsup (fun (n : ℤ) => ↑(c n ^ (1 / ↑n))) Filter.atTop ≤ Filter.limsup (fun (n : ℤ) => ↑(c (n + 1) / c n)) Filter.atTop

Lemma 7.5.2 / Exercise 7.5.1

theorem Chapter7.Series.ratio_test_pos {s : Series} (hnon : ∀ n ≥ s.m, s.seq n ≠ 0) (h : Filter.limsup (fun (n : ℤ) => ↑(|s.seq (n + 1)| / |s.seq n|)) Filter.atTop < 1) : s.absConverges

Corollary 7.5.3 (Ratio test, convergence).

theorem Chapter7.Series.ratio_test_neg {s : Series} (hnon : ∀ n ≥ s.m, s.seq n ≠ 0) (h : Filter.liminf (fun (n : ℤ) => ↑(|s.seq (n + 1)| / |s.seq n|)) Filter.atTop > 1) : s.diverges

Corollary 7.5.3 (Ratio test, divergence).

theorem Chapter7.Series.ratio_test_inconclusive : ∃ (s : Series), (∀ n ≥ s.m, s.seq n ≠ 0) ∧ Filter.Tendsto (fun (n : ℤ) => |s.seq (n + 1)| / |s.seq n|) Filter.atTop (nhds 1) ∧ s.diverges

Corollary 7.5.3(i) (Ratio test inconclusive, diverges) / Exercise 7.5.3

theorem Chapter7.Series.ratio_test_inconclusive' : ∃ (s : Series), (∀ n ≥ s.m, s.seq n ≠ 0) ∧ Filter.Tendsto (fun (n : ℤ) => |s.seq (n + 1)| / |s.seq n|) Filter.atTop (nhds 1) ∧ s.absConverges

Corollary 7.5.3(ii) (Ratio test inconclusive, absConverges) / Exercise 7.5.3

theorem Chapter7.Series.root_self_converges : Filter.Tendsto (fun (n : ℕ) => ↑n ^ (1 / ↑n)) Filter.atTop (nhds 1)

Proposition 7.5.4

theorem Chapter7.Series.poly_mul_geom_converges {x : ℝ} (hx : |x| < 1) (q : ℝ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => ↑n ^ q * x ^ n) n.toNat else 0, vanish := ⋯ }.converges ∧ Filter.Tendsto (fun (n : ℕ) => ↑n ^ q * x ^ n) Filter.atTop (nhds 0)

Exercise 7.5.2