From bb342fc492f491e09a78ee57cba2027cb7a25e66 Mon Sep 17 00:00:00 2001 From: gaojie Date: Fri, 5 Jun 2026 17:37:50 +0800 Subject: [PATCH] =?UTF-8?q?docs(lean):=20=E6=96=B0=E5=A2=9E=20HOWTO=5FPROO?= =?UTF-8?q?F.md=20=E2=80=94=20LeJEPA=20Lean4=20=E8=AF=81=E6=98=8E=E8=BF=87?= =?UTF-8?q?=E7=A8=8B=E5=AE=8C=E6=95=B4=E6=8C=87=E5=8D=97?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 内容涵盖： - 为什么用 Lean4 做数学证明（vs 传统证明） - 项目结构与文件依赖关系 - axiom vs theorem 核心概念 - 5 个证明文件逐行走读（Hermite/Uniqueness/Approx/Dirichlet/Planning） - 关键 Mathlib 定理对照表 - 常用证明策略速查表（linarith/nlinarith/ring/field_simp 等） - 如何添加新定理的完整步骤 - 调试技巧与常见错误解决 --- .../lean/HOWTO_PROOF.md | 517 ++++++++++++++++++ 1 file changed, 517 insertions(+) create mode 100644 JEPA/lejepa-identifiability/lean/HOWTO_PROOF.md diff --git a/JEPA/lejepa-identifiability/lean/HOWTO_PROOF.md b/JEPA/lejepa-identifiability/lean/HOWTO_PROOF.md new file mode 100644 index 0000000..f13b9da --- /dev/null +++ b/JEPA/lejepa-identifiability/lean/HOWTO_PROOF.md @@ -0,0 +1,517 @@ +# LeJEPA Lean 4 证明过程 How-To + +> 本文档面向想要**理解、修改或扩展** LeJEPA 形式化证明的读者。 +> 从"为什么用 Lean"到"如何写一个新定理"，逐步讲解。 + +--- + +## 目录 + +1. [为什么用 Lean 4 做数学证明](#1-为什么用-lean-4-做数学证明) +2. [项目结构速览](#2-项目结构速览) +3. [核心概念：axiom vs theorem](#3-核心概念axiom-vs-theorem) +4. [定理 4.1 证明走读（Hermite.lean）](#4-定理-41-证明走读hermitelean) +5. [定理 4.2 证明走读（Uniqueness.lean）](#5-定理-42-证明走读uniquenesslean) +6. [命题 4.3 证明走读（Approx.lean）](#6-命题-43-证明走读approxlean) +7. [附录 C 证明走读（Dirichlet.lean）](#7-附录-c-证明走读dirichletlean) +8. [推论 4.5 证明走读（Planning.lean）](#8-推论-45-证明走读planninglean) +9. [常用 Lean 4 证明策略速查](#9-常用-lean-4-证明策略速查) +10. [如何添加新定理](#10-如何添加新定理) +11. [调试技巧](#11-调试技巧) + +--- + +## 1. 为什么用 Lean 4 做数学证明 + +### 传统数学证明的问题 + +论文中的数学证明依赖人类读者的直觉填补细节。例如"由 Mehler 公式显然有…"这类表述，实际上隐藏了大量步骤。 + +### Lean 4 的优势 + +``` +人类直觉证明 Lean 4 形式化证明 +───────────────── ───────────────────────────── +"显然 ρᵈ ≤ ρ" pow_le_self_of_pos_lt_one ρ hρ0 hρ1 d hd +"由求和不等式" Summable.tsum_le_tsum (fun d => ...) ... +"等号成立当且仅当线性" equality_forces_degree_one sw ρ hρ0 hρ1 ... +``` + +Lean 4 强制你**填补每一个逻辑跳跃**，编译通过即意味着证明无误。 + +### Mathlib 的作用 + +Mathlib 是 Lean 4 的数学库，包含： +- 实分析（`Mathlib.Analysis.*`） +- 内积空间（`Mathlib.Analysis.InnerProductSpace.*`） +- 无穷级数（`Mathlib.Topology.Algebra.InfiniteSum.*`） +- 线性代数（`Mathlib.LinearAlgebra.*`） + +LeJEPA 的证明大量复用 Mathlib 中已有的定理。 + +--- + +## 2. 项目结构速览 + +``` +lean/ +├── lakefile.lean # 构建配置，声明 Mathlib 依赖 +├── lean-toolchain # 固定 Lean 版本：v4.28.0 +├── lake-manifest.json # 锁定所有依赖的精确 commit +├── LeJEPA.lean # 顶层入口，import 所有子模块 +└── LeJEPA/ + ├── Hermite.lean # 定理 4.1：线性可识别性（主路径） + ├── Uniqueness.lean # 定理 4.2：高斯唯一性 + ├── Approx.lean # 命题 4.3：近似可识别性界 + ├── Dirichlet.lean # 附录 C：Dirichlet 能量替代证明 + ├── Planning.lean # 推论 4.5：规划等价 + ├── PropApprox.lean # 命题 4.3 辅助引理 + ├── ThmHermite.lean # 定理 4.1 辅助引理 + └── ThmDirichlet.lean # 附录 C 辅助引理 +``` + +### 依赖关系 + +``` +Hermite.lean ──────────────────────────────► 定理 4.1 + │ + ▼ +Uniqueness.lean ───────────────────────────► 定理 4.2 + │ + ▼ +Approx.lean ───────────────────────────────► 命题 4.3 + │ + ▼ +Dirichlet.lean ────────────────────────────► 附录 C（独立路径） +Planning.lean ─────────────────────────────► 推论 4.5 +``` + +--- + +## 3. 核心概念：axiom vs theorem + +### `theorem`（已验证） + +```lean +theorem pow_le_self_of_pos_lt_one (ρ : ℝ) (hρ0 : 0 < ρ) (hρ1 : ρ ≤ 1) + (d : ℕ) (hd : 1 ≤ d) : ρ ^ d ≤ ρ := by + calc ρ ^ d ≤ ρ ^ 1 := pow_le_pow_of_le_one (le_of_lt hρ0) hρ1 hd + _ = ρ := pow_one ρ +``` + +`theorem` 后面跟着 `:= by` 和完整的证明策略。Lean 会**机械地验证**每一步。 + +### `axiom`（公理化） + +```lean +axiom mehler_summability + (sw : SpectralWeights) (ρ : ℝ) (hρ0 : 0 < ρ) (hρ1 : ρ < 1) : + Summable (fun d => sw.w d * ρ ^ d) +``` + +`axiom` 是**无证明的假设**，用于： +1. Mathlib 中存在但接口不匹配的结论（如 Mehler 公式） +2. 需要测度论/概率论框架才能严格表述的结论 + +> ⚠️ axiom 不影响已验证定理的正确性，但意味着这些结论的严格性依赖于公理的正确性。 + +### `structure`（数据结构） + +```lean +structure SpectralWeights where + w : ℕ → ℝ -- 权重函数 + nonneg : ∀ d, 0 ≤ w d + zero_degree : w 0 = 0 + summable : Summable w + total_variance : ∑' d, w d = 1 +``` + +`structure` 将相关数据和约束打包，类似于数学中的"设 w 满足以下条件"。 + +--- + +## 4. 定理 4.1 证明走读（Hermite.lean） + +### 数学陈述 + +> 若 h : ℝⁿ → ℝⁿ 满足 h(z) ~ N(0,Iₙ) 且最小化对齐损失，则 h(z) = Uz，U ∈ O(n)。 + +### 证明链 + +``` +Mehler 公式（axiom） + ↓ +corr_i = Σ_d w_d ρᵈ（axiom: correlation_eq_spectral_sum） + ↓ +corr_i ≤ ρ（VERIFIED: correlation_le_rho） + ↓ +𝓛(h) ≥ 2(1-ρ)n（VERIFIED: loss_lower_bound） + ↓ +𝓛(h) = 2(1-ρ)n → 每个 corr_i = ρ（VERIFIED: Finset.sum_lt_sum） + ↓ +corr_i = ρ → w_d = 0 for d ≥ 2（VERIFIED: equality_forces_degree_one） + ↓ +h 是线性的（axiom: linear_of_degree_one） + ↓ +h 是正交的（axiom: orthogonal_of_gaussian_linear） +``` + +### 关键引理逐行解析 + +#### `correlation_le_rho`（相关性上界） + +```lean +theorem correlation_le_rho (sw : SpectralWeights) (ρ : ℝ) + (hρ0 : 0 < ρ) (hρ1 : ρ < 1) + (hsum : Summable (fun d => sw.w d * ρ ^ d)) : + ∑' d, sw.w d * ρ ^ d ≤ ρ := by + calc ∑' d, sw.w d * ρ ^ d + ≤ ∑' d, sw.w d * ρ := -- 逐项 w_d·ρᵈ ≤ w_d·ρ + hsum.tsum_le_tsum + (fun d => spectral_term_le sw ρ hρ0 (le_of_lt hρ1) d) + (summable_spectral_upper sw ρ) + _ = ρ := tsum_spectral_upper sw ρ -- Σ w_d·ρ = ρ（因为 Σ w_d = 1） +``` + +**关键 Mathlib 定理**： +- [`Summable.tsum_le_tsum`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Algebra/InfiniteSum/Order.html)：若逐项 f(d) ≤ g(d) 且两者可求和，则 Σf ≤ Σg +- [`tsum_mul_right`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Algebra/InfiniteSum/Ring.html)：Σ(a_d · c) = (Σ a_d) · c + +#### `equality_forces_degree_one`（等号强制线性） + +```lean +-- 反证法：假设存在 d₀ ≥ 2 使得 w_{d₀} > 0 +by_contra h +push_neg at h +obtain ⟨d₀, hd₀_ge, hd₀_ne⟩ := h +-- 在 d₀ 处有严格不等式：w_{d₀}·ρ^{d₀} < w_{d₀}·ρ +have hstrict : sw.w d₀ * ρ ^ d₀ < sw.w d₀ * ρ := ... +-- 由 tsum_lt_tsum：Σ w_d·ρᵈ < Σ w_d·ρ = ρ +-- 但假设 Σ w_d·ρᵈ = ρ，矛盾 +``` + +**关键 Mathlib 定理**： +- [`Summable.tsum_lt_tsum`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Algebra/InfiniteSum/Order.html)：若存在一项严格小且其余项 ≤，则 tsum 严格小 + +#### `hermite_identifiability`（主定理组装） + +```lean +theorem hermite_identifiability ... := by + -- Step 1: 每个相关性 ≤ ρ + have hcorr_le : ∀ i, enc.correlation i ≤ ρ := ... + -- Step 2: 最优时每个相关性 = ρ（反证：若某个 < ρ，则损失 > 2(1-ρ)n） + have hcorr_eq_rho : ∀ i, enc.correlation i = ρ := by + by_contra hne; push_neg at hne + obtain ⟨i₀, hi₀⟩ := hne + -- Finset.sum_lt_sum：一项严格小 → 总和严格小 → 损失严格大 + have hsum_lt : ∑ i, enc.correlation i < ∑ _i, ρ := + Finset.sum_lt_sum (fun i _ => hcorr_le i) ⟨i₀, ..., hi₀_lt⟩ + ... + -- Step 3: 相关性 = ρ → 度数集中在 1 + have hdeg : ∀ i d, 2 ≤ d → (enc.spectrum i).w d = 0 := ... + -- Step 4-5: 线性 + 正交（axiom） + obtain ⟨M, hM⟩ := linear_of_degree_one enc hdeg + obtain ⟨U, hU⟩ := orthogonal_of_gaussian_linear M hnorm_M + exact ⟨U, fun z => by rw [hM z, hU z]⟩ +``` + +--- + +## 5. 定理 4.2 证明走读（Uniqueness.lean） + +### 数学陈述 + +> 转移算子的第一个非常数特征函数是仿射的，当且仅当 p 是高斯分布。 + +### 核心代数步骤 + +```lean +-- SL 特征方程：K · score(z) · a = −ev·(az + b) +-- 目标：推出 score(z) = αz + β，其中 α < 0 + +theorem score_affine_of_eigenfunction + (lc : LatentComponent) (a b : ℝ) (ha : a ≠ 0) + (heigen : ∀ z, lc.K * lc.score z * a = -(lc.ev * (a * z + b))) : + ∃ (α β : ℝ), α < 0 ∧ (∀ z, lc.score z = α * z + β) := by + refine ⟨-(lc.ev / lc.K), -(lc.ev * b / (lc.K * a)), ?_, ?_⟩ + · -- α = −ev/K < 0（因为 ev > 0, K > 0） + have := div_pos lc.hev lc.hK; linarith + · -- 代数化简：从特征方程解出 score(z) + intro z + have hKa_ne : lc.K * a ≠ 0 := mul_ne_zero (ne_of_gt lc.hK) ha + have h1 : lc.score z = -(lc.ev * (a * z + b)) / (lc.K * a) := by + field_simp at h ⊢; linarith + rw [h1]; field_simp; ring +``` + +**关键策略**： +- `field_simp`：自动化简含除法的等式（需要非零条件） +- `ring`：纯代数恒等式验证 +- `linarith`：线性算术推理 + +--- + +## 6. 命题 4.3 证明走读（Approx.lean） + +### 数学陈述 + +> 𝔼[‖h(z) − Qz‖²] ≤ D + (ε + D)²，其中 D = δ/(2ρ(1−ρ)) + +### 四步证明结构 + +``` +Step 1: 谱间隙控制非线性能量 + δ ≥ 2ρ(1−ρ)·W_nl → W_nl ≤ D + +Step 2: 极分解给出线性偏差 + ‖M−Q‖ ≤ ε + W_nl → ‖M−Q‖² ≤ (ε+W_nl)² + +Step 3: Pythagorean 分解（axiom） + total_error = ‖M−Q‖² + W_nl + +Step 4: 单调性 + W_nl ≤ D → (ε+W_nl)²+W_nl ≤ (ε+D)²+D +``` + +### `nonlinear_energy_le_D`（Step 1） + +```lean +theorem nonlinear_energy_le_D + (ρ δ W_nl : ℝ) (hρ0 : 0 < ρ) (hρ1 : ρ < 1) + (hgap : δ ≥ 2 * ρ * (1 - ρ) * W_nl) : + W_nl ≤ δ / (2 * ρ * (1 - ρ)) := by + have hsgap : (0 : ℝ) < 2 * ρ * (1 - ρ) := two_spectral_gap_pos ρ hρ0 hρ1 + rw [le_div_iff₀ hsgap] -- W_nl ≤ δ/c ↔ W_nl·c ≤ δ（c > 0） + linarith +``` + +### `bound_monotone`（Step 4） + +```lean +theorem bound_monotone (ε W_nl D : ℝ) + (hle : W_nl ≤ D) : + (ε + W_nl) ^ 2 + W_nl ≤ (ε + D) ^ 2 + D := by + have h1 : ε + W_nl ≤ ε + D := by linarith + nlinarith [sq_nonneg (ε + D - ε - W_nl)] + -- nlinarith 处理非线性算术：(ε+D)²-(ε+W_nl)² = (D-W_nl)(2ε+D+W_nl) ≥ 0 +``` + +**关键策略**： +- `le_div_iff₀`：将 `a ≤ b/c`（c > 0）转化为 `a*c ≤ b` +- `nlinarith`：非线性算术推理，可处理平方项 + +--- + +## 7. 附录 C 证明走读（Dirichlet.lean） + +### 数学陈述 + +> C¹ 微分同胚 + 保高斯测度 + 正交 Jacobian → h(z) = Uz + +### 证明链（Step 3-6 已验证） + +``` +正交 Jacobian（假设） + ↓ +h 是 1-Lipschitz（MVT，VERIFIED） + ↓ +h⁻¹ 也是 1-Lipschitz（IFT + MVT，VERIFIED） + ↓ +双 Lipschitz → 全局等距（VERIFIED） + ↓ +Mazur–Ulam（axiom）→ h(z) = Az + b + ↓ +h(0) = 0 → b = 0（VERIFIED） + ↓ +A 保范数 → A 是线性等距（VERIFIED） +``` + +### `lipschitz_of_orthogonal_jacobian`（MVT 应用） + +```lean +theorem lipschitz_of_orthogonal_jacobian + (h : GaussianDiffeo n) + (horth : ∀ z v, ‖h.jacobian z v‖ = ‖v‖) : + LipschitzWith 1 h.toFun := by + apply lipschitzWith_of_nnnorm_fderiv_le (𝕜 := ℝ) + · intro x; exact (h.hasFDeriv x).differentiableAt + · intro x + have hfderiv : fderiv ℝ h.toFun x = h.jacobian x := + (h.hasFDeriv x).fderiv + rw [hfderiv, ContinuousLinearMap.opNNNorm_le_iff] + intro y; simp only [one_mul] + exact_mod_cast le_of_eq (horth x y) +``` + +**关键 Mathlib 定理**： +- [`lipschitzWith_of_nnnorm_fderiv_le`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Calculus/MeanValue.html)：MVT 的 Lipschitz 版本 +- `ContinuousLinearMap.opNNNorm_le_iff`：算子范数的等价刻画 + +### `isometry_of_bilipschitz`（双 Lipschitz → 等距） + +```lean +theorem isometry_of_bilipschitz ... := by + rw [isometry_iff_dist_eq] + intro x y + apply le_antisymm + · -- dist(hx,hy) ≤ dist(x,y)：正向 Lipschitz + have hfwd := hlip.dist_le_mul x y + simp only [NNReal.coe_one, one_mul] at hfwd; exact hfwd + · -- dist(x,y) ≤ dist(hx,hy)：对 h⁻¹ 用 Lipschitz + have hbwd := hinvlip.dist_le_mul (h.toFun x) (h.toFun y) + -- h⁻¹(h(x)) = x，h⁻¹(h(y)) = y + rw [hx, hy] at hbwd; exact hbwd +``` + +--- + +## 8. 推论 4.5 证明走读（Planning.lean） + +### 数学陈述 + +> 对任意 O(n)-不变代价函数，在学习潜空间和真实潜空间中的最优值和最优计划完全一致。 + +### 核心定理：`planning_equivalence` + +```lean +theorem planning_equivalence ... := by + unfold totalCost + -- 阶段代价等价：对每个时间步 t + have hstage : + (∑ t, E_hat.stage_exp a (Q z) t cp.stage_cost) + = ∑ t, E.stage_exp a z t cp.stage_cost := by + apply Finset.sum_congr rfl + intro t _ + exact stage_cost_equiv cp Q E_hat E hinv a z t + -- 终端代价等价 + have hterm := terminal_cost_equiv cp Q E_hat E hinv a z + rw [hstage, hterm] +``` + +### `stage_cost_equiv`（阶段代价等价） + +```lean +-- 关键步骤：O(n)-不变性 + 轨迹推前 → 代价相等 +theorem stage_cost_equiv ... := by + rw [stage_pushforward E_hat E Q a z t cp.stage_cost] + -- 推前后：E_hat.stage_exp a (Qz) t c = E.stage_exp a z t (c ∘ Q) + -- 由 O(n)-不变性：c(Q z', act) = c(z', act) + have hfun : (fun z' act => cp.stage_cost (Q z') act) = cp.stage_cost := by + funext z'; funext act + exact hinv.1 z' act -- IsOrthogonalInvariant 的第一个分量 + rw [hfun] +``` + +--- + +## 9. 常用 Lean 4 证明策略速查 + +| 策略 | 用途 | 示例 | +|------|------|------| +| `linarith` | 线性算术（加减乘常数） | `linarith [h1, h2]` | +| `nlinarith` | 非线性算术（含平方） | `nlinarith [sq_nonneg x]` | +| `ring` | 纯代数恒等式 | `ring` | +| `field_simp` | 化简含除法的等式 | `field_simp [hne]` | +| `simp` | 自动化简 | `simp [lemma1, lemma2]` | +| `exact` | 精确匹配 | `exact h` | +| `exact_mod_cast` | 带类型转换的精确匹配 | `exact_mod_cast h` | +| `apply` | 应用定理（留下子目标） | `apply mul_pos` | +| `rw` | 重写（等式替换） | `rw [h1, h2]` | +| `calc` | 链式计算 | `calc a ≤ b := ... _ = c := ...` | +| `by_contra` | 反证法 | `by_contra h; push_neg at h` | +| `push_neg` | 将否定推入量词 | `push_neg at h` | +| `obtain` | 解构存在量词 | `obtain ⟨x, hx⟩ := h` | +| `intro` | 引入假设/变量 | `intro x hx` | +| `funext` | 函数外延性 | `funext x` | +| `constructor` | 分解 And/Iff | `constructor` | +| `refine` | 部分填充目标 | `refine ⟨_, _, ?_, ?_⟩` | +| `set` | 引入局部定义 | `set D := δ / (2*ρ*(1-ρ)) with hD_def` | + +--- + +## 10. 如何添加新定理 + +### 步骤 1：确定数学内容 + +例如，想证明"当 n=1 时，相关性上界是紧的"。 + +### 步骤 2：在合适的文件中添加 + +```lean +-- 在 Hermite.lean 末尾添加 +/-- 当 n=1 且 w₁=1 时，相关性恰好等于 ρ。 -/ +theorem correlation_tight_when_linear + (sw : SpectralWeights) + (hlin : ∀ d, 2 ≤ d → sw.w d = 0) + (ρ : ℝ) (hρ0 : 0 < ρ) (hρ1 : ρ < 1) + (hsum : Summable (fun d => sw.w d * ρ ^ d)) : + ∑' d, sw.w d * ρ ^ d = ρ := by + -- 由 hlin，所有 d ≥ 2 的项为 0 + -- 由 w₀ = 0（zero_degree），只剩 d=1 项 + -- w₁ = 1（由 total_variance 和其他项为 0） + sorry -- 待完成 +``` + +### 步骤 3：填写证明 + +```lean + -- 将 tsum 分解为 d=0, d=1, d≥2 三部分 + have h_ge2 : ∀ d, 2 ≤ d → sw.w d * ρ ^ d = 0 := by + intro d hd; simp [hlin d hd] + have h0 : sw.w 0 * ρ ^ 0 = 0 := by simp [sw.zero_degree] + -- 利用 tsum_eq_single 或手动计算 + ... +``` + +### 步骤 4：编译验证 + +```bash +cd lean +lake build LeJEPA.Hermite +``` + +### 步骤 5：检查无 sorry + +```bash +grep -n "sorry" LeJEPA/Hermite.lean +``` + +--- + +## 11. 调试技巧 + +### 查看当前目标 + +在证明中插入 `?` 或使用 `#check` 查看类型： + +```lean +theorem my_thm ... := by + intro h + -- 此时在 VS Code 中将鼠标悬停在下一行可看到当前目标 + exact? -- 让 Lean 搜索可用的定理 +``` + +### 使用 `#check` 查看定理类型 + +```lean +#check Summable.tsum_le_tsum +-- Summable.tsum_le_tsum : Summable g → (∀ b, f b ≤ g b) → Summable f → tsum f ≤ tsum g +``` + +### 使用 `example` 快速测试 + +```lean +-- 不需要命名，快速验证一个小引理 +example (a b : ℝ) (ha : 0 < a) (hb : 0 < b) : 0 < a * b := + mul_pos ha hb +``` + +### 常见错误及解决 + +| 错误 | 原因 | 解决 | +|------|------|------| +| `unknown identifier 'xxx'` | 引理名拼写错误 | 用 `exact?` 搜索 | +| `type mismatch` | 类型不匹配 | 检查隐式参数，用 `exact_mod_cast` | +| `failed to synthesize instance` | 缺少类型类实例 | 检查 import，添加 `[...]` 实例 | +| `maximum recursion depth` | 证明太复杂 | 增加 `set_option maxHeartbeats` | +| `tactic 'exact' failed` | \ No newline at end of file