Analysis I, Section 7.2: Infinite 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.

Main constructions and results of this section:

• Formal series and their limits.
• Absolute convergence; basic series laws.

structure Chapter7.Series : Type

Definition 7.2.1 (Formal infinite series). This is similar to Chapter 6 sequence, but is manipulated differently. As with Chapter 5, we will start series from 0 by default.

• m : ℤ
• seq : ℤ → ℝ
• vanish (n : ℤ) : n < self.m → self.seq n = 0

theorem Chapter7.Series.ext_iff {x y : Series} : x = y ↔ x.m = y.m ∧ x.seq = y.seq

theorem Chapter7.Series.ext {x y : Series} (m : x.m = y.m) (seq : x.seq = y.seq) : x = y

instance Chapter7.Series.instCoe : Coe (ℕ → ℝ) Series

Functions from ℕ to ℝ can be thought of as series.

Equations

• Chapter7.Series.instCoe = { coe := fun (a : ℕ → ℝ) => { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } }

@[simp]

theorem Chapter7.Series.eval_coe (a : ℕ → ℝ) (n : ℕ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq ↑n = a n

@[reducible, inline]

abbrev Chapter7.Series.mk' {m : ℤ} (a : { n : ℤ // n ≥ m } → ℝ) : Series

Equations

• Chapter7.Series.mk' a = { m := m, seq := fun (n : ℤ) => if h : n ≥ m then a ⟨n, h⟩ else 0, vanish := ⋯ }

theorem Chapter7.Series.eval_mk' {m : ℤ} (a : { n : ℤ // n ≥ m } → ℝ) {n : ℤ} (h : n ≥ m) : (mk' a).seq n = a ⟨n, h⟩

@[reducible, inline]

abbrev Chapter7.Series.partial (s : Series) (N : ℤ) : ℝ

Definition 7.2.2 (Convergence of series)

Equations

• s.partial N = ∑ n ∈ Finset.Icc s.m N, s.seq n

theorem Chapter7.Series.partial_succ (s : Series) {N : ℤ} (h : N ≥ s.m - 1) : s.partial (N + 1) = s.partial N + s.seq (N + 1)

theorem Chapter7.Series.partial_of_lt {s : Series} {N : ℤ} (h : N < s.m) : s.partial N = 0

@[reducible, inline]

abbrev Chapter7.Series.convergesTo (s : Series) (L : ℝ) : Prop

Equations

• s.convergesTo L = Filter.Tendsto s.partial Filter.atTop (nhds L)

@[reducible, inline]

abbrev Chapter7.Series.converges (s : Series) : Prop

Equations

• s.converges = ∃ (L : ℝ), s.convergesTo L

@[reducible, inline]

abbrev Chapter7.Series.diverges (s : Series) : Prop

Equations

• s.diverges = ¬s.converges

@[reducible, inline]

noncomputable abbrev Chapter7.Series.sum (s : Series) : ℝ

Equations

• s.sum = if h : s.converges then Exists.choose h else 0

theorem Chapter7.Series.converges_of_convergesTo {s : Series} {L : ℝ} (h : s.convergesTo L) : s.converges

theorem Chapter7.Series.sum_of_converges {s : Series} {L : ℝ} (h : s.convergesTo L) : s.sum = L

Remark 7.2.3

theorem Chapter7.Series.convergesTo_uniq {s : Series} {L L' : ℝ} (h : s.convergesTo L) (h' : s.convergesTo L') : L = L'

theorem Chapter7.Series.convergesTo_sum {s : Series} (h : s.converges) : s.convergesTo s.sum

@[reducible, inline]

noncomputable abbrev Chapter7.Series.example_7_2_4 : Series

Example 7.2.4

Equations

• Chapter7.Series.example_7_2_4 = Chapter7.Series.mk' fun (n : { n : ℤ // n ≥ 1 }) => 2 ^ (-↑n)

theorem Chapter7.Series.example_7_2_4a {N : ℤ} (hN : N ≥ 1) : example_7_2_4.partial N = 1 - 2 ^ (-N)

theorem Chapter7.Series.example_7_2_4b : example_7_2_4.convergesTo 1

theorem Chapter7.Series.example_7_2_4c : example_7_2_4.sum = 1

@[reducible, inline]

noncomputable abbrev Chapter7.Series.example_7_2_4' : Series

Equations

• Chapter7.Series.example_7_2_4' = Chapter7.Series.mk' fun (n : { n : ℤ // n ≥ 1 }) => 2 ^ ↑n

theorem Chapter7.Series.example_7_2_4'a {N : ℤ} (hN : N ≥ 1) : example_7_2_4'.partial N = 2 ^ (N + 1) - 2

theorem Chapter7.Series.example_7_2_4'b : example_7_2_4'.diverges

theorem Chapter7.Series.converges_iff_tail_decay (s : Series) : s.converges ↔ ∀ ε > 0, ∃ N ≥ s.m, ∀ p ≥ N, ∀ q ≥ N, |∑ n ∈ Finset.Icc p q, s.seq n| ≤ ε

Proposition 7.2.5 / Exercise 7.2.2

theorem Chapter7.Series.decay_of_converges {s : Series} (h : s.converges) : Filter.Tendsto s.seq Filter.atTop (nhds 0)

Corollary 7.2.6 (Zero test) / Exercise 7.2.3

theorem Chapter7.Series.diverges_of_nodecay {s : Series} (h : ¬Filter.Tendsto s.seq Filter.atTop (nhds 0)) : s.diverges

theorem Chapter7.Series.example_7_2_7 : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => 1) n.toNat else 0, vanish := ⋯ }.diverges

Example 7.2.7

theorem Chapter7.Series.example_7_2_7' : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => (-1) ^ n) n.toNat else 0, vanish := ⋯ }.diverges

@[reducible, inline]

abbrev Chapter7.Series.abs (s : Series) : Series

Definition 7.2.8 (Absolute convergence)

Equations

• s.abs = Chapter7.Series.mk' fun (n : { n : ℤ // n ≥ s.m }) => |s.seq ↑n|

@[reducible, inline]

abbrev Chapter7.Series.absConverges (s : Series) : Prop

Equations

• s.absConverges = s.abs.converges

@[reducible, inline]

abbrev Chapter7.Series.condConverges (s : Series) : Prop

Equations

• s.condConverges = (s.converges ∧ ¬s.absConverges)

theorem Chapter7.Series.converges_of_absConverges {s : Series} (h : s.absConverges) : s.converges

Proposition 7.2.9 (Absolute convergence test) / Example 7.2.4

theorem Chapter7.Series.abs_le {s : Series} (h : s.absConverges) : |s.sum| ≤ s.abs.sum

theorem Chapter7.Series.converges_of_alternating {m : ℤ} {a : { n : ℤ // n ≥ m } → ℝ} (ha : ∀ (n : { n : ℤ // n ≥ m }), a n ≥ 0) (ha' : Antitone a) : (mk' fun (n : { n : ℤ // n ≥ m }) => (-1) ^ ↑n * a n).converges ↔ Filter.Tendsto a Filter.atTop (nhds 0)

Proposition 7.2.12 (Alternating series test)

@[reducible, inline]

noncomputable abbrev Chapter7.Series.example_7_2_13 : Series

Example 7.2.13

Equations

• Chapter7.Series.example_7_2_13 = Chapter7.Series.mk' fun (n : { n : ℤ // n ≥ 1 }) => (-1) ^ ↑n / ↑↑n

theorem Chapter7.Series.example_7_2_13a : example_7_2_13.converges

theorem Chapter7.Series.example_7_2_13b : ¬example_7_2_13.absConverges

theorem Chapter7.Series.example_7_2_13c : example_7_2_13.condConverges

instance Chapter7.Series.inst_add : Add Series

Equations

• Chapter7.Series.inst_add = { add := fun (a b : Chapter7.Series) => { m := max a.m b.m, seq := fun (n : ℤ) => if n ≥ max a.m b.m then a.seq n + b.seq n else 0, vanish := ⋯ } }

theorem Chapter7.Series.add_coe (a b : ℕ → ℝ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } + { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ } = { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => a n + b n) n.toNat else 0, vanish := ⋯ }

theorem Chapter7.Series.convergesTo.add {s t : Series} {L M : ℝ} (hs : s.convergesTo L) (ht : t.convergesTo M) : (s + t).convergesTo (L + M)

Proposition 7.2.14 (a) (Series laws) / Exercise 7.2.5. The convergesTo form can be more convenient for applications.

theorem Chapter7.Series.add {s t : Series} (hs : s.converges) (ht : t.converges) : (s + t).converges ∧ (s + t).sum = s.sum + t.sum

instance Chapter7.Series.inst.smul : SMul ℝ Series

Equations

• Chapter7.Series.inst.smul = { smul := fun (c : ℝ) (s : Chapter7.Series) => { m := s.m, seq := fun (n : ℤ) => if n ≥ s.m then c * s.seq n else 0, vanish := ⋯ } }

theorem Chapter7.Series.smul_coe (a : ℕ → ℝ) (c : ℝ) : c • { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } = { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => c * a n) n.toNat else 0, vanish := ⋯ }

theorem Chapter7.Series.convergesTo.smul {s : Series} {L c : ℝ} (hs : s.convergesTo L) : (c • s).convergesTo (c * L)

Proposition 7.2.14 (b) (Series laws) / Exercise 7.2.5. The convergesTo form can be more convenient for applications.

theorem Chapter7.Series.smul {c : ℝ} {s : Series} (hs : s.converges) : (c • s).converges ∧ (c • s).sum = c * s.sum

instance Chapter7.Series.inst_sub : Sub Series

The corresponding API for subtraction was not in the textbook, but is useful in later sections, so is included here.

Equations

• Chapter7.Series.inst_sub = { sub := fun (a b : Chapter7.Series) => { m := max a.m b.m, seq := fun (n : ℤ) => if n ≥ max a.m b.m then a.seq n - b.seq n else 0, vanish := ⋯ } }

theorem Chapter7.Series.sub_coe (a b : ℕ → ℝ) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } - { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ } = { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => a n - b n) n.toNat else 0, vanish := ⋯ }

theorem Chapter7.Series.convergesTo.sub {s t : Series} {L M : ℝ} (hs : s.convergesTo L) (ht : t.convergesTo M) : (s - t).convergesTo (L - M)

theorem Chapter7.Series.sub {s t : Series} (hs : s.converges) (ht : t.converges) : (s - t).converges ∧ (s - t).sum = s.sum - t.sum

@[reducible, inline]

abbrev Chapter7.Series.from (s : Series) (m₁ : ℤ) : Series

Equations

• s.from m₁ = Chapter7.Series.mk' fun (n : { n : ℤ // n ≥ max s.m m₁ }) => s.seq ↑n

theorem Chapter7.Series.converges_from (s : Series) (k : ℕ) : s.converges ↔ (s.from (s.m + ↑k)).converges

Proposition 7.2.14 (c) (Series laws) / Exercise 7.2.5

theorem Chapter7.Series.sum_from {s : Series} (k : ℕ) (h : s.converges) : s.sum = ∑ n ∈ Finset.Ico s.m (s.m + ↑k), s.seq n + (s.from (s.m + ↑k)).sum

theorem Chapter7.Series.shift {s : Series} {x : ℝ} (h : s.convergesTo x) (L : ℤ) : (mk' fun (n : { n : ℤ // n ≥ s.m + L }) => s.seq (↑n - L)).convergesTo x

Proposition 7.2.14 (d) (Series laws) / Exercise 7.2.5

theorem Chapter7.Series.telescope {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop (nhds 0)) : { m := 0, seq := fun (n : ℤ) => if n ≥ 0 then (fun (n : ℕ) => a (n + 1) - a n) n.toNat else 0, vanish := ⋯ }.convergesTo (a 0)

Lemma 7.2.15 (telescoping series) / Exercise 7.2.6

def Chapter7.Series.exercise_7_2_1_convergent : Decidable (mk' fun (n : { n : ℤ // n ≥ 1 }) => (-1) ^ ↑n).converges

Equations

• Chapter7.Series.exercise_7_2_1_convergent = sorry