08.2 均值定理#

本節目標#

• 敘述 Rolle 定理與均值定理（MVT），理解其幾何意義。
• 認識 Mathlib 敘述中 Convex 與 IsCompact 出現的緣由，並預告第 9 章的拓撲工具。
• 掌握 exists_deriv_eq_slope、exists_ratio_deriv_eq_ratio_slope 等 Mathlib 引理 （並註明命名隨版本演進的差異）。
• 學會 MVT 的兩大應用：單調性判定與不等式證明。

Rolle 定理#

Rolle 定理：設 \(f : [a, b] \to \mathbb{R}\) 連續、在 \((a, b)\) 上可微、且 \(f(a) = f(b)\) ，則存在 \(c \in (a, b)\) 使 \(f'(c) = 0\) 。

幾何意義：曲線起點與終點一樣高，途中必有一處切線水平（想像一顆上拋的球回到原高度， 最高點的速度必為零）。證明靠極值：閉區間上的連續函數必取得最大最小值， 若極值落在內部且可微，則該點導數為零。

Mathlib 中的版本（名稱為 exists_hasDerivAt_eq_zero，敘述以 IsRollean 結構 整理了「連續、內部可微、端點等值」三個條件）：

-- Mathlib（概念示意，實際敘述以你的 Mathlib 版本為準）
theorem exists_hasDerivAt_eq_zero {f : ℝ → ℝ} {a b : ℝ}
    (hf : IsRollean f a b) :
    ∃ x ∈ Ioo a b, HasDerivAt f 0 x

均值定理（MVT）#

把 Rolle 定理的曲線傾斜，就得到均值定理：

MVT：設 \(f\) 在 \([a, b]\) 連續、 \((a, b)\) 上可微，則存在 \(c \in (a, b)\) 使

幾何意義：曲線上總有一點的切線與連接兩端的割線平行。這是把「局部資訊（導數）」 轉換成「整體資訊（函數值差）」的橋樑，是分析學最重要的工具之一。

為什麼 Mathlib 的敘述裡有 Convex 與 IsCompact？#

Mathlib 追求最大一般性，其 MVT 敘述長這樣（Analysis.Calculus.MeanValue）：

-- Mathlib 實際引理（簡化註解版）
theorem exists_deriv_eq_slope {f : 𝕜 → F} {s : Set 𝕜} {x y : 𝕜}
    (hf : ContinuousOn f s)
    (hf' : ∀ z ∈ s, DifferentiableWithinAt 𝕜 f I z)   -- I = Icc x y 或 Ioo x y
    (hx : x ∈ s) (hy : y ∈ s) (hne : x ≠ y)
    (hs : Convex ℝ s) :
    ∃ z ∈ Ioo x y, HasDerivWithinAt f (slope f x y) I z

兩個看似多餘的條件，其實各有深意：

• Convex ℝ s：Mathlib 不想只對區間敘述 MVT，而想對任意凸集（例如 \(\mathbb{R}^n\) 中的球）敘述。凸集正是「連通且無洞」的正確高維推廣。 第 9 章我們會系統介紹凸性，這裡只需知道：對 \(\mathbb{R}\) 而言， Convex ℝ s 在 \(s\) 是區間時自動成立，可用 convex_Icc、convex_Ioo 等引理提供。
• IsCompact / ContinuousOn：Rolle 定理的證明需要「極值存在」，這依賴 閉區間的緊緻性（Heine–Borel）。Mathlib 把條件拆成 ContinuousOn f s 與區間本身的緊緻，而不是假設一個籠統的「 \(f\) 在 \([a,b]\) 上連續」。

這是本書反覆出現的主題：教科書敘述把拓撲性質打包成口語 （「閉區間上的連續函數」），Mathlib 把它們拆開成獨立的假設， 因為拆開才能自由組合與推廣。

Mathlib 的 MVT 引理群#

以下引理都在 Analysis.Calculus.MeanValue（注意：這些名稱在 Mathlib 歷史上 經歷過多次搬移與更名，例如早期有 exists_ratio_slope_eq_ratio_deriv 這類 寫法，後來統一成 exists_ratio_deriv_eq_ratio_slope；使用前請以 exact? 或 Mathlib 文件確認你的版本）：

slope 是 Mathlib 對割線斜率的命名：

slope f x y = (f y - f x) / (y - x)

應用一：單調性判定#

MVT 的經典推論：若 \(f' > 0\) ，則 \(f\) 嚴格遞增。Mathlib 中有現成引理 （位於 Analysis.Calculus.Monotone）：

-- 導數非負 ⟹ 單調（概念示意）
theorem MonotoneOn.of_deriv_nonneg (hf : ∀ x ∈ s, DifferentiableAt ℝ f x)
    (h : ∀ x ∈ s, 0 ≤ deriv f x) (hs : Convex ℝ s) : MonotoneOn f s

直觀地用 MVT 說明：對 \(a < b\) ，取 MVT 點 \(c\) ，則

因為 \(f'(c) \ge 0\) 且 \(b - a > 0\) 。整個論證只是把導數條件乘上一個正數—— 這在 Lean 中對應 mul_nonneg 一類的引理。

open Real

-- 骨架示範：證明 x ↦ x^3 在 ℝ 上嚴格遞增的關鍵步驟
example (a b : ℝ) (hab : a < b) (h : ∀ x, 0 ≤ deriv (fun y => y ^ 3) x) :
    a ^ 3 ≤ b ^ 3 := by
  -- 對區間 [a, b] 套 MVT 取得 z
  obtain ⟨z, hz, hz'⟩ :=
    exists_deriv_eq_slope (fun y => y ^ 3) (convex_Icc a b)
      (fun x _ => (differentiable_pow (n := 3)).differentiableAt |>.continuousAt
        |>.continuousOn) (by fun_prop) (by fun_prop) (by fun_prop) hab.ne
  -- 由 slope f a b = z 的導數值與非負條件推得 f a ≤ f b
  ...

實際操作時，單調性通常不必手展 MVT：直接用上面的 MonotoneOn.of_deriv_nonneg 一類引理，把「逐點導數非負」的證明交給 simp [deriv_pow] 即可。

應用二：不等式證明#

MVT 證不等式的模式：想證 \(f(x) \ge g(x)\) 對所有 \(x\) ，就令 \(h = f - g\) ， 證 \(h(0) = 0\) 且 \(h' \ge 0\) ，再由單調性收工。

以 \(e^x \ge 1 + x\) 為例。令 \(h(x) = e^x - 1 - x\) ，則 \(h(0) = 0\) 且 \(h'(x) = e^x - 1 \ge 0\) （因 \(e^x \ge 1\) 當 \(x \ge 0\) ），故 \(h\) 在 \([0, \infty)\) 遞增，於是 \(x \ge 0\) 時 \(h(x) \ge h(0) = 0\) 。至於 \(x < 0\) 的方向，可在 \([x, 0]\) 上套 MVT：

整理得 \(h(x) \ge 0\) 。Mathlib 中 \(e^x\) 的基本不等式也有現成結果，例如 Real.exp_ge_one_iff（ \(e^x \ge 1 \leftrightarrow x \ge 0\) ）， 以及凸函數切線不等式 ConvexOn.le_left_of_... 系列—— \(e^x\) 是凸函數， 而 \(1 + x\) 正是它在 \(x = 0\) 處的切線，這條路線我們在第 9 章講凸性時會走得更遠。

open Real

-- 概念骨架
example (x : ℝ) : exp x ≥ 1 + x := by
  rcases le_or_lt 0 x with hx | hx
  · -- 用單調性路線：exp - id 遞增且在 0 處為 0
    have hmono : MonotoneOn (fun y => exp y - 1 - y) (Ici 0) := by
      apply MonotoneOn.of_deriv_nonneg _ convex_Ici_0
      · intro y hy; fun_prop
      · intro y hy; simp [sub_add_eq]
    exact le_trans (le_of_eq (by ring : exp 0 - 1 - 0 = 0))
      (hmono (by simp [hx]) (le_refl 0)) |> by simpa using ·
  · sorry -- x < 0 的情形，練習完成

小結與練習#

本節要點：

• Rolle 定理是 MVT 的特例（ \(f(a) = f(b)\) ），MVT 是 Rolle 的仿射變形。
• Mathlib 敘述中的 Convex（推廣到高維、任意凸集）與 ContinuousOn （把緊緻性與連續性拆開）是大一般化的代價，也是第 9 章的主題預告。
• 核心引理：exists_deriv_eq_slope、exists_ratio_deriv_eq_ratio_slope、 exists_hasDerivAt_eq_zero；注意命名隨版本演進，查證優先。
• 兩大應用：導數符號判定單調性；「零點 + 導數符號」證不等式。

練習：

1. 證明：若 \(f\) 在 \([a,b]\) 連續、 \((a,b)\) 可微且 \(f' \equiv 0\) ，則 \(f\) 在 \([a,b]\) 上為常數（提示：對任意 \(x < y\) 套 MVT）。Mathlib 中對應引理是 deriv_zero_of_isOpen 與 IsOpen.eq_const_of_hasDerivAt 一族，試著找到並使用。
2. 用 MVT 證明 \(|\sin a - \sin b| \le |a - b|\) （ \(|\sin'| = |\cos| \le 1\) ）。
3. 完成 \(e^x \ge 1 + x\) 的 \(x < 0\) 情形（提示：Real.exp_pos）。
4. 查一查你的 Mathlib 版本中 exists_deriv_eq_slope 的完整敘述， 寫下一個能通過 type-check 的最小呼叫，練習與「版本差異」共處的能力。