跳轉到

08.1 微分#

本節目標#

  • 理解導數的極限定義 \(f'(x) = \lim_{h \to 0} \frac{f(x+h) - f(x)}{h}\) 。
  • 認識 Mathlib 中的 HasDerivAt 與 deriv 兩個核心概念。
  • 會用 deriv_pow、deriv_add 等引理做多項式微分。
  • 會用 HasDerivAt.comp 表達鏈鎖律。
  • 體會實務上的證明套路：simp 開路、ring 收尾。

導數的定義#

在標準微積分課程中，導數是用極限定義的：

\[ f'(x) = \lim_{h \to 0} \frac{f(x+h) - f(x)}{h} \]

幾何上， \(\frac{f(x+h) - f(x)}{h}\) 是過 \((x, f(x))\) 與 \((x+h, f(x+h))\) 的割線斜率， 當 \(h \to 0\) 時割線逼近切線，所以 \(f'(x)\) 就是切線斜率。

但在 Mathlib 中，你幾乎找不到這個極限的直接定義。原因很實際： \(\varepsilon\) - \(\delta\) 極限在證明中很難操作。Mathlib 採用的是一階近似（first-order approximation）的觀點：

定義：我們說 \(f'\) 是 \(f\) 在 \(x\) 處的導數，記作 HasDerivAt f f' x，若差商的 誤差在 \(h \to 0\) 時是線性小項，也就是存在一個函數 \(r\) 滿足

\[ f(x+h) = f(x) + f' \cdot h + r(h), \qquad \lim_{h \to 0} \frac{r(h)}{h} = 0 \]

這個定義與極限定義等價（Mathlib 中有引理銜接兩者），但它在代數操作上好用得多： 乘積法則、鏈鎖律都能直接用代數變換證出來，而不必搬弄極限。

Mathlib 的兩層架構：HasDerivAt 與 deriv#

Mathlib 把「可微」分成兩層：

  • HasDerivAt f f' x：命題層，說「 \(f'\) 是 \(f\) 在 \(x\) 處的導數」。證明時用。
  • deriv f x : 𝕜：函數層，直接取出導數的值。計算時用。

兩者由 HasDerivAt.deriv : HasDerivAt f f' x → HasDerivAt f (deriv f x) x 銜接。 另外 deriv f x 是用 Classical.choice 定義出來的：只要 \(f\) 在 \(x\) 可微， 就取那個唯一的 \(f'\) ；不可微時取 \(0\) （這是數學上無關緊要、但讓定義良定的選擇）。

open Real

-- 平方函數在任意點可微，且導數為 2x
example (x : ℝ) : HasDerivAt (fun y => y ^ 2) (2 * x) x := by
  hasDerivAt (x ^ 2) 2 x  -- Mathlib 的便利 tactic，本質是 mul_one 與 hasDerivAt_pow

上面用的是 Mathlib 提供的 hasDerivAt tactic；若要手寫，核心引理是 hasDerivAt_pow（或對整數指數的 HasDerivAt.pow）。

多項式微分#

多項式微分靠兩條引理組合：

open Real

example (a b : ℝ) (x : ℝ) : deriv (fun y => a * y + b) x = a := by
  simp [deriv_add]

example (x : ℝ) : deriv (fun y => y ^ 3 + 2 * y) x = 3 * x ^ 2 + 2 := by
  simp [deriv_add, deriv_pow]   -- simp 後通常已把 deriv 全部展開

常用引理一覽（命名都很好猜）：

引理 內容
deriv_id' \(\frac{d}{dx} x = 1\)
deriv_const \(\frac{d}{dx} c = 0\)
deriv_add \((f + g)' = f' + g'\)
deriv_mul \((fg)' = f'g + fg'\)
deriv_pow \(\frac{d}{dx} x^n = n \cdot x^{n-1}\)
deriv_const_mul \((cf)' = c \cdot f'\)

鏈鎖律#

鏈鎖律在 Mathlib 中是 HasDerivAt.comp：

theorem HasDerivAt.comp
    (hf : HasDerivAt f f' x) (hg : HasDerivAt g g' (f x)) :
    HasDerivAt (g ∘ f) (g' * f') x

注意乘法的順序是 \(g' \cdot f'\) （先外層後內層），這是因為 comp 把外層函數 g 寫在前面。複合函數在 Mathlib 中寫成 g ∘ f。

open Real

-- (x^2 + 1)^3 的導數是 3 * (x^2+1)^2 * 2x
example (x : ℝ) :
    HasDerivAt (fun y => (y ^ 2 + 1) ^ 3) (3 * (x ^ 2 + 1) ^ 2 * (2 * x)) x := by
  have h1 : HasDerivAt (fun y => y ^ 2 + 1) (2 * x) x := by
    have hpow : HasDerivAt (fun y => y ^ 2) (2 * x) x := by
      simpa using hasDerivAt_pow x 2
    exact hpow.add (hasDerivAt_const x 1)
  have h2 : HasDerivAt (fun u => u ^ 3) (3 * (x ^ 2 + 1) ^ 2) (x ^ 2 + 1) := by
    simpa using hasDerivAt_pow (x ^ 2 + 1) 3
  exact h2.comp h1

完整對照：求 \(x^2\) 的導數#

手算過程：

\[ \lim_{h \to 0} \frac{(x+h)^2 - x^2}{h} = \lim_{h \to 0} \frac{x^2 + 2xh + h^2 - x^2}{h} = \lim_{h \to 0} (2x + h) = 2x \]

Lean 對照：我們直接從定義出發，用 HasDerivAt 的展開形式證明。 Mathlib 提供引理 HasDerivAt.div_const 之餘，更根本的是可以直接構造 線性近似：

open Real

-- 目標：HasDerivAt (fun y => y ^ 2) (2 * x) x
example (x : ℝ) : HasDerivAt (fun y => y ^ 2) (2 * x) x := by
  -- 第一步（對應手算的展開）：代數恆等式 (x+h)^2 = x^2 + 2x*h + h*h
  have key : ∀ h : ℝ, (x + h) ^ 2 - x ^ 2 - (2 * x) * h = h * h := by
    intro h; ring
  -- 第二步（對應取極限）：h*h 除以 h 是 h，趨近 0
  exact HasDerivAt.of_isLittleOTVS
    (fun h => key h)  -- 誤差項恰好是 h*h
    (isLittleO_id' (fun _ => one_ne_zero) one_mul).congr_left (by fun_prop)

實務上沒有人這樣從定義硬寫；標準做法是呼叫 hasDerivAt tactic 或組合引理。 這個對照想傳達的重點是：手算中「展開後約去 \(h\) 」的那一步，在 Lean 中變成 一個純代數的 ring 恆等式，而「 \(h \to 0\) 時 \(h^2/h \to 0\) 」這件麻煩事被 封裝在 HasDerivAt 的定義裡。這正是 Lean 式數學的日常：把解析論證化約成代數。

實務建議：simp + ring 收尾#

計算型微積分目標（例如 deriv f x = 某式）的標準流程：

  1. 先 simp [deriv_add, deriv_pow, ...] 把 deriv 消化掉。
  2. 剩下的多是整式恆等式，用 ring 收尾。
  3. 有分式時用 field_simp 預處理，再 ring。
open Real

example (x : ℝ) (hx : x ≠ 0) : deriv (fun y => y / y ^ 2) x = -1 / x ^ 2 := by
  simp only [deriv_div]  -- (f/g)' = (f'g - fg')/g^2
  field_simp
  ring

遇到 simp 不動時，先用 deriv 的計算 lemma（derive tactic 也值得一試： derive 會自動搜尋可微性與導數公式），再回頭手動組 HasDerivAt 引理。

小結與練習#

本節要點：

  • 導數的極限定義在 Mathlib 中被 HasDerivAt 的「一階近似」定義取代，兩者等價。
  • HasDerivAt f f' x 是命題層（用來證明），deriv f x 是函數層（用來計算）。
  • 多項式微分 = deriv_add + deriv_pow；鏈鎖律 = HasDerivAt.comp。
  • 實務套路：simp 消導數、ring（或 field_simp + ring）收尾。

練習：

  1. 用 simp [deriv_add, deriv_pow] 證明：對任意 \(x : \mathbb{R}\) ， \(\frac{d}{dx}(x^4 - 3x) = 4x^3 - 3\) 。
  2. 用 HasDerivAt.comp 證明 \(\sin(x^2)\) 在任意點可微，並寫出 Lean 中的導數表達式 （提示：Real.hasDerivAt_sin）。
  3. 從定義層次重現本節的 \(x^2\) 對照：把 key 中的多項式換成 \((x+h)^3\) ， 證明 (x + h) ^ 3 - x ^ 3 - 3 * x ^ 2 * h = 3 * x * h ^ 2 + h ^ 3（ring 即可）， 並觀察誤差項仍是 \(O(h)\) 。
  4. 挑戰：證明 deriv (fun y => 1 / y) x = -1 / x ^ 2（提示：deriv_inv，需要 \(x \neq 0\) ）。