第12章微分学 - 深度伴读

本章定位

本章覆盖一元微积分和一般赋范空间中的微分：

一元微积分：HasDerivAt、deriv、中值定理

赋范空间：NormedAddCommGroup、NormedSpace、Banach 空间

连续线性映射：E →L[𝕜] F、算子范数

Fréchet 导数：HasFDerivAt、fderiv、ContDiff

反函数定理：局部逆映射

12.1 一元微分学

核心洞见

HasDerivAt f a x = f 在 x 处导数为 a。deriv f x 是取导数的函数，不可导时返回 0。

12.1.1 导数的定义

open Real
 
-- hasDerivAt_sin x : HasDerivAt sin (cos x) x，即 sin 在 x 处的导数是 cos x
-- 特别地，在 x = 0 处，cos 0 = 1，所以 sin 在 0 处的导数为 1
example : HasDerivAt sin 1 0 := by simpa using hasDerivAt_sin 0
 
-- sin 处处可导：对任意 x，hasDerivAt_sin x 给出 sin 在 x 处的导数为 cos x
example (x : ℝ) : DifferentiableAt ℝ sin x :=
  (hasDerivAt_sin x).differentiableAt
 
-- HasDerivAt 推出 deriv 的值
example {f : ℝ → ℝ} {x a : ℝ} (h : HasDerivAt f a x) : deriv f x = a :=
  h.deriv

deriv 在不可导点返回 0
example {f : ℝ → ℝ} {x : ℝ} (h : ¬DifferentiableAt ℝ f x) : deriv f x = 0 :=
  deriv_zero_of_not_differentiableAt h
这使得某些引理不需要可导假设！见 Rolle 定理。

12.1.2 导数法则

example {f g : ℝ → ℝ} {x : ℝ} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) :
    deriv (f + g) x = deriv f x + deriv g x :=
  deriv_add hf hg
 
-- simp 可自动计算简单导数
example : deriv (fun x : ℝ ↦ x ^ 5) 6 = 5 * 6 ^ 4 := by simp
example : deriv sin π = -1 := by simp

12.1.3 中值定理

-- Rolle 定理（无需可导假设！）
example {f : ℝ → ℝ} {a b : ℝ} (hab : a < b)
    (hfc : ContinuousOn f (Icc a b)) (hfI : f a = f b) :
    ∃ c ∈ Ioo a b, deriv f c = 0 :=
  exists_deriv_eq_zero hab hfc hfI
 
-- Lagrange 中值定理
example (f : ℝ → ℝ) {a b : ℝ} (hab : a < b)
    (hf : ContinuousOn f (Icc a b))
    (hf' : DifferentiableOn ℝ f (Ioo a b)) :
    ∃ c ∈ Ioo a b, deriv f c = (f b - f a) / (b - a) :=
  exists_deriv_eq_slope f hab hf hf'

Rolle 定理为什么不需要可导假设？

如果 f 在 (a,b) 内某点不可导，则 deriv f c = 0 自动成立（由定义）。如果 f 在端点不可导也没关系，因为定理只关心内部点。

12.1.4 微积分基本定理

open intervalIntegral
open Interval  -- 引入 [[a, b]] 记号 = [min a b, max a b]
 
-- 导数的积分（微积分第一基本定理）
-- integral_hasStrictDerivAt_right：若 f 连续，则 F(u) = ∫ₐᵘ f(x)dx 在 u=b 处严格可导，导数为 f(b)
example (f : ℝ → ℝ) (hf : Continuous f) (a b : ℝ) :
    deriv (fun u ↦ ∫ x : ℝ in a..u, f x) b = f b :=
  (integral_hasStrictDerivAt_right
    (hf.intervalIntegrable _ _) (hf.stronglyMeasurableAtFilter _ _) hf.continuousAt
  ).hasDerivAt.deriv
 
-- Newton-Leibniz 公式
example {f : ℝ → ℝ} {a b : ℝ} {f' : ℝ → ℝ}
    (h : ∀ x ∈ [[a, b]], HasDerivAt f (f' x) x)
    (h' : IntervalIntegrable f' volume a b) :
    (∫ y in a..b, f' y) = f b - f a :=
  integral_eq_sub_of_hasDerivAt h h'

[[a, b]] 记号

Interval [[a, b]] = [min a b, max a b]，确保无论 a,b 大小关系如何都正确。

12.2 赋范空间中的微分学

12.2.1 赋范群与赋范空间

variable {E : Type*} [NormedAddCommGroup E]
 
-- 范数公理
example (x : E) : 0 ≤ ‖x‖ := norm_nonneg x
example {x : E} : ‖x‖ = 0 ↔ x = 0 := norm_eq_zero
example (x y : E) : ‖x + y‖ ≤ ‖x‖ + ‖y‖ := norm_add_le x y
 
-- 赋范群自动是度量空间和拓扑空间
example : MetricSpace E := by infer_instance
example {X : Type*} [TopologicalSpace X] {f : X → E} (hf : Continuous f) :
    Continuous fun x ↦ ‖f x‖ := hf.norm

赋范向量空间：

variable [NormedSpace ℝ E]
 
example (a : ℝ) (x : E) : ‖a • x‖ = |a| * ‖x‖ := norm_smul a x
 
-- 有限维 ⇒ 完备（Banach 空间）
example [FiniteDimensional ℝ E] : CompleteSpace E := by infer_instance

非平凡赋范域：

example (𝕜 : Type*) [NontriviallyNormedField 𝕜] (x y : 𝕜) : ‖x * y‖ = ‖x‖ * ‖y‖ :=
  norm_mul x y
 
-- 存在范数大于 1 的元素（区别于平凡赋范）
example (𝕜 : Type*) [NontriviallyNormedField 𝕜] : ∃ x : 𝕜, 1 < ‖x‖ :=
  NormedField.exists_one_lt_norm 𝕜
 
-- 完备域上有限维空间完备
example (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Type*) [NormedAddCommGroup E]
    [NormedSpace 𝕜 E] [CompleteSpace 𝕜] [FiniteDimensional 𝕜 E] : CompleteSpace E :=
  FiniteDimensional.complete 𝕜 E

12.2.2 连续线性映射

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
 
-- 连续线性映射类型
example : E →L[𝕜] E := ContinuousLinearMap.id 𝕜 E
 
-- 自动 coercion 到函数
example (f : E →L[𝕜] F) : E → F := f
example (f : E →L[𝕜] F) : Continuous f := f.cont
example (f : E →L[𝕜] F) (x y : E) : f (x + y) = f x + f y := f.map_add x y
example (f : E →L[𝕜] F) (a : 𝕜) (x : E) : f (a • x) = a • f x := f.map_smul a x

算子范数：

variable (f : E →L[𝕜] F)
 
-- 基本估计
example (x : E) : ‖f x‖ ≤ ‖f‖ * ‖x‖ := f.le_opNorm x
 
-- 反向：若对所有 x 有 ‖f x‖ ≤ M ‖x‖，则 ‖f‖ ≤ M
example {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ x, ‖f x‖ ≤ M * ‖x‖) : ‖f‖ ≤ M :=
  f.opNorm_le_bound hMp hM

算子范数的几何

‖f‖ = sup {‖f x‖ / ‖x‖ | x ≠ 0}，即 f 的最大”伸缩率”。

12.2.3 Banach-Steinhaus 定理（一致有界原理）

open Metric
 
example {ι : Type*} [CompleteSpace E] {g : ι → E →L[𝕜] F}
    (h : ∀ x, ∃ C, ∀ i, ‖g i x‖ ≤ C) :
    ∃ C', ∀ i, ‖g i‖ ≤ C' := by
  -- 核心思路：用 Baire 纲定理
  let e : ℕ → Set E := fun n ↦ ⋂ i : ι, { x : E | ‖g i x‖ ≤ n }
  have hc : ∀ n : ℕ, IsClosed (e n) := sorry
  have hU : (⋃ n : ℕ, e n) = univ := sorry
  obtain ⟨m, x, hx⟩ : ∃ m, ∃ x, x ∈ interior (e m) := sorry
  -- ...
  sorry

12.2.4 渐近比较：大 O 与小 o

open Asymptotics
 
-- IsBigOWith：明确常数 C
example {α : Type*} {E : Type*} [NormedGroup E] {F : Type*} [NormedGroup F] (c : ℝ)
    (l : Filter α) (f : α → E) (g : α → F) :
    IsBigOWith c l f g ↔ ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖ :=
  isBigOWith_iff
 
-- 大 O
example {α E F : Type*} [NormedGroup E] [NormedGroup F]
    (l : Filter α) (f : α → E) (g : α → F) : f =O[l] g ↔ ∃ C, IsBigOWith C l f g :=
  isBigO_iff_isBigOWith
 
-- 小 o
example {α E F : Type*} [NormedGroup E] [NormedGroup F]
    (l : Filter α) (f : α → E) (g : α → F) : f =o[l] g ↔ ∀ C > 0, IsBigOWith C l f g :=
  isLittleO_iff_forall_isBigOWith
 
-- 渐近等价
example {α E : Type*} [NormedAddCommGroup E] (l : Filter α) (f g : α → E) :
    f ~[l] g ↔ (f - g) =o[l] g :=
  Iff.rfl

12.2.5 Fréchet 导数

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
 
-- HasFDerivAt：f 在 x₀ 处有 Fréchet 导数 f'
example (f : E → F) (f' : E →L[𝕜] F) (x₀ : E) :
    HasFDerivAt f f' x₀ ↔
      (fun x ↦ f x - f x₀ - f' (x - x₀)) =o[𝓝 x₀] fun x ↦ x - x₀ :=
  hasFDerivAtFilter_iff_isLittleO ..
 
-- fderiv：取导数（不可导时返回 0）
example (f : E → F) (f' : E →L[𝕜] F) (x₀ : E) (hff' : HasFDerivAt f f' x₀) :
    fderiv 𝕜 f x₀ = f' :=
  hff'.fderiv

Fréchet 导数的直觉

一元时：f(x₀ + h) ≈ f(x₀) + f'(x₀)·h 一般时：f(x₀ + h) ≈ f(x₀) + f'(h)，其中 f' 是连续线性映射。

高阶导数与光滑性：

-- n 阶导数（取值于多重线性映射）
example (n : ℕ) (f : E → F) : E → E[×n]→L[𝕜] F :=
  iteratedFDeriv 𝕜 n f
 
-- ContDiff 𝕜 n f = f 是 C^n 的
example (n : ℕ∞) {f : E → F} :
    ContDiff 𝕜 n f ↔
      (∀ m : ℕ, (m : WithTop ℕ) ≤ n → Continuous fun x ↦ iteratedFDeriv 𝕜 m f x) ∧
        ∀ m : ℕ, (m : WithTop ℕ) < n → Differentiable 𝕜 fun x ↦ iteratedFDeriv 𝕜 m f x :=
  contDiff_iff_continuous_differentiable

ℕ∞ = ℕ ∪ {∞}

ContDiff 𝕜 ⊤ f = C^∞（光滑函数） ContDiff 𝕜 ω f = 解析函数（ω : WithTop ℕ∞）

12.2.6 反函数定理

section LocalInverse
variable [CompleteSpace E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E}
 
-- 严格可导 + 导数是同构 ⇒ 局部逆存在
example (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) : F → E :=
  HasStrictFDerivAt.localInverse f f' a hf
 
-- 局部左逆
example (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) :
    ∀ᶠ x in 𝓝 a, hf.localInverse f f' a (f x) = x :=
  hf.eventually_left_inverse
 
-- 局部右逆
example (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) :
    ∀ᶠ x in 𝓝 (f a), f (hf.localInverse f f' a x) = x :=
  hf.eventually_right_inverse
 
-- 局部逆也可导
example (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) :
    HasStrictFDerivAt (HasStrictFDerivAt.localInverse f f' a hf)
      (f'.symm : F →L[𝕜] E) (f a) :=
  HasStrictFDerivAt.to_localInverse hf
end LocalInverse

HasStrictFDerivAt vs HasFDerivAt

HasStrictFDerivAt 更强，用于反函数/隐函数定理。在 ℝ 或 ℂ 上，ContDiff 蕴含 HasStrictFDerivAt。

12.2.7 更一般的可导性

-- 在集合内可导
#check HasFDerivWithinAt
 
-- 关于滤子可导（最一般）
#check HasFDerivAtFilter

本章核心概念总结

概念	类型/记号	含义
有导数	`HasDerivAt f a x`	f 在 x 处导数为 a
导函数	`deriv f x`	不可导时返回 0
可导	`DifferentiableAt ℝ f x`	存在导数
范数	`‖x‖`	赋范群中的范数
赋范空间	`[NormedSpace 𝕜 E]`	标量乘法保范数
Banach 空间	`[CompleteSpace E]`	完备的赋范空间
连续线性映射	`E →L[𝕜] F`	bundled，含连续性证明
算子范数	`‖f‖`	最小 Lipschitz 常数
大 O	`f =O[l] g`	`‖f‖ ≤ C·‖g‖` 最终
小 o	`f =o[l] g`	`‖f‖ ≤ ε·‖g‖` 对任意 ε>0 最终
Fréchet 导	`HasFDerivAt f f' x₀`	最佳线性逼近
取导数	`fderiv 𝕜 f x₀`	返回 `E →L[𝕜] F`
C^n	`ContDiff 𝕜 n f`	n 阶连续可导
C^∞	`ContDiff 𝕜 ⊤ f`	光滑
解析	`ContDiff 𝕜 ω f`	实/复解析
严格可导	`HasStrictFDerivAt`	用于反函数定理
局部逆	`HasStrictFDerivAt.localInverse`	反函数定理构造

关键学习策略

1. 证明函数可导的模板

example (f : ℝ → ℝ) (x : ℝ) : DifferentiableAt ℝ f x := by
  -- 方式1：用已知可导函数的复合
  simp [differentiableAt_id, differentiableAt_sin, differentiableAt_exp]
 
  -- 方式2：用 HasDerivAt
  have h : HasDerivAt f a x := ...
  exact h.differentiableAt

2. 计算导数的模板

example (f g : ℝ → ℝ) (x : ℝ) : deriv (f * g) x = deriv f x * g x + f x * deriv g x := by
  -- 需要可导假设
  apply deriv_mul
  · exact hf
  · exact hg

3. Fréchet 导数证明模板

example {f : E → F} {x₀ : E} : HasFDerivAt f f' x₀ := by
  rw [hasFDerivAtFilter_iff_isLittleO]
  -- 证明余项是小 o
  sorry

预告：第13章会学到什么

第13章进入积分与测度论：

Bochner 积分（Banach 空间值函数的积分）
σ-代数与可测空间
测度与几乎处处
控制收敛定理、Fubini 定理、变量替换

自测问题

deriv f x 在不可导点返回什么？这有什么好处？

为什么 NormedAddCommGroup 和 NormedSpace 要分开？

连续线性映射 E →L[𝕜] F 与线性映射 E →ₗ[𝕜] F 有什么区别？

Fréchet 导数与小 o 记号的关系是什么？

ContDiff 𝕜 ⊤ f 和 ContDiff 𝕜 ω f 有什么区别？

反函数定理需要什么条件？

伴读文档 - 第12章完

我的博客

探索

Ch12 微分学 - 深度伴读

第12章微分学 - 深度伴读

12.1 一元微分学

12.1.1 导数的定义

12.1.2 导数法则

12.1.3 中值定理

12.1.4 微积分基本定理

12.2 赋范空间中的微分学

12.2.1 赋范群与赋范空间

12.2.2 连续线性映射

12.2.3 Banach-Steinhaus 定理（一致有界原理）

12.2.4 渐近比较：大 O 与小 o

12.2.5 Fréchet 导数

12.2.6 反函数定理

12.2.7 更一般的可导性

本章核心概念总结

关键学习策略

1. 证明函数可导的模板

2. 计算导数的模板

3. Fréchet 导数证明模板

预告：第13章会学到什么

关系图谱

目录

反向链接

我的博客

探索

Ch12 微分学 - 深度伴读

第12章 微分学 - 深度伴读

12.1 一元微分学

12.1.1 导数的定义

12.1.2 导数法则

12.1.3 中值定理

12.1.4 微积分基本定理

12.2 赋范空间中的微分学

12.2.1 赋范群与赋范空间

12.2.2 连续线性映射

12.2.3 Banach-Steinhaus 定理（一致有界原理）

12.2.4 渐近比较：大 O 与小 o

12.2.5 Fréchet 导数

12.2.6 反函数定理

12.2.7 更一般的可导性

本章核心概念总结

关键学习策略

1. 证明函数可导的模板

2. 计算导数的模板

3. Fréchet 导数证明模板

预告：第13章会学到什么

关系图谱

目录

反向链接

第12章微分学 - 深度伴读