Analysis I, Section 7.1: Finite 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.

Technical note: it is convenient in Lean to extend finite sequences (usually by zero) to be functions on the entire integers.

Main constructions and results of this section:

• API for summation over finite sets (encoded using Mathlib's Finset type), using the Finset.sum method and the ∑ n ∈ A, f n notation.
• Fubini's theorem for finite series

We do not attempt to replicate the full API for Finset.sum here, but in subsequent sections we shall make liberal use of this API.

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

Definition 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)

Definition 7.1.1. This is similar to Mathlib's Finset.sum_Icc_succ_top except that the latter involves summation over the natural numbers rather than integers.

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

Lemma 7.1.4(a) / Exercise 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)

Lemma 7.1.4(b) / Exercise 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

Lemma 7.1.4(c) / Exercise 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

Lemma 7.1.4(d) / Exercise 7.1.1

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

Lemma 7.1.4(e) / Exercise 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

Lemma 7.1.4(f) / Exercise 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 : ↥(Icc 1 ↑n) → ↥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

Proposition 7.1.8.

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

This fact ensures that Definition 7.1.6 would be well-defined even if we did not appeal to the existing Finset.sum method.

theorem Finset.finite_series_eq {n : ℕ} {Y : Type u_1} (X : Finset Y) (f : Y → ℝ) (g : ↥(Icc 1 ↑n) → ↥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

Definition 7.1.6

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

Proposition 7.1.11(a) / Exercise 7.1.2

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

Proposition 7.1.11(b) / Exercise 7.1.2

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

A technical lemma relating a sum over a finset with a sum over a fintype. Combines well with tools such as map_finite_series below.

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)

Proposition 7.1.11(c) / Exercise 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

Proposition 7.1.11(e) / Exercise 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

Proposition 7.1.11(f) / Exercise 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

Proposition 7.1.11(g) / Exercise 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

Proposition 7.1.11(h) / Exercise 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|

Proposition 7.1.11(i) / Exercise 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

Lemma 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)

Corollary 7.1.14 (Fubini's theorem for finite series)

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)

Exercise 7.1.4. Note: there may be some technicalities passing back and forth between natural numbers and integers. Look into the tactics zify, norm_cast, and 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))

Exercise 7.1.5

theorem Finset.sum_union_disjoint {n : ℕ} {S : Type u_1} [Fintype S] (E : Fin n → Finset S) (disj : ∀ (i j : Fin n), i ≠ j → Disjoint (E i) (E j)) (cover : ∀ (s : S), ∃ (i : Fin n), s ∈ E i) (f : S → ℝ) : ∑ s : S, f s = ∑ i : Fin n, ∑ s ∈ E i, f s

Exercise 7.1.6

theorem Finset.sum_finite_col_row_counts {n m : ℕ} (a : Fin n → Fin m) : ∑ i : Fin n, ↑(a i) = ∑ j : Fin m, {i : Fin n | j < a i}.toFinset.card

Exercise 7.1.7. Uses Fin m (so aᵢ < m) instead of the book's aᵢ ≤ m; the bound is baked into the type, and < replaces ≤ to match the 0-indexed shift.