7.4 級數與收斂判別#

本節目標#

理解級數即「部分和序列的極限」，把級數問題化約為 7.2 的序列極限。
認識 Mathlib 的 Summable 與 tsum。
完整證明幾何級數： \(\sum r^n = 1/(1-r)\) （當 \(|r| < 1\) ），含 Lean 敘述。
掌握比較判別法（comparison test）。
建立交錯級數的直覺，並寫出調和級數發散的 Lean 敘述。

級數即部分和序列的極限#

給定數列 \((a_n)\) ，級數 \(\sum_{n=0}^{\infty} a_n\) 的嚴格定義不是「無限加總」這個神祕動作，而是：

\[ \sum_{n=0}^{\infty} a_n \;=\; \lim_{N \to \infty} S_N, \qquad S_N = \sum_{n=0}^{N} a_n \]

其中 \(S_N\) 稱為部分和。級數收斂，就是序列 \(S_0, S_1, S_2, \dots\) 收斂—— 於是 7.2 的整套工具（唯一性、四則、夾擠）全部可以直接搬過來用。

在 Lean/Mathlib 中，無窮級數寫作 ∑' n, f n（tsum），「可加總」的性質是 Summable f：

#check @Summable
-- Summable f : Prop，定義為 (∑' n, f n) 存在（部分和收斂）

#check @summable_iff_hasSum
#check @hasSum
-- HasSum f a : 把 f 的值（可交換地）加總會得到 a

Summable f 與「部分和收斂」的橋樑：

-- Mathlib 對 ℕ 上的級數有直接的等價：
#check @Summable.tendsto_atTop_of_nat
-- 或：summable 與部分和 tendsto 的轉換引理
#check @Summable.tendsto_of_nat

（確切名稱依 Mathlib 版本而定；常用的是 Summable.tendsto_of_nat : Summable f → Tendsto (fun N => ∑ i ≤ N, f i) atTop (𝓝 (∑' i, f i))。）

重要觀念：Summable 比「項趨於零」強得多。項趨於零是收斂的必要條件（ \(a_n = S_n - S_{n-1} \to S - S = 0\) ），但絕不充分——調和級數就是反例（見後）。

幾何級數：完整證明#

定理：若 \(|r| < 1\) ，則

\[ \sum_{n=0}^{\infty} r^n = \frac{1}{1 - r} \]

數學證明。部分和有閉式：

\[ S_N = 1 + r + r^2 + \cdots + r^N = \frac{1 - r^{N+1}}{1 - r} \]

（驗證：兩邊同乘 \(1 - r\) ，右邊變 \(1 - r^{N+1}\) ，左邊中間項兩兩相消。）

因為 \(|r| < 1\) ， \(r^{N+1} \to 0\) （7.2 的夾擠： \(|r^{N+1}| = |r|^{N+1} \le |r| \cdot |r|^N\) ，或直接用指數衰減），故

\[ \lim_{N \to \infty} S_N = \frac{1 - 0}{1 - r} = \frac{1}{1 - r}. \qquad \blacksquare \]

Lean 敘述。Mathlib 有幾何級數的現成引理：

#check @summable_geometric_of_lt_one
-- summable_geometric_of_lt_one :
--   |r| < 1 → Summable (fun n : ℕ => r ^ n)

#check @tendsto_pow_atTop_nhds_0_of_lt_1
-- tendsto_pow_atTop_nhds_0_of_lt_1 : |r| < 1 → Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0)

#check @tsum_geometric_of_lt_one
-- tsum_geometric_of_lt_one : |r| < 1 → (∑' n : ℕ, r ^ n) = 1 / (1 - r)

於是定理的主敘述就是一行引用：

example (r : ℝ) (hr : |r| < 1) : (∑' n : ℕ, r ^ n) = 1 / (1 - r) :=
  tsum_geometric_of_lt_one hr

自己動手證一次（部分和路線），體會「級數 = 部分和極限」：

example (r : ℝ) (hr : |r| < 1) :
    Tendsto (fun N : ℕ => ∑ n ∈ Finset.range (N + 1), r ^ n) atTop (𝓝 (1 / (1 - r))) := by
  -- 部分和的閉式：∑_{n<N+1} r^n = (1 - r^(N+1)) / (1 - r)
  have hclosed : ∀ N : ℕ, ∑ n ∈ Finset.range (N + 1), r ^ n = (1 - r ^ (N + 1)) / (1 - r) := by
    intro N
    have hne : (1 : ℝ) - r ≠ 0 := by
      have : |r| < 1 := hr
      rintro rfl
      simp at this
    induction N with
    | zero => simp [hne]
    | succ N ih =>
      rw [Finset.sum_range_succ, ih]
      field_simp
      ring
  -- 極限計算：r^(N+1) → 0
  have hpow : Tendsto (fun N : ℕ => r ^ (N + 1)) atTop (𝓝 0) := by
    have := tendsto_pow_atTop_nhds_0_of_lt_1 (a := r) (by
      have := hr; simpa using this)
    simpa using this
  have : Tendsto (fun N : ℕ => (1 - r ^ (N + 1)) / (1 - r)) atTop
      (𝓝 ((1 - 0) / (1 - r))) := by
    apply Tendsto.div_const
    exact tendsto_const_nhds.sub (hpow)
  simp only [sub_zero] at this
  apply this.congr'
  filter_upwards [] with N
  rw [hclosed]

結構完全對應數學證明：先證閉式（歸納法），再取極限（r^{N+1} → 0），最後相除。r ≠ 1 的排除用到了 \(|r| < 1\) 。

比較判別法#

定理（比較判別法）：若 \(0 \le a_n \le b_n\) 對所有（或「最終」所有） \(n\) ，且 \(\sum b_n\) 收斂，則 \(\sum a_n\) 收斂。

直覺：小級數被收斂的大級數「壓住」，部分和單調遞增又有上界，只能收斂（這裡再次用到完備性——單調有界序列收斂）。

Mathlib 中的形式：

#check @Summable.of_nonneg_of_le
-- Summable.of_nonneg_of_le :
--   (∀ n, 0 ≤ f n) → (∀ n, f n ≤ g n) → Summable g → Summable f

example : Summable (fun n : ℕ => 1 / (2 ^ n * (n + 1 : ℝ))) := by
  refine Summable.of_nonneg_of_le (fun n => by positivity) (fun n => ?_) ?_
  · -- 1/(2ⁿ(n+1)) ≤ 1/2ⁿ
    rw [le_div_iff (by positivity)]
    nlinarith [pow_pos (2 : ℝ) n]
  · -- ∑ 1/2ⁿ 收斂（幾何級數，r = 1/2）
    have := summable_geometric_of_lt_one (r := (1 : ℝ) / 2) (by norm_num)
    simpa [one_div_pow] using this

應用節奏：拿到一個級數，先找一個「已知的」收斂或發散級數（幾何級數、p-級數）當比較對象，證明不等式，套引理。

交錯級數的直覺#

考慮符號正負交錯的級數，例如

\[ 1 - \frac{1}{2} + \frac{1}{3} - \frac{1}{4} + \cdots = \ln 2 \]

直覺：如果 \(a_n\) 單調遞減趨於 \(0\) ，交錯和 \(a_0 - a_1 + a_2 - a_3 + \cdots\) 的部分和會來回「鋸齒式」擺動，但每跨一步的幅度（ \(a_n\) ）越來越小，擺動被夾在越來越窄的區間裡——最終收斂。這是夾擠思想的離散版：偶數項部分和與奇數項部分和互相夾住。

Mathlib 中對應的工具是 Summable 的交錯級數判別（Leibniz 判別法），以及更一般的 HasSum 交錯求和引理：

#check @Summable.alternating_of_nonneg_of_antitone
-- 或以 tsum/alternating 系列搜尋；確切名稱依版本而定

（Leibniz 判別法在 Mathlib 中的形式與名稱隨版本演進，建議以 alternating 為關鍵字用 exact? 或 Mathlib 文件搜尋。思想不變：單調遞減 + 趨零 + 交錯 ⟹ 收斂。）

交錯級數還有一個好性質：誤差可控。取到第 \(N\) 項為止，誤差不超過第 \(N+1\) 項的大小—— 這讓交錯級數成為實際計算（如計算 \(\ln 2\) 、 \(\pi/4\) ）的利器。

調和級數發散#

\[ \sum_{n=1}^{\infty} \frac{1}{n} = 1 + \frac12 + \frac13 + \frac14 + \cdots = \infty \]

雖然 \(1/n \to 0\) （必要條件滿足！），級數仍然發散。 Oresme 的經典證明：按 2 的冪次分組——

\[ \frac12 \le \frac12,\qquad \frac14 + \frac14 \le \frac13 + \frac14,\qquad \frac18 \times 4 \le \frac15 + \cdots + \frac18 \]

每組的和都 \(\ge 1/2\) ，而組有無窮多個，故部分和無界。

Lean 敘述：

#check @not_summable_nat_cast_inv
-- 或：harmonic 系列引理
example : ¬ Summable (fun n : ℕ => (1 : ℝ) / (n + 1)) := by
  intro h
  exact not_summable_nat_cast_inv ℝ h   -- 名稱以 Mathlib 為準

Mathlib 對 \(\sum 1/n\) （用 n + 1 或 n.cast 的形式）提供發散引理；若引理簽記不同，可自行用分組論證：假設 Summable，則部分和有界，但顯式構造 \(N = 2^k\) 使部分和 \(\ge 1 + k/2\) ，與 Archimedean 性質矛盾。

教訓： \(a_n \to 0\) 離收斂很遠。比較判別法的另一面（ \(a_n \ge c/n\) 型的下界比較）正是證明發散的武器。

小結與練習#

本節要點：

級數收斂 = 部分和序列收斂；Lean 中以 Summable / tsum 表達。
幾何級數 \(\sum r^n = 1/(1-r)\) （ \(|r|<1\) ）：部分和閉式 + r^n → 0 + 四則運算律； Mathlib 引理 summable_geometric_of_lt_one、tsum_geometric_of_lt_one。
比較判別法 Summable.of_nonneg_of_le：用已知級數夾住未知級數。
交錯級數：單調遞減趨零 + 正負交錯 ⟹ 鋸齒式夾逼收斂，誤差可控。
調和級數 \(\sum 1/n\) 發散：項趨零不是充分條件；Oresme 分組證明。

練習：

證明 \(\sum_{n=0}^{\infty} 2^{-n} = 2\) （提示：tsum_geometric_of_lt_one 代入 \(r = 1/2\) ，norm_num 收尾）。
用比較判別法證明 \(\sum \frac{1}{n^2 + n}\) 收斂（比較對象： \(\frac{1}{n^2}\) 或 \(\frac{1}{n(n+1)}\) ，後者其實有閉式可算）。
用 ε-N 語言寫出「級數 \(\sum a_n\) 收斂」的定義（把 7.2 的定義套在 \(S_N\) 上），並說明 Cauchy 準則版本：收斂 \(\iff\) \(\forall \varepsilon > 0\ \exists N\ \forall m > n \ge N,\ |\sum_{k=n+1}^{m} a_k| < \varepsilon\) 。
證明：若 \(\sum a_n\) 收斂則 \(a_n \to 0\) （提示： \(a_n = S_n - S_{n-1}\) ，用 Tendsto.sub）。
（挑戰）仿照 Oresme 論證，在 Lean 中證明調和級數的部分和 \(S_{2^k} \ge 1 + k/2\) （可用歸納法），從而推出發散。
（預習）計算 \(\sum_{n=1}^{\infty} \frac{(-1)^{n+1}}{n}\) 的前幾個部分和，驗證「鋸齒式夾逼」的直覺，並思考誤差界 \(|S - S_N| \le a_{N+1}\) 為何成立。