Analysis I, Section 7.5: The root and ratio tests

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:

• The root and ratio tests/

A point that is only implicitly stated in the text is that for the root and ratio tests, the lim inf and lim sup should be interpreted within the extended reals. The Lean formalizations below make this point more explicit.

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)

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)

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 (Ratio test) / 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 (Ratio test) / Exercise 7.5.3

theorem Chapter7.Series.root_self_converges : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => ↑n ^ (1 / ↑n)) n.toNat else 0, vanish := ⋯ }.convergesTo 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