跳轉到

08.4 專案：Taylor 定理#

本節目標#

  • 敘述含 Lagrange 餘項的 Taylor 定理。
  • 理解其證明策略：對餘項函數反覆套用 Rolle 定理。
  • 在 Lean 中搭建可執行的骨架，並討論 Mathlib 相關設施 （HasFTaylorSeriesUpTo、IntervalIntegrable、多重可微的設定）。
  • 應用：用 \(e^x\) 與 \(\sin x\) 的泰勒多項式做函數逼近。

Taylor 定理#

設 \(f\) 在 \([a, b]\) 上有 \(n+1\) 階連續導數、在 \((a, b)\) 上有 \(n+1\) 階導數， \(x_0 \in [a, b]\) ， \(x \in [a, b]\) 、 \(x \neq x_0\) 。則存在 \(c\) 介於 \(x_0\) 與 \(x\) 之間，使

\[ f(x) = \sum_{k=0}^{n} \frac{f^{(k)}(x_0)}{k!} (x - x_0)^k + \frac{f^{(n+1)}(c)}{(n+1)!} (x - x_0)^{n+1} \]

最後一項稱為 Lagrange 餘項。 \(n = 0\) 的情形恰是 MVT（第 8.2 節）—— Taylor 定理可以看作 MVT 的高階推廣，這不是巧合，證明也正是同一套路。

證明策略：重複 Rolle#

經典證明（Cauchy 的構造）：

  1. 固定 \(x\) 與 \(x_0\) ，定義輔助函數
\[ g(t) = f(x) - \sum_{k=0}^{n} \frac{f^{(k)}(t)}{k!} (x - t)^k \]

它把「以 \(t\) 為展開點的 \(n\) 階泰勒多項式」從 \(f(x)\) 中扣掉。

  1. 直接計算可發現望遠鏡結構： \(g(x) = 0\) 、 \(g(x_0) = R_n\) （餘項）， 且 \(g'\) 恰好是 \(g\) 的同型表達式把 \(n\) 換成 \(n - 1\) 。

  2. 對 \(g\) 套 Rolle： \(g'\) 在 \(x\) 與 \(x_0\) 之間有零點；對 \(g'\) 再套 Rolle…… 反覆 \(n+1\) 次後，得到一點 \(c\) 使 \(g^{(n+1)}(c) = 0\) 。

  3. 解開 \(g^{(n+1)}(c) = 0\) ，就得到 \(R_n = \frac{f^{(n+1)}(c)}{(n+1)!}(x - x_0)^{n+1}\) 。

整個證明的引擎就是 Rolle 定理加代數望遠鏡——第 8.2、8.3 節的主題在此匯流。

Mathlib 的現狀：誠實說明#

在動手之前必須告訴讀者：Mathlib 對 Taylor 定理的正式化走的是「形式冪級數」 路線，核心設施是：

  • HasFTaylorSeriesUpTo n f F： \(f\) 擁有一個到 \(n\) 階的泰勒級數 \(F\) （ \(F\) 是一個把階數映到多重線性型序列的對象）。
  • AnalyticAt、taylorWithin 系列：解析函數的泰勒係數與收斂性。
  • Mathlib 中有「用泰勒多項式逼近」的結果（如 Convex.norm_le_of_taylor... 一類的餘項估計、AnalyticAt.taylor 系列），但一維 Lagrange 餘項形式 （如上節末尾的顯式 \(c\) ）並沒有以一個方便的引理直接提供。

因此本節的專案定位是：自己動手，把 Lagrange 餘項的骨架立起來。 這正是最好的練習——你會用上本章全部工具：HasDerivAt、Rolle、IntervalIntegrable。

骨架：逐步把 sorry 換成證明#

我們證 \(n = 0\) 的情形（即 MVT 的導數形式），這是完整定理的最小基因。 骨架如下；每一個 sorry 都標註了提示，讀者可依提示逐一填補。

open Real

/-- Lagrange 餘項的最小情形：f(x) = f(x₀) + f'(c)(x - x₀)。 -/
theorem taylor_lagrange_zero (f : ℝ → ℝ) (x₀ x : ℝ) (hx : x₀ < x)
    (hcont : ContinuousOn f (Icc x₀ x))
    (hdiff : ∀ t ∈ Ioo x₀ x, DifferentiableAt ℝ f t) :
    ∃ c ∈ Ioo x₀ x, f x = f x₀ + deriv f c * (x - x₀) := by
  -- 第一步：化約到 slope 形式，直接引用 MVT
  obtain ⟨c, hc, hcslope⟩ :=
    exists_slope_eq_deriv (fun t ht => (hdiff t ht).derivWithin (Ioo_diff _ _)) hx
  refine ⟨c, hc, ?_⟩
  -- 第二步：整理 slope 成 f x = f x₀ + f' c * (x - x₀)
  rw [slope, div_eq_iff (sub_ne_zero_of_ne (ne_of_lt hx))] at hcslope
  linarith [hcslope]

往上加階數時，核心輔助步驟是「輔助函數的導數具有望遠鏡結構」。 先在純代數層把它敲定：

open Real

-- 望遠鏡恆等式（代數層）：n = 1 時輔助函數導數的關鍵項
example (x t f₀ f₁ f₂ : ℝ) :
    deriv (fun s => f₀ + f₁ * (s - x) + f₂ * (s - x) ^ 2 / 2) t
      = f₁ + f₂ * (t - x) := by
  simp [deriv_add, deriv_pow]   -- 提示：deriv_pow、deriv_const_mul，最後 ring_nf
  ring

一般 \(n\) 時，把「多項式求導會把 \(\frac{f^{(k)}(t)}{k!}(x-t)^k\) 項轉化為 \(\frac{f^{(k+1)}(t)}{k!}(x-t)^k\) 與 \(\frac{f^{(k)}(t)}{(k-1)!}(x-t)^{k-1}\) 兩塊， 而這兩塊在總和中相鄰、恰好相消」這件事用 Finset.sum 的望遠鏡引理 （Finset.sum_range_succ' 一族）整理。這是骨架中最花工的部分，但每一步 都是純代數：simp、ring、sum_range 系列。

完整的遞迴結構如下（保留 sorry 的專案骨架）：

open Real

/-- 對可 n 次微分的 f，Lagrange 餘項定理（骨架版）。 -/
theorem taylor_lagrange (f : ℝ → ℝ) (n : ℕ) (x₀ x : ℝ) (hx : x₀ < x)
    (hdiff : ContDiffOn ℝ n f (Icc x₀ x))
    (hdiffO : ∀ t ∈ Ioo x₀ x, DifferentiableAt ℝ (iteratedDerivWithin n f) t) :
    ∃ c ∈ Ioo x₀ x,
      |f x - (∑ k in Finset.range (n + 1),
        (iteratedDerivWithin k f x₀) / (k.factorial : ℝ) * (x - x₀) ^ k)|
        ≤ |(iteratedDerivWithin (n + 1) f c) / ((n + 1).factorial : ℝ)| * (x - x₀) ^ (n + 1) := by
  sorry -- 第一步：n = 0 已在上面的定理完成；一般情形照「重複 Rolle」策略歸納

建議的攻關順序：

  1. 把 taylor_lagrange_zero 的每個 fun_prop / 化約步驟跑通（無 sorry）。
  2. 證 \(n = 1\) ：輔助函數 \(g(t) = f(x) - f(t) - f'(t)(x-t)\) ，計算 \(g(x_0) =\) 餘項、 \(g(x) = 0\) 、 \(g'(t) = -f''(t)(x - t)\) （這裡 ring 立大功）， 對 \(g\) 套 Rolle 再對 \(g'\) 套一次 Rolle 或 MVT。
  3. 一般 \(n\) ：歸納 + 望遠鏡和整理。若時間有限，至少完成到 \(n = 2\) ， 你就已經親手走完 Cauchy 證明的精華。

應用： \(e^x\) 與 \(\sin x\) 的逼近#

有了餘項估計，逼近論證的模式是固定的：

** \(e^x\) **： \(f^{(k)} = e^x\) 全相同，取 \(x_0 = 0\) 得

\[ e^x = \sum_{k=0}^{n} \frac{x^k}{k!} + \frac{e^c}{(n+1)!} x^{n+1} \]

當 \(x \in [0, 1]\) 時 \(e^c \le e < 3\) ，故餘項 \(\le \frac{3}{(n+1)!}\) ， 衰減極快。Mathlib 中 \(e^x\) 的級數表示是 Real.exp_eq_exp_ceil？ 正確引理是 Real.exp_eq_taylor_sum 一族（ \(e^x\) 的級數定義即泰勒級數， 見 Real.exp_series / Real.exp_eq_sum；以版本查證為準）。

** \(\sin x\) **：導數循環 \(\sin \to \cos \to -\sin \to -\cos \to \sin\) ， 故所有導數絕對值 \(\le 1\) ，餘項 \(\le \frac{|x|^{n+1}}{(n+1)!}\) —— 這正是 Mathlib 中 Real.sin_eq_sin_... 與 FormalMultilinearSeries 路線 共用的核心估計：對有界導數的函數，泰勒餘項由 \(|x|^{n+1}/(n+1)!\) 控制。 取 \(n = 5\) 、 \(x = 1\) ，誤差已小於 \(1/720\) ；這就是計算器算 \(\sin\) 的原理。

open Real

-- 骨架：n 階泰勒逼近的誤差控制（以 sin 為例）
example (n : ℕ) (x : ℝ) (hxb : |x| ≤ 1) :
    |sin x - (∑ k in Finset.range (2 * n + 2),
        (iteratedDerivWithin k sin 0) / (k.factorial : ℝ) * x ^ k)|
        ≤ 1 / ((2 * n + 2).factorial : ℝ) := by
  sorry -- 提示：|sin 的各階導數| ≤ 1 + Lagrange 餘項

專案反思#

  • 定理的層次感：Rolle → MVT → FTC → Taylor，每一層都以上一層為引擎。 在 Lean 中走一遍，比在紙上更清楚依賴方向。
  • Mathlib 的一般性代價：HasFTaylorSeriesUpTo 那套多重線性型設施 在高維無所不能，但對一維教學場景偏重。自己立一維骨架是合理的學習路徑， 也讓你體會「為什麼 Mathlib 要那樣設計」。
  • ** sorry 不是失敗**：把大定理切成能各自攻克的 sorry，是 Lean 專案的 標準工作流。每填掉一個，依賴圖就縮小一圈。
  • 版本意識：iteratedDerivWithin、taylorWithin、intervalIntegral 家族的名稱近兩年都有變動。本節引理名以 Mathlib 2024–2026 主線為準， 請養成用 exact?、Mathlib 文件站查證的習慣。

小結與練習#

本節要點：

  • Taylor 定理 = MVT 的高階版；Lagrange 餘項由「重複 Rolle + 望遠鏡代數」產生。
  • Mathlib 的 Taylor 設施走形式冪級數路線（HasFTaylorSeriesUpTo、AnalyticAt）， 一維 Lagrange 餘項值得自己立骨架。
  • 骨架工作流：最小情形（ \(n=0\) ）→ 望遠鏡恆等式 → 歸納補全。
  • 逼近應用的萬用模板：導數有界 \(\Rightarrow\) 餘項 \(\le \frac{M |x|^{n+1}}{(n+1)!}\) 。

練習：

  1. 完成 taylor_lagrange_zero 中被化約的細節，確保整段程式無 sorry 編譯通過。
  2. 證明 \(n = 1\) 的 Lagrange 餘項：對 \(g(t) = f(x) - f(t) - f'(t)(x - t)\) ，證 \(g'(t) = -f''(t)(x - t)\) （需 \(f\) 兩階可微），再套兩次 Rolle。
  3. 用 \(e^x\) 的餘項估計證明：對 \(x \in [0, 1]\) ， \(e\) 與 \(\sum_{k=0}^{10} \frac{1}{k!}\) 的差小於 \(\frac{3}{11!}\) 。
  4. 查證你的 Mathlib 版本中 HasFTaylorSeriesUpTo 的定義， 用一句話向自己解釋 \(F\ 0\) 、 \(F\ 1\) 各代表什麼。