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.

namespace Chapter7open BigOperators @[simp] theorem Series.eval_coe (a: ℕ → ℝ) (n: ℕ) : (a: Series).seq n = a n := bya:ℕ → ℝn:ℕ⊢ { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq ↑n = a n simpAll goals completed! 🐙abbrev Series.mk' {m:ℤ} (a: { n // n ≥ m } → ℝ) : Series where m := m seq n := if h : n ≥ m then a ⟨n, h⟩ else 0 vanish := bym:ℤa:{ n // n ≥ m } → ℝ⊢ ∀ n < m, (if h : n ≥ m then a ⟨n, h⟩ else 0) = 0 grindAll goals completed! 🐙theorem Series.eval_mk' {m:ℤ} (a : { n // n ≥ m } → ℝ) {n : ℤ} (h:n ≥ m) : (Series.mk' a).seq n = a ⟨ n, h ⟩ := bym:ℤa:{ n // n ≥ m } → ℝn:ℤh:n ≥ m⊢ (mk' a).seq n = a ⟨n, h⟩ simp [h]All goals completed! 🐙 theorem Series.partial_succ (s : Series) {N:ℤ} (h: N ≥ s.m-1) : s.partial (N+1) = s.partial N + s.seq (N+1) := bys:SeriesN:ℤh:N ≥ s.m - 1⊢ s.partial (N + 1) = s.partial N + s.seq (N + 1) unfold Series.partials:SeriesN:ℤh:N ≥ s.m - 1⊢ ∑ n ∈ Finset.Icc s.m (N + 1), s.seq n = ∑ n ∈ Finset.Icc s.m N, s.seq n + s.seq (N + 1) rw [add_comm (s.partial N) _]s:SeriesN:ℤh:N ≥ s.m - 1⊢ ∑ n ∈ Finset.Icc s.m (N + 1), s.seq n = s.seq (N + 1) + s.partial N convert Finset.sum_insert (show N+1 ∉ Finset.Icc s.m N bys:SeriesN:ℤh:N ≥ s.m - 1⊢ s.partial (N + 1) = s.partial N + s.seq (N + 1) simpAll goals completed! 🐙) symmh.e'_2.hs:SeriesN:ℤh:N ≥ s.m - 1⊢ insert (N + 1) (Finset.Icc s.m N) = Finset.Icc s.m (N + 1); apply Finset.insert_Icc_right_eq_Icc_add_oneh.e'_2.h.hs:SeriesN:ℤh:N ≥ s.m - 1⊢ s.m ≤ N + 1; linarithAll goals completed! 🐙theorem Series.partial_of_lt {s : Series} {N:ℤ} (h: N < s.m) : s.partial N = 0 := bys:SeriesN:ℤh:N < s.m⊢ s.partial N = 0 unfold Series.partials:SeriesN:ℤh:N < s.m⊢ ∑ n ∈ Finset.Icc s.m N, s.seq n = 0 rw [Finset.sum_eq_zero]s:SeriesN:ℤh:N < s.m⊢ ∀ x ∈ Finset.Icc s.m N, s.seq x = 0 intro n hns:SeriesN:ℤh:N < s.mn:ℤhn:n ∈ Finset.Icc s.m N⊢ s.seq n = 0; simp at hns:SeriesN:ℤh:N < s.mn:ℤhn:s.m ≤ n ∧ n ≤ N⊢ s.seq n = 0; grindAll goals completed! 🐙abbrev Series.convergesTo (s : Series) (L:ℝ) : Prop := Filter.atTop.Tendsto (s.partial) (nhds L)abbrev Series.converges (s : Series) : Prop := ∃ L, s.convergesTo Labbrev Series.diverges (s : Series) : Prop := ¬s.convergesopen Classical in noncomputable abbrev Series.sum (s : Series) : ℝ := if h : s.converges then h.choose else 0theorem Series.converges_of_convergesTo {s : Series} {L:ℝ} (h: s.convergesTo L) : s.converges := bys:SeriesL:ℝh:s.convergesTo L⊢ s.converges use LAll goals completed! 🐙 theorem Series.convergesTo_uniq {s : Series} {L L':ℝ} (h: s.convergesTo L) (h': s.convergesTo L') : L = L' := tendsto_nhds_unique h h'theorem Series.convergesTo_sum {s : Series} (h: s.converges) : s.convergesTo s.sum := bys:Seriesh:s.converges⊢ s.convergesTo s.sum simp [sum, h]s:Seriesh:s.converges⊢ s.convergesTo (Exists.choose ⋯); exact h.choose_specAll goals completed! 🐙 theorem declaration uses 'sorry'Series.example_7_2_4a {N:ℤ} (hN: N ≥ 1) : example_7_2_4.partial N = 1 - (2:ℝ)^(-N) := byN:ℤhN:N ≥ 1⊢ example_7_2_4.partial N = 1 - 2 ^ (-N) sorryAll goals completed! 🐙theorem declaration uses 'sorry'Series.example_7_2_4b : example_7_2_4.convergesTo 1 := by⊢ example_7_2_4.convergesTo 1 sorryAll goals completed! 🐙theorem declaration uses 'sorry'Series.example_7_2_4c : example_7_2_4.sum = 1 := by⊢ example_7_2_4.sum = 1 sorryAll goals completed! 🐙noncomputable abbrev Series.example_7_2_4' := mk' (m := 1) (fun n ↦ (2:ℝ)^(n:ℤ))theorem declaration uses 'sorry'Series.example_7_2_4'a {N:ℤ} (hN: N ≥ 1) : example_7_2_4'.partial N = (2:ℝ)^(N+1) - 2 := byN:ℤhN:N ≥ 1⊢ example_7_2_4'.partial N = 2 ^ (N + 1) - 2 sorryAll goals completed! 🐙theorem declaration uses 'sorry'Series.example_7_2_4'b : example_7_2_4'.diverges := by⊢ example_7_2_4'.diverges sorryAll goals completed! 🐙 theorem declaration uses 'sorry'Series.diverges_of_nodecay {s:Series} (h: ¬ Filter.atTop.Tendsto s.seq (nhds 0)) : s.diverges := bys:Seriesh:¬Filter.Tendsto s.seq Filter.atTop (nhds 0)⊢ s.diverges sorryAll goals completed! 🐙 theorem declaration uses 'sorry'Series.example_7_2_7' : ((fun n:ℕ ↦ (-1:ℝ)^n):Series).diverges := by⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => (-1) ^ n) n.toNat else 0, vanish := ⋯ }.diverges apply diverges_of_nodecayh⊢ ¬Filter.Tendsto { m := 0, seq := fun n => if n ≥ 0 then (fun n => (-1) ^ n) n.toNat else 0, vanish := ⋯ }.seq Filter.atTop (nhds 0) sorryAll goals completed! 🐙 abbrev Series.absConverges (s:Series) : Prop := s.abs.convergesabbrev Series.condConverges (s:Series) : Prop := s.converges ∧ ¬ s.absConverges theorem declaration uses 'sorry'Series.abs_le {s:Series} (h : s.absConverges) : |s.sum| ≤ s.abs.sum := bys:Seriesh:s.absConverges⊢ |s.sum| ≤ s.abs.sum sorryAll goals completed! 🐙 theorem declaration uses 'sorry'Series.example_7_2_13a : example_7_2_13.converges := by⊢ example_7_2_13.converges sorryAll goals completed! 🐙theorem declaration uses 'sorry'Series.example_7_2_13b : ¬ example_7_2_13.absConverges := by⊢ ¬example_7_2_13.absConverges sorryAll goals completed! 🐙theorem declaration uses 'sorry'Series.example_7_2_13c : example_7_2_13.condConverges := by⊢ example_7_2_13.condConverges sorryAll goals completed! 🐙instance Series.inst_add : Add Series where add a b := { m := max a.m b.m seq n := if n ≥ max a.m b.m then a.seq n + b.seq n else 0 vanish n hn := bya:Seriesb:Seriesn:ℤhn:n < max a.m b.m⊢ (if n ≥ max a.m b.m then a.seq n + b.seq n else 0) = 0 rw [lt_iff_not_ge] at hna:Seriesb:Seriesn:ℤhn:¬max a.m b.m ≤ n⊢ (if n ≥ max a.m b.m then a.seq n + b.seq n else 0) = 0; simp [hn]All goals completed! 🐙 }theorem Series.add_coe (a b: ℕ → ℝ) : (a:Series) + (b:Series) = (fun n ↦ a n + b n) := bya:ℕ → ℝ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 := ⋯ } ext nma:ℕ → ℝ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 = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n + b n) n.toNat else 0, vanish := ⋯ }.mseq.ha:ℕ → ℝb:ℕ → ℝn:ℤ⊢ ({ 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 := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n + b n) n.toNat else 0, vanish := ⋯ }.seq n; rflseq.ha:ℕ → ℝb:ℕ → ℝn:ℤ⊢ ({ 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 := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n + b n) n.toNat else 0, vanish := ⋯ }.seq n by_cases h:n ≥ 0pos._@._hyg.3496a:ℕ → ℝb:ℕ → ℝn:ℤh:n ≥ 0⊢ ({ 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 := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n + b n) n.toNat else 0, vanish := ⋯ }.seq nneg._@._hyg.3496a:ℕ → ℝb:ℕ → ℝn:ℤh:¬n ≥ 0⊢ ({ 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 := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n + b n) n.toNat else 0, vanish := ⋯ }.seq n <;>pos._@._hyg.3496a:ℕ → ℝb:ℕ → ℝn:ℤh:n ≥ 0⊢ ({ 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 := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n + b n) n.toNat else 0, vanish := ⋯ }.seq nneg._@._hyg.3496a:ℕ → ℝb:ℕ → ℝn:ℤh:¬n ≥ 0⊢ ({ 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 := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n + b n) n.toNat else 0, vanish := ⋯ }.seq n simp [h, HAdd.hAdd, Add.add]All goals completed! 🐙 theorem declaration uses 'sorry'Series.add {s t:Series} (hs: s.converges) (ht: t.converges) : (s + t).converges ∧ (s+t).sum = s.sum + t.sum := bys:Seriest:Serieshs:s.convergesht:t.converges⊢ (s + t).converges ∧ (s + t).sum = s.sum + t.sum sorryAll goals completed! 🐙instance Series.inst.smul : SMul ℝ Series where smul c s := { m := s.m seq n := if n ≥ s.m then c * s.seq n else 0 vanish := byc:ℝs:Series⊢ ∀ n < s.m, (if n ≥ s.m then c * s.seq n else 0) = 0 grindAll goals completed! 🐙 }theorem Series.smul_coe (a: ℕ → ℝ) (c: ℝ) : (c • a:Series) = (fun n ↦ c * a n) := bya:ℕ → ℝ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 := ⋯ } ext nma:ℕ → ℝc:ℝ⊢ (c • { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }).m = { m := 0, seq := fun n => if n ≥ 0 then (fun n => c * a n) n.toNat else 0, vanish := ⋯ }.mseq.ha:ℕ → ℝc:ℝn:ℤ⊢ (c • { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => c * a n) n.toNat else 0, vanish := ⋯ }.seq n; rflseq.ha:ℕ → ℝc:ℝn:ℤ⊢ (c • { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => c * a n) n.toNat else 0, vanish := ⋯ }.seq n by_cases h:n ≥ 0pos._@._hyg.3733a:ℕ → ℝc:ℝn:ℤh:n ≥ 0⊢ (c • { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => c * a n) n.toNat else 0, vanish := ⋯ }.seq nneg._@._hyg.3733a:ℕ → ℝc:ℝn:ℤh:¬n ≥ 0⊢ (c • { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => c * a n) n.toNat else 0, vanish := ⋯ }.seq n <;>pos._@._hyg.3733a:ℕ → ℝc:ℝn:ℤh:n ≥ 0⊢ (c • { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => c * a n) n.toNat else 0, vanish := ⋯ }.seq nneg._@._hyg.3733a:ℕ → ℝc:ℝn:ℤh:¬n ≥ 0⊢ (c • { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => c * a n) n.toNat else 0, vanish := ⋯ }.seq n simp [h, HSMul.hSMul, SMul.smul]All goals completed! 🐙 theorem declaration uses 'sorry'Series.smul {c:ℝ} {s:Series} (hs: s.converges) : (c • s).converges ∧ (c • s).sum = c * s.sum := byc:ℝs:Serieshs:s.converges⊢ (c • s).converges ∧ (c • s).sum = c * s.sum sorryAll goals completed! 🐙 theorem Series.sub_coe (a b: ℕ → ℝ) : (a:Series) - (b:Series) = (fun n ↦ a n - b n) := bya:ℕ → ℝ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 := ⋯ } ext nma:ℕ → ℝ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 = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n - b n) n.toNat else 0, vanish := ⋯ }.mseq.ha:ℕ → ℝb:ℕ → ℝn:ℤ⊢ ({ 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 := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n - b n) n.toNat else 0, vanish := ⋯ }.seq n; rflseq.ha:ℕ → ℝb:ℕ → ℝn:ℤ⊢ ({ 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 := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n - b n) n.toNat else 0, vanish := ⋯ }.seq n by_cases h:n ≥ 0pos._@._hyg.3981a:ℕ → ℝb:ℕ → ℝn:ℤh:n ≥ 0⊢ ({ 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 := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n - b n) n.toNat else 0, vanish := ⋯ }.seq nneg._@._hyg.3981a:ℕ → ℝb:ℕ → ℝn:ℤh:¬n ≥ 0⊢ ({ 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 := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n - b n) n.toNat else 0, vanish := ⋯ }.seq n <;>pos._@._hyg.3981a:ℕ → ℝb:ℕ → ℝn:ℤh:n ≥ 0⊢ ({ 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 := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n - b n) n.toNat else 0, vanish := ⋯ }.seq nneg._@._hyg.3981a:ℕ → ℝb:ℕ → ℝn:ℤh:¬n ≥ 0⊢ ({ 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 := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n - b n) n.toNat else 0, vanish := ⋯ }.seq n simp [h, HSub.hSub, Sub.sub]All goals completed! 🐙theorem declaration uses 'sorry'Series.convergesTo.sub {s t:Series} {L M: ℝ} (hs: s.convergesTo L) (ht: t.convergesTo M) : (s - t).convergesTo (L - M) := bys:Seriest:SeriesL:ℝM:ℝhs:s.convergesTo Lht:t.convergesTo M⊢ (s - t).convergesTo (L - M) sorryAll goals completed! 🐙theorem declaration uses 'sorry'Series.sub {s t:Series} (hs: s.converges) (ht: t.converges) : (s - t).converges ∧ (s-t).sum = s.sum - t.sum := bys:Seriest:Serieshs:s.convergesht:t.converges⊢ (s - t).converges ∧ (s - t).sum = s.sum - t.sum sorryAll goals completed! 🐙abbrev Series.from (s:Series) (m₁:ℤ) : Series := mk' (m := max s.m m₁) (fun n ↦ s.seq (n:ℤ)) theorem declaration uses 'sorry'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 := bys:Seriesk:ℕh:s.converges⊢ s.sum = ∑ n ∈ Finset.Ico s.m (s.m + ↑k), s.seq n + (s.from (s.m + ↑k)).sum sorryAll goals completed! 🐙 /- Exercise 7.2.1 -/ def declaration uses 'sorry'Series.exercise_7_2_1_convergent : Decidable ((mk' (m := 1) (fun n ↦ (-1:ℝ)^(n:ℤ))).converges ) := by⊢ Decidable (mk' fun n => (-1) ^ ↑n).converges -- The first line of this proof should be `apply isTrue` or `apply isFalse`. sorryAll goals completed! 🐙end Chapter7