Аналіз I, Глава 7.5

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

Теорема 7.5.1(a) (Root test). A technical condition hbound 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

Теорема 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

Теорема 7.5.1(c) (Root test) / Вправа 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

Теорема 7.5.1 (Root test) / Вправа 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

Лема 7.5.2 / Вправа 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

Наслідок 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

Наслідок 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

Наслідок 7.5.3 (Ratio test) / Вправа 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

Наслідок 7.5.3 (Ratio test) / Вправа 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

Твердження 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)

Вправа 7.5.2