Analysis I, Section 7.4: Rearrangement of series

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:

• Rearrangement of non-negative or absolutely convergent series.

theorem Chapter7.Series.sum_eq_sum (b : ℕ → ℝ) {N : ℤ} (hN : N ≥ 0) : (∑ n ∈ Finset.Icc 0 N, if 0 ≤ n then b n.toNat else 0) = ∑ n ∈ Finset.Iic N.toNat, b n

theorem Chapter7.Series.converges_of_permute_nonneg {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) {f : ℕ → ℕ} (hf : Function.Bijective f) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => a (f n)) n.toNat else 0, vanish := ⋯ }.converges ∧ { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.sum = { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => a (f n)) n.toNat else 0, vanish := ⋯ }.sum

Proposition 7.4.1

theorem Chapter7.Series.zeta_2_converges : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => 1 / (↑n + 1) ^ 2) n.toNat else 0, vanish := ⋯ }.converges

Example 7.4.2

theorem Chapter7.Series.permuted_zeta_2_converges : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => if Even n then 1 / (↑n + 2) ^ 2 else 1 / ↑n ^ 2) n.toNat else 0, vanish := ⋯ }.converges

theorem Chapter7.Series.permuted_zeta_2_eq_zeta_2 : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => if Even n then 1 / (↑n + 2) ^ 2 else 1 / ↑n ^ 2) n.toNat else 0, vanish := ⋯ }.sum = { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => 1 / (↑n + 1) ^ 2) n.toNat else 0, vanish := ⋯ }.sum

theorem Chapter7.Series.absConverges_of_permute {a : ℕ → ℝ} (ha : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.absConverges) {f : ℕ → ℕ} (hf : Function.Bijective f) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => a (f n)) n.toNat else 0, vanish := ⋯ }.absConverges ∧ { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.sum = { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => a (f n)) n.toNat else 0, vanish := ⋯ }.sum

Proposition 7.4.3 (Rearrangement of series)

@[reducible, inline]

noncomputable abbrev Chapter7.Series.a_7_4_4 : ℕ → ℝ

Example 7.4.4

Equations

• Chapter7.Series.a_7_4_4 n = (-1) ^ n / (↑n + 2)

theorem Chapter7.Series.ex_7_4_4_conv : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a_7_4_4 n.toNat else 0, vanish := ⋯ }.converges

theorem Chapter7.Series.ex_7_4_4_sum : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a_7_4_4 n.toNat else 0, vanish := ⋯ }.sum > 0

@[reducible, inline]

abbrev Chapter7.Series.f_7_4_4 : ℕ → ℕ

Equations

• Chapter7.Series.f_7_4_4 n = if n % 3 = 0 then 2 * (n / 3) else 2 * n - n / 3 - 1

theorem Chapter7.Series.f_7_4_4_bij : Function.Bijective f_7_4_4

theorem Chapter7.Series.ex_7_4_4'_conv : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => a_7_4_4 (f_7_4_4 n)) n.toNat else 0, vanish := ⋯ }.converges

theorem Chapter7.Series.ex_7_4_4'_sum : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => a_7_4_4 (f_7_4_4 n)) n.toNat else 0, vanish := ⋯ }.sum < 0

theorem Chapter7.Series.absConverges_of_subseries {a : ℕ → ℝ} (ha : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.absConverges) {f : ℕ → ℕ} (hf : StrictMono f) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => a (f n)) n.toNat else 0, vanish := ⋯ }.absConverges

Exercise 7.4.1

theorem Chapter7.Series.absConverges_of_permute' {a : ℕ → ℝ} (ha : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.absConverges) {f : ℕ → ℕ} (hf : Function.Bijective f) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => a (f n)) n.toNat else 0, vanish := ⋯ }.absConverges ∧ { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.sum = { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => a (f n)) n.toNat else 0, vanish := ⋯ }.sum

Exercise 7.4.2 : reprove Proposition 7.4.3 using Proposition 7.41, Proposition 7.2.14, and expressing a n as the difference of a n + |a n| and |a n|.