跳轉到

08.3 積分與微積分基本定理#

本節目標#

  • 回顧 Riemann 和的直覺，理解「面積」的逼近思想。
  • 誠實面對現代 Mathlib 的路線：積分以 Lebesgue 積分統一，Riemann 積分是特例。
  • 熟悉 \(\int x \text{ in } a..b, f x\) 記號與 IntervalIntegrable。
  • 掌握微積分基本定理（FTC）在 Mathlib 中的形態與用法。

Riemann 和的直覺#

想求曲線 \(y = f(x)\) 下方、區間 \([a, b]\) 之上的面積。把 \([a, b]\) 切成 \(n\) 小段， 每段上用一個矩形近似，矩形高的典型選擇是取樣點 \(f(x_i)\) ：

\[ \sum_{i=1}^{n} f(x_i) \, \Delta x, \qquad \Delta x = \frac{b-a}{n} \]

當 \(n \to \infty\) 、 \(\Delta x \to 0\) 時，若這些和收斂到同一極限，就稱之為 \(f\) 在 \([a, b]\) 上的 Riemann 積分 \(\int_a^b f(x)\, dx\) 。

傳統的 Riemann 積分有個著名痛點：收斂性理論破碎（什麼函數可積？極限與積分 何時可交換？需要一致收斂這類重砲）。Lebesgue 積分用「先測度後積分」的思路 徹底解決了這些問題，代價是入門門檻較高。

Mathlib 的誠實說明：Lebesgue 路線#

需要向讀者講清楚一件事：Mathlib 沒有獨立的 Riemann 積分理論當作主要接口。 它的積分是建立在測度論（MeasureTheory 命名空間）之上的 Lebesgue 積分：

  • 基礎：MeasureTheory.measure（測度）、MeasureTheory.integral（積分）。
  • 一維區間積分：IntervalIntegrable f μ a b 表示 \(f\) 在 \(a..b\) 上關於測度 \(\mu\) 可積；區間積分記號是
∫ x in a..b, f x    -- 即 intervalIntegral.integral f a b μ
  • Riemann 可積性與 Lebesgue 可積性的關係：在緊區間上有界且間斷點集測度為零的 函數（Riemann 可積函數）必 Lebesgue 可積，且積分值相等。所以你在數學分析課 學到的所有計算結果，在 Mathlib 的框架下依然成立。

這是「現代數學基礎化」的典型取捨：與其做兩套積分再證它們相容， 不如做一套最強的，把經典理論當作特例吸收進來。對初學者的副作用是： Mathlib 的積分引理偶爾帶有測度論的雜訊（如 μ = volume、a.e. 條件）， 本節會指出哪些雜訊可以用標準參數（volume、fun_prop）機械化地處理掉。

IntervalIntegrable 與基本計算#

區間積分位於 MeasureTheory.Integral.IntervalIntegral。常用的計算引理：

open MeasureTheory intervalIntegral Real

example (a b : ℝ) : ∫ x in a..b, (1 : ℝ) = b - a := by
  simp

example (a b c : ℝ) : ∫ x in a..b, c = c * (b - a) := by
  simp

example (a b : ℝ) (f g : ℝ → ℝ)
    (hf : IntervalIntegrable f volume a b) (hg : IntervalIntegrable g volume a b) :
    ∫ x in a..b, f x + g x = (∫ x in a..b, f x) + (∫ x in a..b, g x) :=
  intervalIntegral.integral_add hf hg

可積性通常不用手證：IntervalIntegrable.continuous（連續函數在緊區間可積）、 fun_prop tactic 能自動處理大部分情況。

微積分基本定理（FTC）#

FTC 有兩個方向：

第一部分（由導數算積分）：若 \(F' = f\) ，則

\[ \int_a^b f(x)\, dx = F(b) - F(a) \]

第二部分（由積分造原函數）：若 \(f\) 連續，則 \(F(x) = \int_a^x f(t)\, dt\) 可微且 \(F' = f\) 。

Mathlib 中第一部分的關鍵引理是：

-- Mathlib 實際引理（MeasureTheory/Interval/Integral 及 Analysis 目錄下）
theorem intervalIntegral.integral_eq_sub_of_hasDerivAt
    {f f' : ℝ → ℝ} {a b : ℝ} (hf : ∀ x ∈ Icc a b, HasDerivAt f (f' x) x)
    (hfb : IntervalIntegrable f' volume a b) :
    (∫ x in a..b, f' x) = f b - f a

這正是「原函數代入相減」的嚴格形式。條件的意義：

  • hf： \(f'\) 確實是 \(f\) 的導數（在整個閉區間上）。
  • hfb： \(f'\) 可積（連續函數自動滿足，IntervalIntegrable.continuous 或 fun_prop）。

注意：題目要求中提到的 intervalIntegral.integral_add 只是「積分的線性性」， 與 FTC 無關；FTC 的主角是 integral_eq_sub_of_hasDerivAt。 另外還有對稱的第二部分引理，如 intervalIntegral.deriv_integral_right / intervalIntegral.hasDerivAt_integral_right 一族（此家族的確切名稱 在 Mathlib 版本間有變動，建議用 exact? 查證）。

證明概觀#

FTC 第一部分的證明（Mathlib 的路線，非 Riemann 和的暴力路線）：

  1. 對任意分割 \(a = x_0 < x_1 < \cdots < x_n = b\) ，望遠鏡和：
\[ f(b) - f(a) = \sum_{i} \bigl( f(x_{i+1}) - f(x_i) \bigr) = \sum_i f'(c_i) \, (x_{i+1} - x_i) \]

中間那步用 MVT（第 8.2 節！）把每個差變成導數乘區間長。

  1. 右邊正是 \(f'\) 的 Riemann 和；當分割變細時它收斂到積分 （這裡用 Lebesgue 積分對緊區間上連續函數的逼近性質）。

  2. 於是 \(\int_a^b f' = f(b) - f(a)\) 。

看到了嗎？MVT 是 FTC 的引擎。這也解釋了為什麼 Mathlib 的 integral_eq_sub_of_hasDerivAt 與上一節的 exists_deriv_eq_slope 在同一個依賴鏈上。

Lean 使用示範#

open Real MeasureTheory intervalIntegral

-- 例 1：∫₀¹ x^2 dx = 1/3
example : (∫ x in (0 : ℝ)..1, x ^ 2) = 1 / 3 := by
  have key : ∀ x ∈ Icc (0 : ℝ) 1, HasDerivAt (fun y => y ^ 3 / 3) (x ^ 2) x := by
    intro x _
    have := hasDerivAt_pow x 3
    convert this.div_const 3 using 1
    field_simp
  have hI : IntervalIntegrable (fun x : ℝ => x ^ 2) volume 0 1 := by fun_prop
  -- FTC：導數的積分 = 原函數兩端相減
  simpa using integral_eq_sub_of_hasDerivAt key hI

-- 例 2：FTC 的一般形式（原函數代入相減）
example (a b : ℝ) (F f : ℝ → ℝ)
    (hF : ∀ x ∈ Icc a b, HasDerivAt F (f x) x)
    (hf : IntervalIntegrable f volume a b) :
    (∫ x in a..b, f x) = F b - F a :=
  integral_eq_sub_of_hasDerivAt hF hf

例 1 的流程值得記住：構造原函數 → 逐點驗證 HasDerivAt → 提供可積性 → 套 FTC → simp/ring 算兩端差。這就是 Lean 時代的「算積分」： 不是查積分表，而是構造反導函數。

小結與練習#

本節要點：

  • Riemann 和給出積分的直覺，但 Mathlib 以 Lebesgue 積分（MeasureTheory） 為統一基礎，經典結果作為特例保留。
  • 區間積分記號：∫ x in a..b, f x；可積性用 IntervalIntegrable， 連續函數自動可積（fun_prop 常能代勞）。
  • FTC 第一部分的主角是 intervalIntegral.integral_eq_sub_of_hasDerivAt； 其證明引擎是 MVT + 望遠鏡和。
  • 實務套路：構造原函數、驗 HasDerivAt、給可積性、套 FTC、simp 收尾。

練習：

  1. 計算 \(\int_0^1 (3x^2 + 2x) \, dx\) （答案： \(2\) ），完全仿照例 1 的四步驟。
  2. 證明 \(\int_a^b e^x \, dx = e^b - e^a\) （提示：Real.hasDerivAt_exp）。
  3. 用 integral_add 與第 1 題的結果，計算 \(\int_0^1 (x^2 + (3x^2 + 2x)) \, dx\) 。
  4. 查證你版本的 Mathlib 中 FTC 第二部分的引理名稱（搜尋 deriv_integral 或 hasDerivAt_integral），寫出其完整敘述並註明出處。