@[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 ⊥)