第13章积分与测度论 - 深度伴读

本章定位

本章是教程的最高级章节，核心内容：

一元积分：区间积分、微积分基本定理、卷积

测度论：σ-代数、测度、几乎处处

Bochner 积分：Banach 空间值函数的积分

积分定理：控制收敛、Fubini、变量替换

Mathlib 使用Bochner 积分，统一处理实值积分和向量值积分。

13.1 一元积分

核心洞见

区间积分用 ∫ x in a..b, f x。[[a, b]] 自动处理 a,b 大小关系。

13.1.1 基本积分

open intervalIntegral
open Interval  -- [[a, b]] = [min a b, max a b]
 
-- 幂函数积分
example (a b : ℝ) : (∫ x in a..b, x) = (b ^ 2 - a ^ 2) / 2 := integral_id
 
-- 1/x 的积分
example {a b : ℝ} (h : (0 : ℝ) ∉ [[a, b]]) : (∫ x in a..b, 1 / x) = Real.log (b / a) :=
  integral_one_div h

[[a, b]] vs [a, b]

[[a, b]] 是 Icc (min a b) (max a b)，确保积分区间方向无关。若 a > b，则 ∫ x in a..b, f x = -∫ x in b..a, f x。

13.1.2 微积分基本定理

-- 第一基本定理：积分上限函数的导数
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'

13.1.3 卷积

open Convolution
 
example (f : ℝ → ℝ) (g : ℝ → ℝ) : f ⋆ g = fun x ↦ ∫ t, f t * g (x - t) :=
  rfl

13.2 测度论

核心洞见

测度 = 集合的”大小”。Mathlib 中测度对所有集合有定义，非可测集取为可测覆盖的下确界。

13.2.1 σ-代数与可测空间

variable {α : Type*} [MeasurableSpace α]
 
-- 可测集公理
example : MeasurableSet (∅ : Set α) := MeasurableSet.empty
example : MeasurableSet (univ : Set α) := MeasurableSet.univ
example {s : Set α} (hs : MeasurableSet s) : MeasurableSet (sᶜ) := hs.compl
 
-- 可数并/交封闭（需要 Encodable 假设）
variable {ι : Type*} [Encodable ι]
 
example {f : ι → Set α} (h : ∀ b, MeasurableSet (f b)) : MeasurableSet (⋃ b, f b) :=
  MeasurableSet.iUnion h
 
example {f : ι → Set α} (h : ∀ b, MeasurableSet (f b)) : MeasurableSet (⋂ b, f b) :=
  MeasurableSet.iInter h

Encodable vs Countable

Encodable ι = 存在到 ℕ 的显式单射。比 Countable 强，但对证明可数运算封闭性足够。 ℕ 和 Fin n 都是 Encodable。

13.2.2 测度

open MeasureTheory Function
variable {μ : Measure α}
 
-- 测度对所有集合有定义（非可测集 = 可测覆盖的下确界）
example (s : Set α) : μ s = ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), μ t :=
  measure_eq_iInf s
 
-- 次可数可加性
example (s : ι → Set α) : μ (⋃ i, s i) ≤ ∑' i, μ (s i) :=
  measure_iUnion_le s
 
-- 可数不交并的可加性（需可测性假设）
example {f : ℕ → Set α} (hmeas : ∀ i, MeasurableSet (f i)) (hdis : Pairwise (Disjoint on f)) :
    μ (⋃ i, f i) = ∑' i, μ (f i) :=
  μ.m_iUnion hmeas hdis

测度值类型

μ s : ℝ≥0∞（扩展非负实数，含 ∞）。 ENNReal.toReal : ℝ≥0∞ → ℝ 把 ∞ 映射到 0。

13.2.3 几乎处处

-- "对 μ-几乎处处的 x，P x 成立"
example {P : α → Prop} : (∀ᵐ x ∂μ, P x) ↔ ∀ᶠ x in ae μ, P x := Iff.rfl
 
-- `ae μ` 是滤子，可用 Eventually 的所有操作
-- ∀ᵐ x ∂μ, P x ∧ Q x = (∀ᵐ x ∂μ, P x) ∧ (∀ᵐ x ∂μ, Q x)

两种记号等价

∀ᵐ x ∂μ, P x 是 ∀ᶠ x in ae μ, P x 的简写。前者更常见于测度论语境，后者更通用。

13.3 Bochner 积分

核心洞见

Bochner 积分 = Lebesgue 积分的推广，目标空间可以是任意 Banach 空间。非可积函数的积分定义为 0。

13.3.1 积分记号

open MeasureTheory
 
variable {α : Type*} [MeasurableSpace α] {μ : Measure α}
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : α → E}
 
-- 基本积分记号
∫ a, f a ∂μ        -- 关于测度 μ 的积分
∫ a, f a           -- 关于默认测度
∫ x in s, f x ∂μ   -- 在集合 s 上的积分

13.3.2 积分的基本性质

example {f g : α → E} (hf : Integrable f μ) (hg : Integrable g μ) :
    ∫ a, f a + g a ∂μ = ∫ a, f a ∂μ + ∫ a, g a ∂μ :=
  integral_add hf hg
 
example {s : Set α} (c : E) : ∫ x in s, c ∂μ = (μ s).toReal • c :=
  setIntegral_const c

Integrable 假设

大多数积分引理需要 Integrable f μ 假设。若 f 不可积，∫ a, f a ∂μ = 0（由定义）。

13.3.3 控制收敛定理

open Filter
 
example {F : ℕ → α → E} {f : α → E} (bound : α → ℝ)
    (hmeas : ∀ n, AEStronglyMeasurable (F n) μ)
    (hint : Integrable bound μ)
    (hbound : ∀ n, ∀ᵐ a ∂μ, ‖F n a‖ ≤ bound a)
    (hlim : ∀ᵐ a ∂μ, Tendsto (fun n : ℕ ↦ F n a) atTop (𝓝 (f a))) :
    Tendsto (fun n ↦ ∫ a, F n a ∂μ) atTop (𝓝 (∫ a, f a ∂μ)) :=
  tendsto_integral_of_dominated_convergence bound hmeas hint hbound hlim

控制收敛定理的条件

F n 几乎处处可测

存在可积控制函数 bound

F n 逐点收敛到 f

结论：积分与极限可交换

13.3.4 Fubini 定理

example {α : Type*} [MeasurableSpace α] {μ : Measure α} [SigmaFinite μ]
    {β : Type*} [MeasurableSpace β] {ν : Measure β} [SigmaFinite ν]
    (f : α × β → E) (hf : Integrable f (μ.prod ν)) :
    ∫ z, f z ∂ μ.prod ν = ∫ x, ∫ y, f (x, y) ∂ν ∂μ :=
  integral_prod f hf

SigmaFinite

[SigmaFinite μ] = 空间可表为可数个有限测度集合的并。 Lebesgue 测度和计数测度都是 σ-有限的。

13.3.5 一般卷积

open Convolution
 
variable {𝕜 : Type*} {G : Type*} {E : Type*} {E' : Type*} {F : Type*}
  [NormedAddCommGroup E] [NormedAddCommGroup E'] [NormedAddCommGroup F]
  [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 E'] [NormedSpace 𝕜 F]
  [MeasurableSpace G] [NormedSpace ℝ F] [CompleteSpace F] [Sub G]
 
-- 一般卷积：由连续双线性形式 L 定义
example (f : G → E) (g : G → E') (L : E →L[𝕜] E' →L[𝕜] F) (μ : Measure G) :
    f ⋆[L, μ] g = fun x ↦ ∫ t, L (f t) (g (x - t)) ∂μ :=
  rfl

13.3.6 变量替换（换元公式）

example {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure]
    {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
    {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E}
    (hs : MeasurableSet s)
    (hf : ∀ x : E, x ∈ s → HasFDerivWithinAt f (f' x) s x)
    (h_inj : InjOn f s) (g : E → F) :
    ∫ x in f '' s, g x ∂μ = ∫ x in s, |(f' x).det| • g (f x) ∂μ :=
  integral_image_eq_integral_abs_det_fderiv_smul μ hs hf h_inj g

换元公式的条件

BorelSpace E：σ-代数由开集生成

IsAddHaarMeasure μ：平移不变、紧集有限、开集正测度

HasFDerivWithinAt：在 s 内有 Fréchet 导数

InjOn f s：f 在 s 上单射

结论：Jacobian 行列式的绝对值作为权重

本章核心概念总结

概念	类型/记号	含义
可测空间	`[MeasurableSpace α]`	σ-代数结构
可测集	`MeasurableSet s`	s 属于 σ-代数
测度	`μ : Measure α`	集合 → ℝ≥0∞
几乎处处	`∀ᵐ x ∂μ, P x`	不满足的集测度为零
可积	`Integrable f μ`	强可测且范数积分有限
积分	`∫ a, f a ∂μ`	Bochner 积分
集合上积分	`∫ x in s, f x ∂μ`	限制在 s 上
控制收敛	`tendsto_integral_of_dominated_convergence`	积分与极限交换
Fubini	`integral_prod`	重积分换序
卷积	`f ⋆[L, μ] g`	一般卷积
Haar 测度	`IsAddHaarMeasure μ`	平移不变测度
换元	`integral_image_eq_integral_abs_det_fderiv_smul`	Jacobian 换元

全书总结

恭喜完成 Mathematics in Lean！

你已经系统掌握了：

Lean 4 基础：类型、函数、证明、tactic

逻辑与集合：命题逻辑、量词、集合运算

代数结构：幺半群、群、环、域、模、向量空间

层级结构：类型类继承、to_additive、bad diamond

线性代数：线性映射、子空间、商空间、矩阵、基、维数

拓扑学：滤子、度量空间、拓扑空间、紧致性

分析学：导数、积分、测度论

下一步：

在 Lean Zulip 社区交流

阅读 Mathlib 文档

尝试形式化自己的数学问题

为 Mathlib 贡献代码

关键学习策略

1. 积分证明模板

example {f : α → E} : ∫ a, f a ∂μ = ... := by
  -- 方式1：用基本性质
  rw [integral_add, integral_smul]
 
  -- 方式2：用控制收敛定理
  apply tendsto_integral_of_dominated_convergence
  · exact bound
  · exact hmeas
  · exact hint
  · exact hbound
  · exact hlim

2. 可测性证明模板

example {s : Set α} : MeasurableSet s := by
  -- 方式1：用可测集的运算封闭性
  apply MeasurableSet.iUnion
  intro i
  exact hmeas i
 
  -- 方式2：用 borel 可测性
  apply MeasurableSet.of_continuous
  exact hf

自测问题

Bochner 积分与 Lebesgue 积分有什么区别？

为什么 Mathlib 中测度对所有集合有定义？

∀ᵐ x ∂μ, P x 和 ∀ᶠ x in ae μ, P x 的关系？

控制收敛定理需要哪些条件？

Fubini 定理为什么需要 SigmaFinite？

换元公式中 Jacobian 行列式为什么取绝对值？

伴读文档 - 第13章完 全书伴读文档完结

我的博客

探索

Ch13 积分与测度论 - 深度伴读

第13章积分与测度论 - 深度伴读

13.1 一元积分

13.1.1 基本积分

13.1.2 微积分基本定理

13.1.3 卷积

13.2 测度论

13.2.1 σ-代数与可测空间

13.2.2 测度

13.2.3 几乎处处

13.3 Bochner 积分

13.3.1 积分记号

13.3.2 积分的基本性质

13.3.3 控制收敛定理

13.3.4 Fubini 定理

13.3.5 一般卷积

13.3.6 变量替换（换元公式）

本章核心概念总结

全书总结

关键学习策略

1. 积分证明模板

2. 可测性证明模板

关系图谱

目录

反向链接

我的博客

探索

Ch13 积分与测度论 - 深度伴读

第13章 积分与测度论 - 深度伴读

13.1 一元积分

13.1.1 基本积分

13.1.2 微积分基本定理

13.1.3 卷积

13.2 测度论

13.2.1 σ-代数与可测空间

13.2.2 测度

13.2.3 几乎处处

13.3 Bochner 积分

13.3.1 积分记号

13.3.2 积分的基本性质

13.3.3 控制收敛定理

13.3.4 Fubini 定理

13.3.5 一般卷积

13.3.6 变量替换（换元公式）

本章核心概念总结

全书总结

关键学习策略

1. 积分证明模板

2. 可测性证明模板

关系图谱

目录

反向链接

第13章积分与测度论 - 深度伴读