Analysis I, Section 7.3: Sums of non-negative numbers

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:

• Equivalent characterizations of convergence of nonnegative series.
• Cauchy condensation test.

@[reducible, inline]

abbrev Chapter7.Series.nonneg (s : Series) : Prop

Equations

• s.nonneg = ∀ (n : ℤ), s.seq n ≥ 0

@[reducible, inline]

abbrev Chapter7.Series.partial_of_nonneg {s : Series} (h : s.nonneg) : Monotone s.partial

Equations

• ⋯ = ⋯

theorem Chapter7.Series.converges_of_nonneg_iff {s : Series} (h : s.nonneg) : s.converges ↔ ∃ (M : ℝ), ∀ (N : ℤ), s.partial N ≤ M

Proposition 7.3.1

theorem Chapter7.Series.sum_of_nonneg_lt {s : Series} (h : s.nonneg) {M : ℝ} (hM : ∀ (N : ℤ), s.partial N ≤ M) : s.sum ≤ M

theorem Chapter7.Series.partial_le_sum_of_nonneg {s : Series} (hnon : s.nonneg) (hconv : s.converges) (N : ℤ) : s.partial N ≤ s.sum

theorem Chapter7.Series.partial_nonneg {s : Series} (hnon : s.nonneg) (N : ℤ) : 0 ≤ s.partial N

Some useful nonnegativity lemmas for later applications.

theorem Chapter7.Series.sum_of_nonneg {s : Series} (hnon : s.nonneg) : 0 ≤ s.sum

theorem Chapter7.Series.converges_of_le {s t : Series} (hm : s.m = t.m) (hcomp : ∀ n ≥ s.m, |s.seq n| ≤ t.seq n) (hconv : t.converges) : s.absConverges ∧ |s.sum| ≤ s.abs.sum ∧ s.abs.sum ≤ t.sum

Corollary 7.3.2 (Comparison test) / Exercise 7.3.1

theorem Chapter7.Series.diverges_of_ge {s t : Series} (hm : s.m = t.m) (hcomp : ∀ n ≥ s.m, |s.seq n| ≤ t.seq n) (hdiv : ¬s.absConverges) : t.diverges

theorem Chapter7.Series.converges_geom {x : ℝ} (hx : |x| < 1) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => x ^ n) n.toNat else 0, vanish := ⋯ }.convergesTo (1 / (1 - x))

Lemma 7.3.3 (Geometric series) / Exercise 7.3.2

theorem Chapter7.Series.absConverges_geom {x : ℝ} (hx : |x| < 1) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => x ^ n) n.toNat else 0, vanish := ⋯ }.absConverges

theorem Chapter7.Series.diverges_geom {x : ℝ} (hx : |x| ≥ 1) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => x ^ n) n.toNat else 0, vanish := ⋯ }.diverges

theorem Chapter7.Series.converges_geom_iff (x : ℝ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => x ^ n) n.toNat else 0, vanish := ⋯ }.converges ↔ |x| < 1

theorem Chapter7.Series.cauchy_criterion {s : Series} (hm : s.m = 1) (hs : s.nonneg) (hmono : ∀ n ≥ 1, s.seq (n + 1) ≤ s.seq n) : s.converges ↔ { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (k : ℕ) => 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := ⋯ }.converges

Proposition 7.3.4 (Cauchy criterion)

theorem Chapter7.Series.converges_qseries (q : ℝ) (hq : q > 0) : (mk' fun (n : { n : ℤ // n ≥ 1 }) => 1 / ↑↑n ^ q).converges ↔ q > 1

Corollary 7.3.7

theorem Chapter7.Series.zeta_eq {q : ℝ} (hq : q > 1) : ↑(mk' fun (n : { n : ℤ // n ≥ 1 }) => 1 / ↑↑n ^ q).sum = riemannZeta ↑q

Remark 7.3.8

theorem Chapter7.Series.Basel_problem : (mk' fun (n : { n : ℤ // n ≥ 1 }) => 1 / ↑↑n ^ 2).sum = Real.pi ^ 2 / 6

theorem Chapter7.Series.nonneg_sum_zero {a : ℕ → ℝ} (ha : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.nonneg) (hconv : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.converges) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.sum = 0 ↔ ∀ (n : ℕ), a n = 0

Exercise 7.3.3