Analysis
7.2. Infinite series

Imports

import Mathlib.Tactic
import Mathlib.Algebra.Field.Power

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

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.

@[ext]
structure Series where
  m : ℤ
  seq : ℤ → ℝ
  vanish : ∀ n < m, seq n = 0

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

instance Series.instCoe : Coe (ℕ → ℝ) Series where
  coe := fun a ↦ {
    m := 0
    seq n := if n ≥ 0 then a n.toNat else 0
    vanish := bya:ℕ → ℝ⊢ ∀ n < 0, (if n ≥ 0 then a n.toNat else 0) = 0 grindAll goals completed! 🐙
  }

              @[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! 🐙

Definition 7.2.2 (Convergence of series)

noncomputable abbrev Series.partial (s : Series) (N:ℤ) : ℝ := ∑ n ∈ Finset.Icc s.m N, s.seq n

              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! 🐙

Remark 7.2.3

theorem Series.sum_of_converges {s : Series} {L:ℝ} (h: s.convergesTo L) : s.sum = L := bys:SeriesL:ℝh:s.convergesTo L⊢ s.sum = L
  simp [sum, converges_of_convergesTo h]s:SeriesL:ℝh:s.convergesTo L⊢ Exists.choose ⋯ = L
  exact tendsto_nhds_unique ((converges_of_convergesTo h).choose_spec) hAll 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! 🐙

Example 7.2.4

noncomputable abbrev Series.example_7_2_4 := mk' (m := 1) (fun n ↦ (2:ℝ)^(-n:ℤ))

              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! 🐙

Proposition 7.2.5 / Exercise 7.2.2

theorem declaration uses `sorry`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| ≤ ε := bys:Series⊢ s.converges ↔ ∀ ε > 0, ∃ N ≥ s.m, ∀ p ≥ N, ∀ q ≥ N, |∑ n ∈ Finset.Icc p q, s.seq n| ≤ ε
  sorryAll goals completed! 🐙

Corollary 7.2.6 (Zero test) / Exercise 7.2.3

theorem declaration uses `sorry`Series.decay_of_converges {s:Series} (h: s.converges) :
    Filter.atTop.Tendsto s.seq (nhds 0) := bys:Seriesh:s.converges⊢ Filter.Tendsto s.seq Filter.atTop (nhds 0)
  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! 🐙

Example 7.2.7

theorem declaration uses `sorry`Series.example_7_2_7 : ((fun _:ℕ ↦ (1:ℝ)):Series).diverges := by⊢ { m := 0, seq := fun n ↦ if n ≥ 0 then (fun x ↦ 1) n.toNat else 0, vanish := ⋯ }.diverges
  apply diverges_of_nodecayh⊢ ¬Filter.Tendsto { m := 0, seq := fun n ↦ if n ≥ 0 then (fun x ↦ 1) n.toNat else 0, vanish := ⋯ }.seq Filter.atTop
    (nhds 0)
  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! 🐙

Definition 7.2.8 (Absolute convergence)

abbrev Series.abs (s:Series) : Series := mk' (m:=s.m) (fun n ↦ |s.seq n|)

abbrev Series.absConverges (s:Series) : Prop := s.abs.convergesabbrev Series.condConverges (s:Series) : Prop := s.converges ∧ ¬ s.absConverges

Proposition 7.2.9 (Absolute convergence test) / Exercise 7.2.4

theorem declaration uses `sorry`Series.converges_of_absConverges {s:Series} (h : s.absConverges) : s.converges := bys:Seriesh:s.absConverges⊢ s.converges
  sorryAll goals completed! 🐙

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! 🐙

Proposition 7.2.12 (Alternating series test)

theorem declaration uses `sorry`Series.converges_of_alternating {m:ℤ} {a: { n // n ≥ m} → ℝ} (ha: ∀ n, a n ≥ 0)
  (ha': Antitone a) :
    ((mk' (fun n ↦ (-1)^(n:ℤ) * a n)).converges ↔ Filter.atTop.Tendsto a (nhds 0)) := bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ (mk' fun n ↦ (-1) ^ ↑n * a n).converges ↔ Filter.Tendsto a Filter.atTop (nhds 0)
  -- This proof is written to follow the structure of the original text.
  constructormpm:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ (mk' fun n ↦ (-1) ^ ↑n * a n).converges → Filter.Tendsto a Filter.atTop (nhds 0)mprm:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ Filter.Tendsto a Filter.atTop (nhds 0) → (mk' fun n ↦ (-1) ^ ↑n * a n).converges
  .mpm:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ (mk' fun n ↦ (-1) ^ ↑n * a n).converges → Filter.Tendsto a Filter.atTop (nhds 0) intro hmpm:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:(mk' fun n ↦ (-1) ^ ↑n * a n).converges⊢ Filter.Tendsto a Filter.atTop (nhds 0); apply decay_of_converges at hmpm:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto (mk' fun n ↦ (-1) ^ ↑n * a n).seq Filter.atTop (nhds 0)⊢ Filter.Tendsto a Filter.atTop (nhds 0)
    rw [tendsto_iff_dist_tendsto_zero] at h ⊢mpm:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto (fun b ↦ dist ((mk' fun n ↦ (-1) ^ ↑n * a n).seq b) 0) Filter.atTop (nhds 0)⊢ Filter.Tendsto (fun b ↦ dist (a b) 0) Filter.atTop (nhds 0)
    rw [←Filter.tendsto_comp_val_Ici_atTop (a := m)] at hmpm:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto (fun x ↦ dist ((mk' fun n ↦ (-1) ^ ↑n * a n).seq ↑x) 0) Filter.atTop (nhds 0)⊢ Filter.Tendsto (fun b ↦ dist (a b) 0) Filter.atTop (nhds 0)
    refine h.congr (fun n => ?_)mpm:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto (fun x ↦ dist ((mk' fun n ↦ (-1) ^ ↑n * a n).seq ↑x) 0) Filter.atTop (nhds 0)n:{ n // n ≥ m }⊢ dist ((mk' fun n ↦ (-1) ^ ↑n * a n).seq ↑n) 0 = dist (a n) 0
    simp [n.property]All goals completed! 🐙
  intro hmprm:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)⊢ (mk' fun n ↦ (-1) ^ ↑n * a n).converges
  unfold converges convergesTomprm:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)⊢ ∃ L, Filter.Tendsto (mk' fun n ↦ (-1) ^ ↑n * a n).partial Filter.atTop (nhds L)
  set b := mk' fun n ↦ (-1) ^ (n:ℤ) * a nmprm:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a n⊢ ∃ L, Filter.Tendsto b.partial Filter.atTop (nhds L)
  set S := b.partialmprm:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partial⊢ ∃ L, Filter.Tendsto S Filter.atTop (nhds L)
  have claim0 {N:ℤ} (hN: N ≥ m) : S (N+1) = S N + (-1)^(N+1) * a ⟨ N+1, bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialN:ℤhN:N ≥ m⊢ N + 1 ≥ m grindAll goals completed! 🐙 ⟩ := bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ (mk' fun n ↦ (-1) ^ ↑n * a n).converges ↔ Filter.Tendsto a Filter.atTop (nhds 0)
    convert b.partial_succ ?_h.e'_3.h.e'_6m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialN:ℤhN:N ≥ m⊢ (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩ = b.seq (N + 1)convert_2m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialN:ℤhN:N ≥ m⊢ N ≥ b.m - 1; simp [b, show N+1 ≥ m by grind]convert_2m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialN:ℤhN:N ≥ m⊢ N ≥ b.m - 1; linarithAll goals completed! 🐙
  have claim1 {N:ℤ} (hN: N ≥ m) : S (N+2) = S N + (-1)^(N+1) * (a ⟨ N+1, bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩N:ℤhN:N ≥ m⊢ N + 1 ≥ m grindAll goals completed! 🐙 ⟩ - a ⟨ N+2, bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩N:ℤhN:N ≥ m⊢ N + 2 ≥ m grindAll goals completed! 🐙 ⟩) := calc
      S (N+2) = S N + (-1)^(N+1) * a ⟨ N+1, bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩N:ℤhN:N ≥ m⊢ N + 1 ≥ m grindAll goals completed! 🐙 ⟩ + (-1)^(N+2) * a ⟨ N+2, bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩N:ℤhN:N ≥ m⊢ N + 2 ≥ m grindAll goals completed! 🐙 ⟩ := bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩N:ℤhN:N ≥ m⊢ S (N + 2) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩ + (-1) ^ (N + 2) * a ⟨N + 2, ⋯⟩
        simp_rw [m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩N:ℤhN:N ≥ m⊢ S (N + 2) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩ + (-1) ^ (N + 2) * a ⟨N + 2, ⋯⟩←claim0 hN, show N+2=N+1+1 bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩N:ℤhN:N ≥ m⊢ S (N + 2) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩ + (-1) ^ (N + 2) * a ⟨N + 2, ⋯⟩ abelAll goals completed! 🐙]; apply claim0hNm:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩N:ℤhN:N ≥ m⊢ N + 1 ≥ m; linarithAll goals completed! 🐙
      _ = S N + (-1)^(N+1) * a ⟨ N+1, bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩N:ℤhN:N ≥ m⊢ N + 1 ≥ m grindAll goals completed! 🐙 ⟩ + (-1) * (-1)^(N+1) * a ⟨ N+2, bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩N:ℤhN:N ≥ m⊢ N + 2 ≥ m grindAll goals completed! 🐙 ⟩ := bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩N:ℤhN:N ≥ m⊢ S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩ + (-1) ^ (N + 2) * a ⟨N + 2, ⋯⟩ =
  S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩ + -1 * (-1) ^ (N + 1) * a ⟨N + 2, ⋯⟩
        congre_a.e_am:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩N:ℤhN:N ≥ m⊢ (-1) ^ (N + 2) = -1 * (-1) ^ (N + 1); rw [←zpow_one_add₀]e_a.e_am:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩N:ℤhN:N ≥ m⊢ (-1) ^ (N + 2) = (-1) ^ (1 + (N + 1))e_a.e_a.hm:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩N:ℤhN:N ≥ m⊢ -1 ≠ 0 <;>e_a.e_am:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩N:ℤhN:N ≥ m⊢ (-1) ^ (N + 2) = (-1) ^ (1 + (N + 1))e_a.e_a.hm:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩N:ℤhN:N ≥ m⊢ -1 ≠ 0 grindAll goals completed! 🐙
      _ = _ := bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩N:ℤhN:N ≥ m⊢ S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩ + -1 * (-1) ^ (N + 1) * a ⟨N + 2, ⋯⟩ =
  S N + (-1) ^ (N + 1) * (a ⟨N + 1, ⋯⟩ - a ⟨N + 2, ⋯⟩) ringAll goals completed! 🐙
  have claim2 {N:ℤ} (hN: N ≥ m) (h': Odd N) : S (N+2) ≥ S N := bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ (mk' fun n ↦ (-1) ^ ↑n * a n).converges ↔ Filter.Tendsto a Filter.atTop (nhds 0)
    simp [claim1 hN, h'.add_one.neg_one_zpow]m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩claim1:∀ {N : ℤ} (hN : N ≥ m), S (N + 2) = S N + (-1) ^ (N + 1) * (a ⟨N + 1, ⋯⟩ - a ⟨N + 2, ⋯⟩)N:ℤhN:N ≥ mh':Odd N⊢ a ⟨N + 2, ⋯⟩ ≤ a ⟨N + 1, ⋯⟩; apply ha'am:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩claim1:∀ {N : ℤ} (hN : N ≥ m), S (N + 2) = S N + (-1) ^ (N + 1) * (a ⟨N + 1, ⋯⟩ - a ⟨N + 2, ⋯⟩)N:ℤhN:N ≥ mh':Odd N⊢ ⟨N + 1, ⋯⟩ ≤ ⟨N + 2, ⋯⟩; simpAll goals completed! 🐙
  have claim3 {N:ℤ} (hN: N ≥ m) (h': Even N) : S (N+2) ≤ S N := bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ (mk' fun n ↦ (-1) ^ ↑n * a n).converges ↔ Filter.Tendsto a Filter.atTop (nhds 0)
    simp [claim1 hN, h'.add_one.neg_one_zpow]m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩claim1:∀ {N : ℤ} (hN : N ≥ m), S (N + 2) = S N + (-1) ^ (N + 1) * (a ⟨N + 1, ⋯⟩ - a ⟨N + 2, ⋯⟩)claim2:∀ {N : ℤ}, N ≥ m → Odd N → S (N + 2) ≥ S NN:ℤhN:N ≥ mh':Even N⊢ a ⟨N + 2, ⋯⟩ ≤ a ⟨N + 1, ⋯⟩; apply ha'am:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩claim1:∀ {N : ℤ} (hN : N ≥ m), S (N + 2) = S N + (-1) ^ (N + 1) * (a ⟨N + 1, ⋯⟩ - a ⟨N + 2, ⋯⟩)claim2:∀ {N : ℤ}, N ≥ m → Odd N → S (N + 2) ≥ S NN:ℤhN:N ≥ mh':Even N⊢ ⟨N + 1, ⋯⟩ ≤ ⟨N + 2, ⋯⟩; simpAll goals completed! 🐙
  have why1 {N:ℤ} (hN: N ≥ m) (h': Even N) (k:ℕ) : S (N+2*k) ≤ S N := bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ (mk' fun n ↦ (-1) ^ ↑n * a n).converges ↔ Filter.Tendsto a Filter.atTop (nhds 0) sorryAll goals completed! 🐙
  have why2 {N:ℤ} (hN: N ≥ m) (h': Even N) (k:ℕ) : S (N+2*k+1) ≥ S N - a ⟨ N+1, bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩claim1:∀ {N : ℤ} (hN : N ≥ m), S (N + 2) = S N + (-1) ^ (N + 1) * (a ⟨N + 1, ⋯⟩ - a ⟨N + 2, ⋯⟩)claim2:∀ {N : ℤ}, N ≥ m → Odd N → S (N + 2) ≥ S Nclaim3:∀ {N : ℤ}, N ≥ m → Even N → S (N + 2) ≤ S Nwhy1:∀ {N : ℤ}, N ≥ m → Even N → ∀ (k : ℕ), S (N + 2 * ↑k) ≤ S NN:ℤhN:N ≥ mh':Even Nk:ℕ⊢ N + 1 ≥ m grindAll goals completed! 🐙 ⟩ := bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ (mk' fun n ↦ (-1) ^ ↑n * a n).converges ↔ Filter.Tendsto a Filter.atTop (nhds 0) sorryAll goals completed! 🐙
  have why3 {N:ℤ} (hN: N ≥ m) (h': Even N) (k:ℕ) : S (N+2*k+1) ≤ S (N+2*k) := bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ (mk' fun n ↦ (-1) ^ ↑n * a n).converges ↔ Filter.Tendsto a Filter.atTop (nhds 0) sorryAll goals completed! 🐙
  have claim4 {N:ℤ} (hN: N ≥ m) (h': Even N) (k:ℕ) : S N -
 a ⟨ N+1, bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩claim1:∀ {N : ℤ} (hN : N ≥ m), S (N + 2) = S N + (-1) ^ (N + 1) * (a ⟨N + 1, ⋯⟩ - a ⟨N + 2, ⋯⟩)claim2:∀ {N : ℤ}, N ≥ m → Odd N → S (N + 2) ≥ S Nclaim3:∀ {N : ℤ}, N ≥ m → Even N → S (N + 2) ≤ S Nwhy1:∀ {N : ℤ}, N ≥ m → Even N → ∀ (k : ℕ), S (N + 2 * ↑k) ≤ S Nwhy2:∀ {N : ℤ} (hN : N ≥ m), Even N → ∀ (k : ℕ), S (N + 2 * ↑k + 1) ≥ S N - a ⟨N + 1, ⋯⟩why3:∀ {N : ℤ}, N ≥ m → Even N → ∀ (k : ℕ), S (N + 2 * ↑k + 1) ≤ S (N + 2 * ↑k)N:ℤhN:N ≥ mh':Even Nk:ℕ⊢ N + 1 ≥ m grindAll goals completed! 🐙 ⟩ ≤ S (N + 2*k + 1) ∧ S (N + 2*k + 1) ≤ S (N + 2*k) ∧ S (N + 2*k) ≤ S N := ⟨ ge_iff_le.mp (why2 hN h' k), why3 hN h' k, why1 hN h' k ⟩
  have why4 {N n:ℤ} (hN: N ≥ m) (h': Even N) (hn: n ≥ N) : S N - a ⟨ N+1, bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩claim1:∀ {N : ℤ} (hN : N ≥ m), S (N + 2) = S N + (-1) ^ (N + 1) * (a ⟨N + 1, ⋯⟩ - a ⟨N + 2, ⋯⟩)claim2:∀ {N : ℤ}, N ≥ m → Odd N → S (N + 2) ≥ S Nclaim3:∀ {N : ℤ}, N ≥ m → Even N → S (N + 2) ≤ S Nwhy1:∀ {N : ℤ}, N ≥ m → Even N → ∀ (k : ℕ), S (N + 2 * ↑k) ≤ S Nwhy2:∀ {N : ℤ} (hN : N ≥ m), Even N → ∀ (k : ℕ), S (N + 2 * ↑k + 1) ≥ S N - a ⟨N + 1, ⋯⟩why3:∀ {N : ℤ}, N ≥ m → Even N → ∀ (k : ℕ), S (N + 2 * ↑k + 1) ≤ S (N + 2 * ↑k)claim4:∀ {N : ℤ} (hN : N ≥ m),
  Even N →
    ∀ (k : ℕ), S N - a ⟨N + 1, ⋯⟩ ≤ S (N + 2 * ↑k + 1) ∧ S (N + 2 * ↑k + 1) ≤ S (N + 2 * ↑k) ∧ S (N + 2 * ↑k) ≤ S NN:ℤn:ℤhN:N ≥ mh':Even Nhn:n ≥ N⊢ N + 1 ≥ m grindAll goals completed! 🐙 ⟩ ≤ S n ∧ S n ≤ S N := bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ (mk' fun n ↦ (-1) ^ ↑n * a n).converges ↔ Filter.Tendsto a Filter.atTop (nhds 0)
    sorryAll goals completed! 🐙
  have why5 {ε:ℝ} (hε: ε > 0) : ∃ N, ∀ n ≥ N, ∀ m ≥ N, |S n - S m| ≤ ε := bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ (mk' fun n ↦ (-1) ^ ↑n * a n).converges ↔ Filter.Tendsto a Filter.atTop (nhds 0) sorryAll goals completed! 🐙
  have : CauchySeq S := bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ (mk' fun n ↦ (-1) ^ ↑n * a n).converges ↔ Filter.Tendsto a Filter.atTop (nhds 0)
    rw [Metric.cauchySeq_iff']m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩claim1:∀ {N : ℤ} (hN : N ≥ m), S (N + 2) = S N + (-1) ^ (N + 1) * (a ⟨N + 1, ⋯⟩ - a ⟨N + 2, ⋯⟩)claim2:∀ {N : ℤ}, N ≥ m → Odd N → S (N + 2) ≥ S Nclaim3:∀ {N : ℤ}, N ≥ m → Even N → S (N + 2) ≤ S Nwhy1:∀ {N : ℤ}, N ≥ m → Even N → ∀ (k : ℕ), S (N + 2 * ↑k) ≤ S Nwhy2:∀ {N : ℤ} (hN : N ≥ m), Even N → ∀ (k : ℕ), S (N + 2 * ↑k + 1) ≥ S N - a ⟨N + 1, ⋯⟩why3:∀ {N : ℤ}, N ≥ m → Even N → ∀ (k : ℕ), S (N + 2 * ↑k + 1) ≤ S (N + 2 * ↑k)claim4:∀ {N : ℤ} (hN : N ≥ m),
  Even N →
    ∀ (k : ℕ), S N - a ⟨N + 1, ⋯⟩ ≤ S (N + 2 * ↑k + 1) ∧ S (N + 2 * ↑k + 1) ≤ S (N + 2 * ↑k) ∧ S (N + 2 * ↑k) ≤ S Nwhy4:∀ {N n : ℤ} (hN : N ≥ m), Even N → n ≥ N → S N - a ⟨N + 1, ⋯⟩ ≤ S n ∧ S n ≤ S Nwhy5:∀ {ε : ℝ}, ε > 0 → ∃ N, ∀ n ≥ N, ∀ m ≥ N, |S n - S m| ≤ ε⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (S n) (S N) < ε
    intro ε hεm:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩claim1:∀ {N : ℤ} (hN : N ≥ m), S (N + 2) = S N + (-1) ^ (N + 1) * (a ⟨N + 1, ⋯⟩ - a ⟨N + 2, ⋯⟩)claim2:∀ {N : ℤ}, N ≥ m → Odd N → S (N + 2) ≥ S Nclaim3:∀ {N : ℤ}, N ≥ m → Even N → S (N + 2) ≤ S Nwhy1:∀ {N : ℤ}, N ≥ m → Even N → ∀ (k : ℕ), S (N + 2 * ↑k) ≤ S Nwhy2:∀ {N : ℤ} (hN : N ≥ m), Even N → ∀ (k : ℕ), S (N + 2 * ↑k + 1) ≥ S N - a ⟨N + 1, ⋯⟩why3:∀ {N : ℤ}, N ≥ m → Even N → ∀ (k : ℕ), S (N + 2 * ↑k + 1) ≤ S (N + 2 * ↑k)claim4:∀ {N : ℤ} (hN : N ≥ m),
  Even N →
    ∀ (k : ℕ), S N - a ⟨N + 1, ⋯⟩ ≤ S (N + 2 * ↑k + 1) ∧ S (N + 2 * ↑k + 1) ≤ S (N + 2 * ↑k) ∧ S (N + 2 * ↑k) ≤ S Nwhy4:∀ {N n : ℤ} (hN : N ≥ m), Even N → n ≥ N → S N - a ⟨N + 1, ⋯⟩ ≤ S n ∧ S n ≤ S Nwhy5:∀ {ε : ℝ}, ε > 0 → ∃ N, ∀ n ≥ N, ∀ m ≥ N, |S n - S m| ≤ εε:ℝhε:ε > 0⊢ ∃ N, ∀ n ≥ N, dist (S n) (S N) < ε; choose N hN using why5 (half_pos hε)m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩claim1:∀ {N : ℤ} (hN : N ≥ m), S (N + 2) = S N + (-1) ^ (N + 1) * (a ⟨N + 1, ⋯⟩ - a ⟨N + 2, ⋯⟩)claim2:∀ {N : ℤ}, N ≥ m → Odd N → S (N + 2) ≥ S Nclaim3:∀ {N : ℤ}, N ≥ m → Even N → S (N + 2) ≤ S Nwhy1:∀ {N : ℤ}, N ≥ m → Even N → ∀ (k : ℕ), S (N + 2 * ↑k) ≤ S Nwhy2:∀ {N : ℤ} (hN : N ≥ m), Even N → ∀ (k : ℕ), S (N + 2 * ↑k + 1) ≥ S N - a ⟨N + 1, ⋯⟩why3:∀ {N : ℤ}, N ≥ m → Even N → ∀ (k : ℕ), S (N + 2 * ↑k + 1) ≤ S (N + 2 * ↑k)claim4:∀ {N : ℤ} (hN : N ≥ m),
  Even N →
    ∀ (k : ℕ), S N - a ⟨N + 1, ⋯⟩ ≤ S (N + 2 * ↑k + 1) ∧ S (N + 2 * ↑k + 1) ≤ S (N + 2 * ↑k) ∧ S (N + 2 * ↑k) ≤ S Nwhy4:∀ {N n : ℤ} (hN : N ≥ m), Even N → n ≥ N → S N - a ⟨N + 1, ⋯⟩ ≤ S n ∧ S n ≤ S Nwhy5:∀ {ε : ℝ}, ε > 0 → ∃ N, ∀ n ≥ N, ∀ m ≥ N, |S n - S m| ≤ εε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, ∀ m ≥ N, |S n - S m| ≤ ε / 2⊢ ∃ N, ∀ n ≥ N, dist (S n) (S N) < ε; use Nhm:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩claim1:∀ {N : ℤ} (hN : N ≥ m), S (N + 2) = S N + (-1) ^ (N + 1) * (a ⟨N + 1, ⋯⟩ - a ⟨N + 2, ⋯⟩)claim2:∀ {N : ℤ}, N ≥ m → Odd N → S (N + 2) ≥ S Nclaim3:∀ {N : ℤ}, N ≥ m → Even N → S (N + 2) ≤ S Nwhy1:∀ {N : ℤ}, N ≥ m → Even N → ∀ (k : ℕ), S (N + 2 * ↑k) ≤ S Nwhy2:∀ {N : ℤ} (hN : N ≥ m), Even N → ∀ (k : ℕ), S (N + 2 * ↑k + 1) ≥ S N - a ⟨N + 1, ⋯⟩why3:∀ {N : ℤ}, N ≥ m → Even N → ∀ (k : ℕ), S (N + 2 * ↑k + 1) ≤ S (N + 2 * ↑k)claim4:∀ {N : ℤ} (hN : N ≥ m),
  Even N →
    ∀ (k : ℕ), S N - a ⟨N + 1, ⋯⟩ ≤ S (N + 2 * ↑k + 1) ∧ S (N + 2 * ↑k + 1) ≤ S (N + 2 * ↑k) ∧ S (N + 2 * ↑k) ≤ S Nwhy4:∀ {N n : ℤ} (hN : N ≥ m), Even N → n ≥ N → S N - a ⟨N + 1, ⋯⟩ ≤ S n ∧ S n ≤ S Nwhy5:∀ {ε : ℝ}, ε > 0 → ∃ N, ∀ n ≥ N, ∀ m ≥ N, |S n - S m| ≤ εε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, ∀ m ≥ N, |S n - S m| ≤ ε / 2⊢ ∀ n ≥ N, dist (S n) (S N) < ε
    intro n hnhm:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩claim1:∀ {N : ℤ} (hN : N ≥ m), S (N + 2) = S N + (-1) ^ (N + 1) * (a ⟨N + 1, ⋯⟩ - a ⟨N + 2, ⋯⟩)claim2:∀ {N : ℤ}, N ≥ m → Odd N → S (N + 2) ≥ S Nclaim3:∀ {N : ℤ}, N ≥ m → Even N → S (N + 2) ≤ S Nwhy1:∀ {N : ℤ}, N ≥ m → Even N → ∀ (k : ℕ), S (N + 2 * ↑k) ≤ S Nwhy2:∀ {N : ℤ} (hN : N ≥ m), Even N → ∀ (k : ℕ), S (N + 2 * ↑k + 1) ≥ S N - a ⟨N + 1, ⋯⟩why3:∀ {N : ℤ}, N ≥ m → Even N → ∀ (k : ℕ), S (N + 2 * ↑k + 1) ≤ S (N + 2 * ↑k)claim4:∀ {N : ℤ} (hN : N ≥ m),
  Even N →
    ∀ (k : ℕ), S N - a ⟨N + 1, ⋯⟩ ≤ S (N + 2 * ↑k + 1) ∧ S (N + 2 * ↑k + 1) ≤ S (N + 2 * ↑k) ∧ S (N + 2 * ↑k) ≤ S Nwhy4:∀ {N n : ℤ} (hN : N ≥ m), Even N → n ≥ N → S N - a ⟨N + 1, ⋯⟩ ≤ S n ∧ S n ≤ S Nwhy5:∀ {ε : ℝ}, ε > 0 → ∃ N, ∀ n ≥ N, ∀ m ≥ N, |S n - S m| ≤ εε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, ∀ m ≥ N, |S n - S m| ≤ ε / 2n:ℤhn:n ≥ N⊢ dist (S n) (S N) < ε; rw [Real.dist_eq]hm:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩claim1:∀ {N : ℤ} (hN : N ≥ m), S (N + 2) = S N + (-1) ^ (N + 1) * (a ⟨N + 1, ⋯⟩ - a ⟨N + 2, ⋯⟩)claim2:∀ {N : ℤ}, N ≥ m → Odd N → S (N + 2) ≥ S Nclaim3:∀ {N : ℤ}, N ≥ m → Even N → S (N + 2) ≤ S Nwhy1:∀ {N : ℤ}, N ≥ m → Even N → ∀ (k : ℕ), S (N + 2 * ↑k) ≤ S Nwhy2:∀ {N : ℤ} (hN : N ≥ m), Even N → ∀ (k : ℕ), S (N + 2 * ↑k + 1) ≥ S N - a ⟨N + 1, ⋯⟩why3:∀ {N : ℤ}, N ≥ m → Even N → ∀ (k : ℕ), S (N + 2 * ↑k + 1) ≤ S (N + 2 * ↑k)claim4:∀ {N : ℤ} (hN : N ≥ m),
  Even N →
    ∀ (k : ℕ), S N - a ⟨N + 1, ⋯⟩ ≤ S (N + 2 * ↑k + 1) ∧ S (N + 2 * ↑k + 1) ≤ S (N + 2 * ↑k) ∧ S (N + 2 * ↑k) ≤ S Nwhy4:∀ {N n : ℤ} (hN : N ≥ m), Even N → n ≥ N → S N - a ⟨N + 1, ⋯⟩ ≤ S n ∧ S n ≤ S Nwhy5:∀ {ε : ℝ}, ε > 0 → ∃ N, ∀ n ≥ N, ∀ m ≥ N, |S n - S m| ≤ εε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, ∀ m ≥ N, |S n - S m| ≤ ε / 2n:ℤhn:n ≥ N⊢ |S n - S N| < ε; linarith [hN n hn N (bym:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Series := mk' fun n ↦ (-1) ^ ↑n * a nS:ℤ → ℝ := b.partialclaim0:∀ {N : ℤ} (hN : N ≥ m), S (N + 1) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩claim1:∀ {N : ℤ} (hN : N ≥ m), S (N + 2) = S N + (-1) ^ (N + 1) * (a ⟨N + 1, ⋯⟩ - a ⟨N + 2, ⋯⟩)claim2:∀ {N : ℤ}, N ≥ m → Odd N → S (N + 2) ≥ S Nclaim3:∀ {N : ℤ}, N ≥ m → Even N → S (N + 2) ≤ S Nwhy1:∀ {N : ℤ}, N ≥ m → Even N → ∀ (k : ℕ), S (N + 2 * ↑k) ≤ S Nwhy2:∀ {N : ℤ} (hN : N ≥ m), Even N → ∀ (k : ℕ), S (N + 2 * ↑k + 1) ≥ S N - a ⟨N + 1, ⋯⟩why3:∀ {N : ℤ}, N ≥ m → Even N → ∀ (k : ℕ), S (N + 2 * ↑k + 1) ≤ S (N + 2 * ↑k)claim4:∀ {N : ℤ} (hN : N ≥ m),
  Even N →
    ∀ (k : ℕ), S N - a ⟨N + 1, ⋯⟩ ≤ S (N + 2 * ↑k + 1) ∧ S (N + 2 * ↑k + 1) ≤ S (N + 2 * ↑k) ∧ S (N + 2 * ↑k) ≤ S Nwhy4:∀ {N n : ℤ} (hN : N ≥ m), Even N → n ≥ N → S N - a ⟨N + 1, ⋯⟩ ≤ S n ∧ S n ≤ S Nwhy5:∀ {ε : ℝ}, ε > 0 → ∃ N, ∀ n ≥ N, ∀ m ≥ N, |S n - S m| ≤ εε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, ∀ m ≥ N, |S n - S m| ≤ ε / 2n:ℤhn:n ≥ N⊢ N ≥ N simpAll goals completed! 🐙)]
  exact cauchySeq_tendsto_of_complete thisAll goals completed! 🐙

Example 7.2.13

noncomputable abbrev Series.example_7_2_13 : Series := (mk' (m:=1) (fun n ↦ (-1:ℝ)^(n:ℤ) / (n:ℤ)))

              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 := min a.m b.m
    seq n := a.seq n + b.seq n
    vanish n hn := bya:Seriesb:Seriesn:ℤhn:n < min a.m b.m⊢ a.seq n + b.seq n = 0 simp [a.vanish n (by omega), b.vanish n (by omega)]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
  change (a:Series).seq n + (b:Series).seq n = _seq.ha:ℕ → ℝb:ℕ → ℝn:ℤ⊢ { 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 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 ≥ 0posa:ℕ → ℝb:ℕ → ℝn:ℤh:n ≥ 0⊢ { 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 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 nnega:ℕ → ℝb:ℕ → ℝn:ℤh:¬n ≥ 0⊢ { 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 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 <;>posa:ℕ → ℝb:ℕ → ℝn:ℤh:n ≥ 0⊢ { 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 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 nnega:ℕ → ℝb:ℕ → ℝn:ℤh:¬n ≥ 0⊢ { 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 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]All goals completed! 🐙

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

theorem declaration uses `sorry`Series.convergesTo.add {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.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 ≥ 0posa:ℕ → ℝ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 nnega:ℕ → ℝ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 <;>posa:ℕ → ℝ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 nnega:ℕ → ℝ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! 🐙

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

theorem declaration uses `sorry`Series.convergesTo.smul {s:Series} {L c: ℝ} (hs: s.convergesTo L) :
    (c • s).convergesTo (c * L) := bys:SeriesL:ℝc:ℝhs:s.convergesTo L⊢ (c • s).convergesTo (c * L)
  sorryAll 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! 🐙

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

instance Series.inst_sub : Sub Series where
  sub a b := {
    m := min a.m b.m
    seq n := a.seq n - b.seq n
    vanish n hn := bya:Seriesb:Seriesn:ℤhn:n < min a.m b.m⊢ a.seq n - b.seq n = 0 simp [a.vanish n (by omega), b.vanish n (by omega)]All 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
  change (a:Series).seq n - (b:Series).seq n = _seq.ha:ℕ → ℝb:ℕ → ℝn:ℤ⊢ { 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 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 ≥ 0posa:ℕ → ℝb:ℕ → ℝn:ℤh:n ≥ 0⊢ { 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 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 nnega:ℕ → ℝb:ℕ → ℝn:ℤh:¬n ≥ 0⊢ { 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 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 <;>posa:ℕ → ℝb:ℕ → ℝn:ℤh:n ≥ 0⊢ { 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 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 nnega:ℕ → ℝb:ℕ → ℝn:ℤh:¬n ≥ 0⊢ { 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 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]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:ℤ))

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

theorem declaration uses `sorry`Series.converges_from (s:Series) (k:ℕ) : s.converges ↔ (s.from (s.m+k)).converges := bys:Seriesk:ℕ⊢ s.converges ↔ (s.from (s.m + ↑k)).converges
  sorryAll goals completed! 🐙

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! 🐙

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

theorem declaration uses `sorry`Series.shift {s:Series} {x:ℝ} (h: s.convergesTo x) (L:ℤ) :
    (mk' (m := s.m + L) (fun n ↦ s.seq (n - L))).convergesTo x := bys:Seriesx:ℝh:s.convergesTo xL:ℤ⊢ (mk' fun n ↦ s.seq (↑n - L)).convergesTo x
  sorryAll goals completed! 🐙

Lemma 7.2.15 (telescoping series) / Exercise 7.2.6

theorem declaration uses `sorry`Series.telescope {a:ℕ → ℝ} (ha: Filter.atTop.Tendsto a (nhds 0)) :
    ((fun n:ℕ ↦ a n - a (n+1)):Series).convergesTo (a 0) := bya:ℕ → ℝha:Filter.Tendsto a Filter.atTop (nhds 0)⊢ { m := 0, seq := fun n ↦ if n ≥ 0 then (fun n ↦ a n - a (n + 1)) n.toNat else 0, vanish := ⋯ }.convergesTo (a 0)
  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