Analysis I, Section 8.2: Summation on infinite sets

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:

• Absolute convergence and summation on countably infinite or general sets.
• Connections with Mathlib's Summable and tsum.
• The Riemann rearrangement theorem.

Some non-trivial API is provided beyond what is given in the textbook in order connect these notions with existing summation notions.

After this section, the summation notation developed here will be deprecated in favor of Mathlib's API for Summable and tsum.

@[reducible, inline]

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

Definition 8.2.1 (Series on countable sets). Note that with this definition, functions defined on finite sets will not be absolutely convergent; one should use AbsConvergent' instead for such cases.

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 → ℝ) : ℝ

The definition has been chosen to give a sensible value when X is finite, even though AbsConvergent is by definition false in this context.

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)

Theorem 8.2.2, preliminary version. The arguments here are rearranged slightly from the text.

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)

Theorem 8.2.2, second version

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)

Theorem 8.2.2, third version

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

Theorem 8.2.2, fourth version

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

Lemma 8.2.3 / Exercise 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

Not in textbook, but should have been included.

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

Lemma 8.2.5 / Exercise 8.2.2

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

Compare with Mathlib's Summable.subtype

@[reducible, inline]

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

A generalized sum. Note that this will give junk values if f is not 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

Not in textbook, but should have been included (the series laws are significantly harder to establish without this)

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

Not in textbook, but should have been included (the series laws are significantly harder to establish without this)

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

Connection with Mathlib's Summable property. Some version of this might be suitable for Mathlib?

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

Maybe suitable for porting to 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

Connection with Mathlib's tsum (or Σ') operation

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

Proposition 8.2.6 (a) (Absolutely convergent series laws) / Exercise 8.2.3

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

Proposition 8.2.6 (b) (Absolutely convergent series laws) / Exercise 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

This law is not explicitly stated in Proposition 8.2.6, but follows easily from parts (a) and (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

Proposition 8.2.6 (c) (Absolutely convergent series laws) / Exercise 8.2.3. The first part of this proposition has been moved to AbsConvergent'.subtype.

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

This technical claim, the analogue of tsum_univ, is required due to the way Mathlib handles sets.

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

Lemma 8.2.7 / Exercise 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

Theorem 8.2.8 (Riemann rearrangement theorem) / Exercise 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 ⊤)

Exercise 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 ⊥)