计量经济学的 Lean 路径

Hansen 定理如何接到 Mathlib

前几篇把 Lean 当成一般工具。本页转到本项目的对象：Bruce Hansen《Econometrics》(Hansen 2022年) 里那些「看起来只是线性代数和概率」的定理。它们在课堂上好写，在类型里会暴露测度、几乎处处与矩阵奇异性。社区仓库 lean-hansen-econometrics 是对照物；我们的差异化仍是中文 L1、实证数字，以及与 hansenEM 的章节对齐。不要整库 fork。

1 为什么计量比「习题集代数」硬

第 3 章的投影代数接近纯矩阵恒等式，Mathlib（Lean 的数学库）矩阵库足以支撑，适合作为第一条 L3（逻辑证书）。一离开代数，教材默认的背景就开始和库错位：

教材口吻 形式化时通常变成
\(E(Y\mid X)\) 子 σ-代数上的 condExp，等式多为几乎处处
「随机样本」 独立同分布（i.i.d., independent and identically distributed）随机元，要有测度空间
\((X'X)^{-1}X'Y\) 先规定 \(X'X\) 不可逆时估计量取何值
「正则条件」 可积、σ-有限、可测、矩
\(\sqrt{n}(\hat\beta-\beta)\to_d\) 依分布收敛的类型，外加 Cramér–Wold 等桥
「条件于 \(X\)」 条件测度 / 条件期望，与无条件定理不同

Deng 与 Shum 形式化概率讲义时的中心经验完全适用：Mathlib 追求一般性（Bochner 积分、Banach 值），教材追求可教的特殊情形，必须写 bridge (Deng 和 Shum 2026年)。

2 Mathlib 里已经有什么

条件期望的主接口是 MeasureTheory.condExp，记号 μ[f | m]：m 是原 σ-代数的子 σ-代数，\(f\) 取值于 Banach 空间。可积时它可积、强可测，并在 m-可测集上积分还原。还有 L¹ 上的连续线性映射版本。概率侧另有独立性、条件独立、部分核表示。

线性代数侧有向量空间、子空间、矩阵与有限维。普通最小二乘（OLS, Ordinary Least Squares）的投影 / 歼灭子，应尽量表示为幂等线性映射的代数，而不是从零定义「计量专用投影」。

缺口（随 Mathlib 版本变化，引用前查文档）通常在：教材形状的中心极限定理（CLT, Central Limit Theorem）数组、Edgeworth 展开、自助法高阶展开、弱工具局部渐近。这些不是「不能做」，而是 L3 成本比第 3 章高一个数量级。

3 社区 Hansen 项目可搬用的方法

以该仓库 README 为准（工具链 Lean 4.29.0 / Mathlib v4.29.0）：

  • 第 2–13 章有 Lean 模块并被根库导入；第 1、14–29 章多为 inventory（定理清单）。
  • 没有任何一章被标成覆盖所有小节、推导、例子与习题。
  • 分层：LinearAlgebraUtils / ProbabilityUtils / AsymptoticUtils 为可复用层；章文件给 Hansen 记号的薄包装。
  • 有限样本 OLS 三种全函数化：Base / Star / OrZero。
  • 第 11–13 章显式区分字面陈述、修正陈述、诊断性反例。
  • 工作顺序：抽原文 → inventory → 可复用依赖 → 先证底层 → 章表面包装 → 构建与审阅。

对我们：inventory 与对照表要学；Lean 源码按需对照，不进本 git。对外定理名与中文评注以我们自己的清单为准。

4 建议的定理次序

与方法页阶段 3–4 一致，但加上「Mathlib 友好度」。下图中 FWL 为 Frisch–Waugh–Lovell 定理，LOO 为 leave-one-out（逐一剔除），IV 为工具变量（Instrumental Variables），GMM 为广义矩方法（Generalized Method of Moments）。

flowchart TB
  a["第 3 章代数<br/>正规方程 / P,M / FWL / LOO"] --> b["第 2 章<br/>塔性质 / 正交 / 线性投影"]
  b --> c["第 4 章有限样本<br/>无偏性与方差（写清 i.i.d. 与满秩）"]
  c --> d["第 6–7 章渐近"]
  d --> e["第 12–13 章 IV / GMM"]

先做第 3 章一条链，例如 Frisch–Waugh–Lovell：假设与结论几乎是矩阵恒等式，L1 本仓库已有记号与 leave-one-out 笔记，可升格为定理级展开后再考虑 L3。

第 2 章虽然出现更早，但条件期望的几乎处处与可积性会拖慢第一条成功体验。教学上可以 L1 先写第 2 章，L3 仍从第 3 章破冰。

第 4 章无偏性看起来短，类型上要同时处理：随机设计还是固定设计、条件于 \(X\) 还是无条件、\(X'X\) 几乎处处可逆还是路径wise 可逆。inventory 必须先写清 Hansen 原文采用哪一种。

IV / GMM 放到能稳定复用渐近引理之后。弱工具、许多工具的极限是研究前沿与教材交界，更不宜作为学习项目的第一批目标。

5 条件期望：一处典型翻译

Hansen 第 2 章把条件期望函数（CEF, Conditional Expectation Function）当作最佳预测，并迅速进入线性投影。Lean 里一条可用的翻译策略：

  1. 底层调用 condExp（σ-代数版）。
  2. 定义 mX 为协变量生成的子 σ-代数（包装层）。
  3. 章表面定理写成 \(E(Y\mid X)\) 的 Hansen 记号，文档字符串指向原文编号。
  4. 塔性质、拉出性质、CEF 误差正交，优先引用 Mathlib，再写变量版包装。

若教材在有限矩条件下写点点等式，而库只给几乎处处（a.e., almost everywhere），对照表写「我们采用 a.e.」。这不是挑剔，是避免课堂上把零测集上的修改说成另一种估计量。

6 普通最小二乘（OLS）：可逆性不能假装看不见

板书写 \(\hat\beta=(X'X)^{-1}X'Y\) 时，满秩常常写在假设里，推导中再也不提。形式化必须选一种全函数化，否则估计量的类型在奇异点无定义，后面无法谈「对所有样本路径」。

与 lean-hansen 对齐的三种选择：

  • Base：假设 IsUnit (Xᵀ * X)（或等价满秩），定理干净，渐近里不好用。
  • Star：用 Matrix.nonsingInv（或同类），处处有定义，证明引擎走这条。
  • OrZero：奇异时规定估计量为 0，接近部分教材/程序的静默行为，适合对外包装。

L1 笔记应告诉学生：R 的 solve 在奇异时会报错或走数值伪逆，与哪一种 Lean 定义对应，本身就是教学点。

7 本仓库的落点

当前（教程阶段）只做这些：

  1. 用本栏目建立共同语言。
  2. 对准备动手的章写 inventory，Lean 目标列可空。
  3. 继续 L1；能算的恒等式走 L2。
  4. L3 另开独立 git 时，第一条链建议仍是第 3 章 FWL。

原文始终以 hansenEM/chapters_eng（或中文译本）为准。Agent 写证明前必须打开对应 .qmd，禁止只靠参数记忆生成「Hansen 定理」。

学习练习不要一上来就克隆整个 Hansen Lean 库。下一篇给出从 Natural Number Game 到 Mathlib 概率的顺序，以及本栏目以后如何加「实作笔记」。

参考文献

Deng, Shuo, 和 Kenneth Shum. 2026年. From Lecture Notes to Lean: Formalizing a Textbook on Probability Theory. https://arxiv.org/abs/2607.27298.
Hansen, Bruce. 2022年. Econometrics. Princeton University Press.