Аналіз I, Розділ 7.1: Скінченні ряди

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

Технічна примітка: у Lean зручно поширювати скінченні послідовності (зазвичай доповнюючи нулями) до функцій на всіх цілих числах.

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

• API для підсумовування по скінченних множинах (представлених типом Finset з Mathlib), з використанням методу Finset.sum і нотації ∑ n ∈ A, f n.
• Теорема Фубіні для скінченних сум

Ми не намагаємося відтворити повний API Finset.sum тут, але в наступних розділах широко користуватимемося цим API.

theorem Finset.sum_of_empty {n m : ℤ} (h : n < m) (a : ℤ → ℝ) : ∑ i ∈ Icc m n, a i = 0

Визначення 7.1.1

theorem Finset.sum_of_nonempty {n m : ℤ} (h : n ≥ m - 1) (a : ℤ → ℝ) : ∑ i ∈ Icc m (n + 1), a i = ∑ i ∈ Icc m n, a i + a (n + 1)

Визначення 7.1.1. Це схоже на Mathlib's Finset.sum_Icc_succ_top, тільки там сума береться по натуральних числах, а не по цілих.

theorem Finset.concat_finite_series {m n p : ℤ} (hmn : m ≤ n + 1) (hpn : n ≤ p) (a : ℤ → ℝ) : ∑ i ∈ Icc m n, a i + ∑ i ∈ Icc (n + 1) p, a i = ∑ i ∈ Icc m p, a i

Лема 7.1.4(a) / Вправа 7.1.1

theorem Finset.shift_finite_series {m n k : ℤ} (a : ℤ → ℝ) : ∑ i ∈ Icc m n, a i = ∑ i ∈ Icc (m + k) (n + k), a (i - k)

Лема 7.1.4(b) / Вправа 7.1.1

theorem Finset.finite_series_add {m n : ℤ} (a b : ℤ → ℝ) : ∑ i ∈ Icc m n, (a i + b i) = ∑ i ∈ Icc m n, a i + ∑ i ∈ Icc m n, b i

Лема 7.1.4(c) / Вправа 7.1.1

theorem Finset.finite_series_const_mul {m n : ℤ} (a : ℤ → ℝ) (c : ℝ) : ∑ i ∈ Icc m n, c * a i = c * ∑ i ∈ Icc m n, a i

Лема 7.1.4(d) / Вправа 7.1.1

theorem Finset.abs_finite_series_le {m n : ℤ} (a : ℤ → ℝ) (c : ℝ) : |∑ i ∈ Icc m n, a i| ≤ ∑ i ∈ Icc m n, |a i|

Лема 7.1.4(e) / Вправа 7.1.1

theorem Finset.finite_series_of_le {m n : ℤ} {a b : ℤ → ℝ} (h : ∀ (i : ℤ), m ≤ i → i ≤ n → a i ≤ b i) : ∑ i ∈ Icc m n, a i ≤ ∑ i ∈ Icc m n, b i

Лема 7.1.4(f) / Вправа 7.1.1

theorem Finset.finite_series_of_rearrange {n : ℕ} {X' : Type u_1} (X : Finset X') (hcard : X.card = n) (f : X' → ℝ) (g h : { x : ℤ // x ∈ Icc 1 ↑n } → { x : X' // x ∈ X }) (hg : Function.Bijective g) (hh : Function.Bijective h) : (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0

Твердження 7.1.8.

theorem Finset.exist_bijection {n : ℕ} {Y : Type u_1} (X : Finset Y) (hcard : X.card = n) : ∃ (g : { x : ℤ // x ∈ Icc 1 ↑n } → { x : Y // x ∈ X }), Function.Bijective g

Цей факт гарантує, що Визначення 7.1.6 буде коректним навіть без звертання до існуючого методу Finset.sum.

theorem Finset.finite_series_eq {n : ℕ} {Y : Type u_1} (X : Finset Y) (f : Y → ℝ) (g : { x : ℤ // x ∈ Icc 1 ↑n } → { x : Y // x ∈ X }) (hg : Function.Bijective g) : ∑ i ∈ X, f i = ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0

Визначення 7.1.6

theorem Finset.finite_series_of_empty {X' : Type u_1} (f : X' → ℝ) : ∑ i ∈ ∅, f i = 0

Твердження 7.1.11(a) / Вправа 7.1.2

theorem Finset.finite_series_of_singleton {X' : Type u_1} (f : X' → ℝ) (x₀ : X') : ∑ i ∈ {x₀}, f i = f x₀

Твердження 7.1.11(b) / Вправа 7.1.2

theorem Finset.finite_series_of_fintype {X' : Type u_1} (f : X' → ℝ) (X : Finset X') : ∑ x ∈ X, f x = ∑ x : { x : X' // x ∈ X }, f ↑x

Технічна лема, що пов'язує суму по finset із сумою по fintype. Добре поєднується з інструментами такими як map_finite_series нижче.

theorem Finset.map_finite_series {Y : Type u_2} {X : Type u_1} [Fintype X] [Fintype Y] (f : X → ℝ) {g : Y → X} (hg : Function.Bijective g) : ∑ x : X, f x = ∑ y : Y, f (g y)

Твердження 7.1.11(c) / Вправа 7.1.2

theorem Finset.finite_series_of_disjoint_union {Z : Type u_1} {X Y : Finset Z} (hdisj : Disjoint X Y) (f : Z → ℝ) : ∑ z ∈ X ∪ Y, f z = ∑ z ∈ X, f z + ∑ z ∈ Y, f z

Твердження 7.1.11(e) / Вправа 7.1.2

theorem Finset.finite_series_of_add {X' : Type u_1} (f g : X' → ℝ) (X : Finset X') : ∑ x ∈ X, (f + g) x = ∑ x ∈ X, f x + ∑ x ∈ X, g x

Твердження 7.1.11(f) / Вправа 7.1.2

theorem Finset.finite_series_of_const_mul {X' : Type u_1} (f : X' → ℝ) (X : Finset X') (c : ℝ) : ∑ x ∈ X, c * f x = c * ∑ x ∈ X, f x

Твердження 7.1.11(g) / Вправа 7.1.2

theorem Finset.finite_series_of_le' {X' : Type u_1} (f g : X' → ℝ) (X : Finset X') (h : ∀ x ∈ X, f x ≤ g x) : ∑ x ∈ X, f x ≤ ∑ x ∈ X, g x

Твердження 7.1.11(h) / Вправа 7.1.2

theorem Finset.abs_finite_series_le' {X' : Type u_1} (f : X' → ℝ) (X : Finset X') : |∑ x ∈ X, f x| ≤ ∑ x ∈ X, |f x|

Твердження 7.1.11(i) / Вправа 7.1.2

theorem Finset.finite_series_of_finite_series {XX : Type u_1} {YY : Type u_2} (X : Finset XX) (Y : Finset YY) (f : XX × YY → ℝ) : ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z

Лема 7.1.13 -

theorem Finset.finite_series_refl {XX : Type u_1} {YY : Type u_2} (X : Finset XX) (Y : Finset YY) (f : XX × YY → ℝ) : ∑ z ∈ X.product Y, f z = ∑ z ∈ Y.product X, f (z.2, z.1)

Наслідок 7.1.14 (Теорема Фубіні для скінченних сум)

theorem Finset.finite_series_comm {XX : Type u_1} {YY : Type u_2} (X : Finset XX) (Y : Finset YY) (f : XX × YY → ℝ) : ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ y ∈ Y, ∑ x ∈ X, f (x, y)

theorem Finset.binomial_theorem (x y : ℝ) (n : ℕ) : (x + y) ^ n = ∑ j ∈ Icc 0 ↑n, ↑n.factorial / (↑j.toNat.factorial * ↑(↑n - j).toNat.factorial) * x ^ j * y ^ (↑n - j)

Вправа 7.1.4. Примітка: можуть виникнути технічні питання при переходах між натуральними числами і цілими. Ознайомтеся з тактиками zify, norm_cast і omega.

theorem Finset.lim_of_finite_series {X : Type u_1} [Fintype X] (a : X → ℕ → ℝ) (L : X → ℝ) (h : ∀ (x : X), Filter.Tendsto (a x) Filter.atTop (nhds (L x))) : Filter.Tendsto (fun (n : ℕ) => ∑ x : X, a x n) Filter.atTop (nhds (∑ x : X, L x))

Вправа 7.1.5