7.2 序列極限#

本節目標#

• 掌握序列極限的 ε-N 定義，並理解每個量詞的意義。
• 認識 Mathlib 的 Tendsto（濾波器觀點，一句話簡介）與手寫 ε-N 的對照。
• 完整證明範例： \(1/n \to 0\) ，兩種寫法各一次。
• 證明極限的唯一性，並學會使用四則運算律（Tendsto.add 等）。
• 學會夾擠定理 tendsto_of_tendsto_of_tendsto_of_le_of_le。

ε-N 定義#

設 \((a_n)\) 是實數序列， \(L\) 是實數。我們說 \(a_n\) 收斂到 \(L\) （記作 \(\lim_{n \to \infty} a_n = L\) ），定義如下：

逐句解讀（第一次接觸 ε-N，量詞順序是全部的關鍵）：

• 「 \(\forall \varepsilon > 0\) 」：對手先出招——不管對手要求多小的誤差容許量 \(\varepsilon\) 。
• 「 \(\exists N\) 」：我們必須回應——找到一個門檻 \(N\) （可以依賴 \(\varepsilon\) ）。
• 「 \(\forall n \ge N,\ |a_n - L| < \varepsilon\) 」：門檻之後的所有項， 與 \(L\) 的距離都小於 \(\varepsilon\) 。

這是一場遊戲：對手給 \(\varepsilon\) ，我們給 \(N\) ；只要對手任意出招我們都能贏， 就收斂。注意 \(N\) 可以依賴 \(\varepsilon\) （ \(\varepsilon\) 越小 \(N\) 通常越大）， 但 \(N\) 不能依賴 \(n\) 。

用 Lean 直接寫出這個定義：

def SeqLimit (a : ℕ → ℝ) (L : ℝ) : Prop :=
  ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε

Mathlib 的 Tendsto：濾波器一句話#

Mathlib 中收斂的一般化概念叫 Tendsto：

#check @Tendsto
-- Tendsto : (α → β) → Filter α → Filter β → Prop

一句話解釋：Tendsto f F G 表示「把 \(f\) 沿著濾波器 \(F\) 推過去， 會落在濾波器 \(G\) 中」。對序列而言，取 \(F\) 為「尾段濾波器」 atTop（越來越靠後的 \(n\) 們）、 \(G\) 為 \(L\) 的鄰域濾波器 𝓝 L， 就得到：

-- 序列收斂：Tendsto a atTop (𝓝 L)
example (a : ℕ → ℝ) (L : ℝ) :
    Tendsto a atTop (𝓝 L) ↔
    ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - L| < ε :=
  Metric.tendsto_atTop

Metric.tendsto_atTop 正是把濾波器定義「翻譯」回 ε-N 語言的橋樑。 本書的策略：概念上用濾波器，計算上用 ε-N， 兩種寫法我們都要會。

範例： \(1/n \to 0\)#

數學證明。給定 \(\varepsilon > 0\) 。由 Archimedean 性質 （7.1 節！）取 \(N\) 使 \(1/\varepsilon < N\) ，即 \(1/N < \varepsilon\) 。 當 \(n \ge N\) 時 \(1/n \le 1/N < \varepsilon\) ，故 \(|1/n - 0| < \varepsilon\) 。 \(\blacksquare\)

寫法一：手寫 ε-N。

example : SeqLimit (fun n => 1 / (n + 1 : ℝ)) 0 := by
  intro ε hε
  obtain ⟨N, hN⟩ := exists_nat_gt (1 / ε)
  refine ⟨N, fun n hn => ?_⟩
  have hn' : (0 : ℝ) < n + 1 := by positivity
  have key : (1 : ℝ) / (n + 1) ≤ 1 / N := by
    apply div_le_div_right (by positivity)
    calc (0 : ℝ) < N := by positivity
    _   ≤ n         := hn
  rw [sub_zero]
  calc |1 / (n + 1) - 0| = 1 / (n + 1) := abs_of_nonneg (le_of_lt (div_pos one_pos hn'))
  _                     ≤ 1 / N        := key
  _                     < ε            := by
    rw [one_div_lt (by positivity) (by positivity)] at hN ⊢ <;> linarith

寫法二：用 Mathlib 的現成引理。

example : Tendsto (fun n : ℕ => 1 / ((n : ℝ) + 1)) atTop (𝓝 0) := by
  have : (fun n : ℕ => 1 / ((n : ℝ) + 1))
       = fun n : ℕ => ((n : ℝ) + 1)⁻¹ := by
    funext n; field_simp
  rw [this]
  exact tendsto_inv_atTop_zero <| tendsto_nat_cast_atTop_atTop (n := ℝ) |>.const_add_atTop 1

（確切的引理組合以 Mathlib 版本為準；例如也可從 tendsto_one_div_atTop 或 simpa using 出發。 實務上先用 exact? 搜尋，失敗再手寫 ε-N。）

觀察：寫法一告訴你「為什麼收斂」，寫法二告訴你「Mathlib 已經知道了」。 初學階段建議兩種都練：手寫一次建立直覺，再用庫加速。

極限的唯一性#

定理：若 \(a_n \to L\) 且 \(a_n \to M\) ，則 \(L = M\) 。

證明：反證。設 \(L \ne M\) ，令 \(\varepsilon = |L - M| / 2 > 0\) 。 由收斂性，存在 \(N_1\) 使 \(n \ge N_1\) 時 \(|a_n - L| < \varepsilon\) ， 存在 \(N_2\) 使 \(n \ge N_2\) 時 \(|a_n - M| < \varepsilon\) 。 取 \(n = \max(N_1, N_2)\) ，則

矛盾。 \(\blacksquare\)

在 Lean 中，唯一性由濾波器理論自動給出（濾波器極限本來就唯一）：

example (a : ℕ → ℝ) (L M : ℝ)
    (hL : Tendsto a atTop (𝓝 L)) (hM : Tendsto a atTop (𝓝 M)) : L = M :=
  tendsto_antisym' ... -- 實務上直接寫：

最直接的寫法是利用「極限是唯一的」這個一般事實：

example (a : ℕ → ℝ) (L M : ℝ)
    (hL : Tendsto a atTop (𝓝 L)) (hM : Tendsto a atTop (𝓝 M)) : L = M :=
  hL.unique hM

四則運算律#

收斂序列可以放心地做算術，這是極限理論的主力工具：

在 Mathlib 中，它們是 Tendsto.add、Tendsto.mul 等：

#check @Tendsto.add
#check @Tendsto.mul
#check @Tendsto.neg
#check @Tendsto.sub
#check @Tendsto.const_mul
#check @Filter.Tendsto.congr'

範例：證明 \(a_n = \frac{2n + 1}{n + 1} \to 2\) 。

數學上： \(\dfrac{2n+1}{n+1} = \dfrac{2 + 1/n}{1 + 1/n} \to \dfrac{2+0}{1+0} = 2\) 。

example : Tendsto (fun n : ℕ => (2 * (n : ℝ) + 1) / ((n : ℝ) + 1)) atTop (𝓝 2) := by
  have h1 : Tendsto (fun n : ℕ => 1 / ((n : ℝ) + 1)) atTop (𝓝 0) := by
    simpa using tendsto_one_div_atTop (fun n => ((n : ℝ) + 1)) (by positivity)
    -- 或以 7.2 前文的手寫引理代入
  have h2 : Tendsto (fun n : ℕ => 2 + 1 / ((n : ℝ) + 1)) atTop (𝓝 (2 + 0)) :=
    (tendsto_const_nhds.add h1)
  have h3 : Tendsto (fun n : ℕ => 1 + 1 / ((n : ℝ) + 1)) atTop (𝓝 (1 + 0)) :=
    (tendsto_const_nhds.add h1)
  have h4 : Tendsto (fun n : ℕ => (2 + 1 / ((n : ℝ) + 1)) / (1 + 1 / ((n : ℝ) + 1)))
      atTop (𝓝 ((2 + 0) / (1 + 0))) := h2.div h3 (by norm_num)
  -- 最後把函數改寫成同一個函數
  have : (fun n : ℕ => (2 * (n : ℝ) + 1) / ((n : ℝ) + 1))
       = fun n : ℕ => (2 + 1 / ((n : ℝ) + 1)) / (1 + 1 / ((n : ℝ) + 1)) := by
    funext n
    field_simp
    ring
  rw [this]
  simpa using h4

背後的原理值得一提：Tendsto.mul 之所以成立，是因為 乘法 \(x, y \mapsto xy\) 是連續函數（下一節主角！）—— 「收斂序列經過連續函數仍收斂」的特例。

夾擠定理#

定理（夾擠/squeeze）：若 \(b_n \to L\) 、 \(c_n \to L\) ， 且對足夠大的 \(n\) 恆有 \(b_n \le a_n \le c_n\) ，則 \(a_n \to L\) 。

直覺： \(a_n\) 被兩個都奔向 \(L\) 的序列從上下夾住，無路可逃。

Mathlib 中的形式（名字很長但完全對應）：

#check @tendsto_of_tendsto_of_tendsto_of_le_of_le
-- tendsto_of_tendsto_of_tendsto_of_le_of_le :
--   Tendsto f F (𝓝 b) → Tendsto g F (𝓝 b) → (∀ x, f x ≤ g x) → (∀ x, g x ≤ h x) →
--   Tendsto h F (𝓝 b)

範例：證明 \(\dfrac{\sin n}{n} \to 0\) 。 因為 \(-\dfrac{1}{n} \le \dfrac{\sin n}{n} \le \dfrac{1}{n}\) ， 而 \(\pm 1/n \to 0\) 。

example : Tendsto (fun n : ℕ => Real.sin (n : ℝ) / (n + 1 : ℝ)) atTop (𝓝 0) := by
  apply tendsto_of_tendsto_of_tendsto_of_le_of_le
    (b := (0 : ℝ)) <;> try exact tendsto_neg_neg ...
  -- 結構：下界序列 -1/(n+1) → 0，上界序列 1/(n+1) → 0，夾住
  sorry -- 細節：|sin n| ≤ 1 由 Real.sin_le_one 系列引理給出

（骨架如上；實作時拆成三個 have： 下界收斂、上界收斂、兩個不等式，再套用夾擠引理。）

夾擠定理在 Mathlib 中還有「最終不等式」版本 Tendsto.eventually_le、Filter.Eventually.tendsto_lt 等， 處理「只在 \(n\) 夠大時成立的條件」——這對應 ε-N 定義中 「 \(\exists N\) 之後」的精神：收斂只看尾巴，不在乎前面有限項。

小結與練習#

本節要點：

1. ε-N 定義是「對手給 \(\varepsilon\) 、我們給 \(N\) 」的遊戲；量詞順序不可交換。
2. Mathlib 用 Tendsto a atTop (𝓝 L) 表達收斂；Metric.tendsto_atTop 把它翻譯回 ε-N。
3. \(1/n \to 0\) 的證明用上 Archimedean 性質取 \(N\) 。
4. 極限唯一（Tendsto.unique）；四則運算 Tendsto.add / .mul / .div 是日常工具。
5. 夾擠定理 tendsto_of_tendsto_of_tendsto_of_le_of_le：被收斂序列夾住的序列也收斂。

練習：

1. 證明常數序列收斂：Tendsto (fun _ : ℕ => c) atTop (𝓝 c) （提示：tendsto_const_nhds，並手寫一次 ε-N 版本驗證）。
2. 用 ε-N 證明 \(a_n \to L \implies a_n \to L\) 的平移版本： 對任意 \(k : ℕ\) ，尾巴序列 \(a_{n+k}\) 也收斂到 \(L\) （「收斂只看尾巴」）。
3. 用 Tendsto.add 與 \(1/n \to 0\) 證明 \((3n+1)/(n+1) \to 3\) 。
4. 用夾擠定理證明 \(\frac{n}{n^2 + 1} \to 0\) 。
5. （挑戰）手寫 ε-N 證明：若 \(a_n \to L\) 且 \(a_n > 0\) 恆成立， 則 \(L \ge 0\) （提示：反證，取 \(\varepsilon = L/2\) ）。