Аналіз I, Розділ 7.4: Перестановка рядів

Я (прим. перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним підходом Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підправити", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні конструкції та результати цього розділу:

• Перестановка невід'ємних або абсолютно збіжних рядів.

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

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

Приклад 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

Твердження 7.4.3 (Перестановка рядів)

@[reducible, inline]

noncomputable abbrev Chapter7.Series.a_7_4_4 : ℕ → ℝ

Приклад 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

Вправа 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

Вправа 7.4.2 : Доведіть знову Твердження 7.4.3, використовуючи Твердження 7.41, Твердження 7.2.14 та подаючи a n як різницю між a n + |a n| і |a n|.