Аналіз I, Розділ 8.2: Підсумовування на нескінченних множинах

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

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

• Абсолютна збіжність та підсумовування на зліченних нескінченних або загальних множинах.
• Зв'язки з Mathlib-овськими Summable та tsum.
• Теорема Рімана про перетворення рядів.

Надано деякі нетривіальні API, що доповнюють матеріал підручника і пов'язують ці поняття з існуючими поняттями підсумовування.

Після цього розділу позначення для підсумовування, розроблене тут, буде застаріле на користь API Mathlib для Summable і tsum.

@[reducible, inline]

abbrev Chapter8.AbsConvergent {X : Type} (f : X → ℝ) : Prop

Визначення 8.2.1 (Ряди на лічильних множинах). Зверніть увагу, що з цією дефініцією функції, визначені на скінчених множинах, не будуть абсолютно збіжними; для таких випадків слід використовувати випадки AbsConvergent'.

Equations

• Chapter8.AbsConvergent f = ∃ (g : ℕ → X), Function.Bijective g ∧ { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (f ∘ g) n.toNat else 0, vanish := ⋯ }.absConverges

theorem Chapter8.AbsConvergent.mk {X : Type} {f : X → ℝ} {g : ℕ → X} (h : Function.Bijective g) (hfg : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (f ∘ g) n.toNat else 0, vanish := ⋯ }.absConverges) : AbsConvergent f

@[reducible, inline]

noncomputable abbrev Chapter8.Sum {X : Type} (f : X → ℝ) : ℝ

Дефініція була обрана таким чином, щоб давати змістовне значення, коли X скінченна, навіть якщо AbsConvergent за визначенням є хибним у цьому контексті.

Equations

• One or more equations did not get rendered due to their size.

theorem Chapter8.Sum.of_finite {X : Type} [hX : Finite X] (f : X → ℝ) : Sum f = ∑ x : X, f x

theorem Chapter8.AbsConvergent.comp {X : Type} {f : X → ℝ} {g : ℕ → X} (h : Function.Bijective g) (hf : AbsConvergent f) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (f ∘ g) n.toNat else 0, vanish := ⋯ }.absConverges

theorem Chapter8.Sum.eq {X : Type} {f : X → ℝ} {g : ℕ → X} (h : Function.Bijective g) (hfg : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (f ∘ g) n.toNat else 0, vanish := ⋯ }.absConverges) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (f ∘ g) n.toNat else 0, vanish := ⋯ }.convergesTo (Sum f)

theorem Chapter8.Sum.of_comp {X Y : Type} {f : X → ℝ} (h : AbsConvergent f) {g : Y → X} (hbij : Function.Bijective g) : AbsConvergent (f ∘ g) ∧ Sum f = Sum (f ∘ g)

@[simp]

theorem Chapter8.Finset.Icc_eq_cast (N : ℕ) : Finset.Icc 0 ↑N = Finset.map Nat.castEmbedding (Finset.Icc 0 N)

theorem Chapter8.Finset.Icc_empty {N : ℤ} (h : ¬N ≥ 0) : Finset.Icc 0 N = ∅

theorem Chapter8.sum_of_sum_of_AbsConvergent_nonneg {f : ℕ × ℕ → ℝ} (hf : AbsConvergent f) (hpos : ∀ (n m : ℕ), 0 ≤ f (n, m)) : (∀ (n : ℕ), { m := 0, seq := fun (n_1 : ℤ) => if n_1 ≥ 0 then (fun (m : ℕ) => f (n, m)) n_1.toNat else 0, vanish := ⋯ }.converges) ∧ { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => { m := 0, seq := fun (n_1 : ℤ) => if n_1 ≥ 0 then (fun (m : ℕ) => f (n, m)) n_1.toNat else 0, vanish := ⋯ }.sum) n.toNat else 0, vanish := ⋯ }.convergesTo (Sum f)

Теорема 8.2.2, попередня версія. Аргументи тут трохи переставлені порівняно з текстом.

theorem Chapter8.sum_of_sum_of_AbsConvergent {f : ℕ × ℕ → ℝ} (hf : AbsConvergent f) : (∀ (n : ℕ), { m := 0, seq := fun (n_1 : ℤ) => if n_1 ≥ 0 then (fun (m : ℕ) => f (n, m)) n_1.toNat else 0, vanish := ⋯ }.absConverges) ∧ { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => { m := 0, seq := fun (n_1 : ℤ) => if n_1 ≥ 0 then (fun (m : ℕ) => f (n, m)) n_1.toNat else 0, vanish := ⋯ }.sum) n.toNat else 0, vanish := ⋯ }.convergesTo (Sum f)

Теорема 8.2.2, друга версія

theorem Chapter8.sum_of_sum_of_AbsConvergent' {f : ℕ × ℕ → ℝ} (hf : AbsConvergent f) : (∀ (m : ℕ), { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => f (n, m)) n.toNat else 0, vanish := ⋯ }.absConverges) ∧ { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (m : ℕ) => { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => f (n, m)) n.toNat else 0, vanish := ⋯ }.sum) n.toNat else 0, vanish := ⋯ }.convergesTo (Sum f)

Теорема 8.2.2, третя версія

theorem Chapter8.sum_comm {f : ℕ × ℕ → ℝ} (hf : AbsConvergent f) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => { m := 0, seq := fun (n_1 : ℤ) => if n_1 ≥ 0 then (fun (m : ℕ) => f (n, m)) n_1.toNat else 0, vanish := ⋯ }.sum) n.toNat else 0, vanish := ⋯ }.sum = { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (m : ℕ) => { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => f (n, m)) n.toNat else 0, vanish := ⋯ }.sum) n.toNat else 0, vanish := ⋯ }.sum

Теорема 8.2.2, четверта версія

theorem Chapter8.AbsConvergent.iff {X : Type} (hX : CountablyInfinite X) (f : X → ℝ) : AbsConvergent f ↔ BddAbove ((fun (A : Finset X) => ∑ x ∈ A, |f x|) '' Set.univ)

Лема 8.2.3 / Вправа 8.2.1

@[reducible, inline]

abbrev Chapter8.AbsConvergent' {X : Type} (f : X → ℝ) : Prop

Equations

• Chapter8.AbsConvergent' f = BddAbove ((fun (A : Finset X) => ∑ x ∈ A, |f x|) '' Set.univ)

theorem Chapter8.AbsConvergent'.of_finite {X : Type} [Finite X] (f : X → ℝ) : AbsConvergent' f

theorem Chapter8.AbsConvergent'.of_countable {X : Type} (hX : CountablyInfinite X) {f : X → ℝ} : AbsConvergent' f ↔ AbsConvergent f

Не в підручнику, але мала б бути включена.

theorem Chapter8.AbsConvergent'.countable_supp {X : Type} {f : X → ℝ} (hf : AbsConvergent' f) : AtMostCountable ↑{x : X | f x ≠ 0}

Лема 8.2.5 / Вправа 8.2.2

theorem Chapter8.AbsConvergent'.subtype {X : Type} {f : X → ℝ} (hf : AbsConvergent' f) (A : Set X) : AbsConvergent' fun (x : ↑A) => f ↑x

Порівняйте із Mathlib-овським Summable.subtype

@[reducible, inline]

noncomputable abbrev Chapter8.Sum' {X : Type} (f : X → ℝ) : ℝ

Узагальнена сума. Зверніть увагу, що це дасть некоректні значення, якщо f не є AbsConvergent'.

Equations

• Chapter8.Sum' f = Chapter8.Sum fun (x : ↑{x : X | f x ≠ 0}) => f ↑x

theorem Chapter8.Sum'.of_finsupp {X : Type} {f : X → ℝ} {A : Finset X} (h : ∀ x ∉ A, f x = 0) : Sum' f = ∑ x ∈ A, f x

Не в підручнику, але мала б бути включена (закони рядів значно важче встановити без цього).

theorem Chapter8.Sum'.of_countable_supp {X : Type} {f : X → ℝ} {A : Set X} (hA : CountablyInfinite ↑A) (hfA : ∀ x ∉ A, f x = 0) (hconv : AbsConvergent' f) : (AbsConvergent' fun (x : ↑A) => f ↑x) ∧ Sum' f = Sum fun (x : ↑A) => f ↑x

Не в підручнику, але мала б бути включена (закони рядів значно важче встановити без цього).

theorem Chapter8.AbsConvergent'.iff_Summable {X : Type} (f : X → ℝ) : AbsConvergent' f ↔ Summable f

Зв'язок з властивістю Summable Mathlib. Можлива якась версія доказу може бути підходящою для Mathlib?

theorem Chapter8.Filter.Eventually.int_natCast_atTop (p : ℤ → Prop) : (∀ᶠ (n : ℤ) in Filter.atTop, p n) ↔ ∀ᶠ (n : ℕ) in Filter.atTop, p ↑n

Можливо, підходить для перенесення в Mathlib?

theorem Chapter8.Filter.Tendsto.int_natCast_atTop {R : Type} (f : ℤ → R) (l : Filter R) : Filter.Tendsto f Filter.atTop l ↔ Filter.Tendsto (f ∘ Nat.cast) Filter.atTop l

theorem Chapter8.Sum'.eq_tsum {X : Type} (f : X → ℝ) (h : AbsConvergent' f) : Sum' f = ∑' (x : X), f x

Зв'язок з операцією tsum (або Σ') Mathlib.

theorem Chapter8.Sum'.add {X : Type} {f g : X → ℝ} (hf : AbsConvergent' f) (hg : AbsConvergent' g) : AbsConvergent' (f + g) ∧ Sum' (f + g) = Sum' f + Sum' g

Твердження 8.2.6 (a) (Закони для абсолютно збіжних рядів) / Вправа 8.2.3

theorem Chapter8.Sum'.smul {X : Type} {f : X → ℝ} (hf : AbsConvergent' f) (c : ℝ) : AbsConvergent' (c • f) ∧ Sum' (c • f) = c * Sum' f

Твердження 8.2.6 (b) (Закони для абсолютно збіжних рядів) / Вправа 8.2.3

theorem Chapter8.Sum'.sub {X : Type} {f g : X → ℝ} (hf : AbsConvergent' f) (hg : AbsConvergent' g) : AbsConvergent' (f - g) ∧ Sum' (f - g) = Sum' f - Sum' g

Цей закон не вказаний явно в Твердженні 8.2.6, але легко випливає з частин (a) та (b).

theorem Chapter8.Sum'.of_disjoint_union {X : Type} {f : X → ℝ} (hf : AbsConvergent' f) {X₁ X₂ : Set X} (hdisj : Disjoint X₁ X₂) : (Sum' fun (x : ↑(X₁ ∪ X₂)) => f ↑x) = (Sum' fun (x : ↑X₁) => f ↑x) + Sum' fun (x : ↑X₂) => f ↑x

Твердження 8.2.6 (c) (Закони для абсолютно збіжних рядів) / Вправа 8.2.3. Перша частина цього твердження була переміщена до AbsConvergent'.subtype.

theorem Chapter8.Sum'.of_univ {X : Type} {f : X → ℝ} (hf : AbsConvergent' f) : (Sum' fun (x : ↑Set.univ) => f ↑x) = Sum' f

Це технічне твердження, аналог tsum_univ, необхідне через те, як Mathlib обробляє множини.

theorem Chapter8.Sum'.of_comp {X Y : Type} {f : X → ℝ} (hf : AbsConvergent' f) {φ : Y → X} (hφ : Function.Bijective φ) : AbsConvergent' (f ∘ φ) ∧ Sum' f = Sum' (f ∘ φ)

theorem Chapter8.divergent_parts_of_divergent {a : ℕ → ℝ} (ha : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.converges) (ha' : ¬{ m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.absConverges) : (¬AbsConvergent fun (n : ↑{n : ℕ | a n ≥ 0}) => a ↑n) ∧ ¬AbsConvergent fun (n : ↑{n : ℕ | a n < 0}) => a ↑n

Лема 8.2.7 / Вправа 8.2.4

theorem Chapter8.permute_convergesTo_of_divergent {a : ℕ → ℝ} (ha : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.converges) (ha' : ¬{ m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.absConverges) (L : ℝ) : ∃ (f : ℕ → ℕ), Function.Bijective f ∧ { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (a ∘ f) n.toNat else 0, vanish := ⋯ }.convergesTo L

Теорема 8.2.8 (Теорема Рімана про перестановку) / Вправа 8.2.5

theorem Chapter8.permute_diverges_of_divergent {a : ℕ → ℝ} (ha : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.converges) (ha' : ¬{ m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.absConverges) : ∃ (f : ℕ → ℕ), Function.Bijective f ∧ Filter.Tendsto (fun (N : ℤ) => ↑({ m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (a ∘ f) n.toNat else 0, vanish := ⋯ }.partial N)) Filter.atTop (nhds ⊤)

Вправа 8.2.6

theorem Chapter8.permute_diverges_of_divergent' {a : ℕ → ℝ} (ha : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.converges) (ha' : ¬{ m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.absConverges) : ∃ (f : ℕ → ℕ), Function.Bijective f ∧ Filter.Tendsto (fun (N : ℤ) => ↑({ m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (a ∘ f) n.toNat else 0, vanish := ⋯ }.partial N)) Filter.atTop (nhds ⊥)