# LeJEPA 数学证明专题讲解

> 本目录将论文 *When Does LeJEPA Learn a World Model?*（NeurIPS 2025）的数学证明拆分为 **6 个专题**，每个专题专注一个核心概念，循序渐进地展开严格数学推导。
>
> **建议阅读顺序：** 专题 I → II → III → IV → V → VI（严格依赖关系见下方知识图）
>
> 🎬 **交互式动画：** 每个专题都配有可拖动参数的可视化，见 [`animations/`](animations/README.md)
> 🖥️ **Lean 4 形式化：** 所有核心定理均已零 `sorry` 验证，见 [`lejepa-identifiability/lean/`](../lejepa-identifiability/lean/)

---

## 📚 专题列表与更新状态

| # | 文件 | 核心概念 | 对应定理 | 难度 | 状态 |
|---|------|---------|---------|------|------|
| I | [Hermite 多项式与谱分解理论](01_hermite_polynomials.md) | $L^2(\gamma)$ 完备正交基、Rodrigues公式、生成函数推导 | 定理1基础工具 | ⭐⭐ | ✅ **已重写：严格数学证明** |
| II | [OU 过程与 Mehler 公式](02_ou_process_mehler.md) | SDE显式解、转移核推导、Mehler求和公式完整证明 | 定理1基础工具 | ⭐⭐⭐ | ✅ **已重写：严格数学推导** |
| III | [谱分解与线性可识别性](03_spectral_identifiability.md) | 定理1完整证明（Hermite展开 + Mehler公式组合）| **定理 1** | ⭐⭐⭐ | 📝 待更新为严格版本 |
| IV | [Sturm-Liouville 与高斯唯一性](04_sturm_liouville_uniqueness.md) | SL特征值理论、得分函数分析、ICA对比 | **定理 2** | ⭐⭐⭐ | 📝 待更新为严格版本 |
| V | [近似可识别性界](05_approximate_identifiability.md) | 对齐间隙δ、白化误差ε、Procrustes分析 + 严格四步证明 | **定理 3** | ⭐⭐⭐ | ✅ **已重写：严格数学推导** |
| VI | [正交不变性与最优规划](06_planning_equivalence.md) | O(n)-不变代价函数、转移核推前 + 规划等价严格证明| **定理 4** | ⭐⭐⭐ | ✅ **已重写：严格数学推导** |
| VII | [SIGReg 正则化——切片特征函数高斯约束](07_sigreg_regularization.md) | 特征函数匹配、Cramér-Wold定理、切片技巧、代码逐行解析 | 定理1前提实现 | ⭐⭐⭐ | ✅ **新增：完整数学+代码讲解** |
| VIII | [线性 ICA——FastICA 与 JADE 算法深度分析](08_linear_ica_fastica_jade.md) | 盲源分离、峰度/负熵/累积量、不动点迭代、联合对角化、ICA vs LeJEPA 对偶反转 | 定理2对比背景 | ⭐⭐⭐ | ✅ **新增：算法+理论+对比** |

---

## 🗺️ 知识依赖图

```
专题 I: Hermite多项式与谱分解理论（严格证明 ✅）
    │  ├─ Rodrigues定义 + 递推公式证明
    │  ├─ 生成函数法推导
    │  └─ L²(γ) Hilbert空间框架 + Parseval恒等式
    │
    ↓
专题 II: OU过程与Mehler公式（严格推导 ✅）
    │  ├─ SDE显式解 + Ornstein-Uhlenbeck公式
    │  ├─ 平稳分布证明（连续+离散时间）
    │  └─ Mehler求和公式完整推导 + 转移核等价性验证
    │
    ↓
专题 III: 谱分解 → 线性可识别性（定理1）
    │                    │
    ↓                    ↓
专题 IV: 高斯唯一性   专题 V: 近似界    专题 VI: 最优规划
（定理2）              （定理3）           （定理4）

专题 IV: Sturm-Liouville理论
    ├─ 转移算子自伴性证明
    └─ SL方程 → 得分函数分析

专题 V: δ + ε → D+(ε+D)²
    ├─ 谱间隙分析
    └─ Procrustes误差界

专题 VI: O(n)-不变性 + 轨迹推前
    ├─ 代价等价引理证明
    └─ DMC Reacher实验验证
```

---

## 🎯 四大定理速查表

| 定理 | 标题 | 核心结论 | 核心工具 |
|------|------|---------|---------|
| **定理1** | 线性可识别性（正向） | 高斯世界 + LeJEPA最优 → $h(z) = Qz$（正交矩阵） | Hermite谱分解 + OU衰减 + 最优性条件 |
| **定理2** | 高斯唯一性（逆向） | 高斯分布是**唯一**使线性可识别性成立的分布 | Sturm-Liouville特征值理论 + 得分函数分析 |
| **定理3** | 近似可识别性 | 条件近似满足时，误差 $\leq D + (\varepsilon+D)^2$ | 三角不等式 + Procrustes分析 |
| **定理4** | 最优潜空间规划 | O(n)-不变代价函数下的规划完全等价 | 正交不变性 + 轨迹推前论证 |

---

## 🔑 关键公式速查

### LeJEPA 训练目标
$$\mathcal{L}(h) = \lambda \cdot \mathcal{L}_{\text{SIG}} + (1-\lambda) \cdot \mathbb{E}[\|h(z') - h(z)\|^2]$$

### OU 过程（正样本对生成）
$$z' = \rho z + \sqrt{1-\rho^2}\,\eta, \quad \eta \sim \mathcal{N}(0, I_n),\;\rho \in (0,1)$$

### Mehler 公式（核心不等式）
$$\mathbb{E}[h_i(z') \cdot h_i(z)] = \sum_{d=1}^{\infty} w_{i,d}\,\rho^d \leq \rho$$
等号 $\iff$ $w_{i,1} = 1$（纯线性）

### 近似界
$$\mathbb{E}[\|h(z) - Qz\|^2] \leq D + (\varepsilon + D)^2$$
其中 $D = \delta / (2\rho(1-\rho))$，$\delta = \mathcal{L}_{\text{align}} - 2(1-\rho)n$，$\varepsilon = \|\text{Cov}(h(z)) - I\|_F$

---

## 🔧 代码对应关系

| 数学概念 | Python实现位置 |
|---------|---------------|
| Hermite展开 + Mehler公式计算相关性 | [`metrics.py:compute_all_metrics()`](../lejepa-identifiability/experiments/lejepa_id/metrics.py) |
| 非线性混合 $g$（spiral/banana/sinusoid/coupling） | [`mixing.py`](../lejepa-identifiability/experiments/lejepa_id/mixing.py) |
| SIGReg 正则化（切片特征函数） | [`losses.py:SIGReg`](../lejepa-identifiability/experiments/lejepa_id/losses.py) |
| 对齐损失 + OU增强 | [`data.py:ou_augment()`](../lejepa-identifiability/experiments/lejepa_id/data.py) |
| Reacher 像素渲染 / 数据集 | [`reacher.py`](../lejepa-identifiability/experiments/lejepa_id/reacher.py) |
| 训练循环（ lejepa / whiten / infonce） | [`engine.py:train_and_evaluate()`](../lejepa-identifiability/experiments/lejepa_id/engine.py) |

---

## 🔬 Lean 4 形式化验证状态

| 定理 | Lean文件 | 核心结论（零 `sorry`） |
|------|---------|---------------------|
| 定理1 / Thm 4.1 | [`Hermite.lean`](../lejepa-identifiability/lean/LeJEPA/Hermite.lean) | Mehler求和 + 相关性上界 + 最优性条件 |
| 定理2（高斯唯一） | [`Uniqueness.lean`](../lejepa-identifiability/lean/LeJEPA/Uniqueness.lean) | SL方程 → 高斯充要条件 |
| 定理3 / Prop 4.3 | [`Approx.lean`](../lejepa-identifiability/lean/LeJEPA/Approx.lean) | 近似界 $D+(\varepsilon+D)^2$ |
| 定理4 / Corollary | [`Planning.lean`](../lejepa-identifiability/lean/LeJEPA/Planning.lean) | 规划等价性 + DMC Reacher验证 |
| 附录E（Dirichlet） | [`Dirichlet.lean`](../lejepa-identifiability/lean/LeJEPA/Dirichlet.lean) | Dirichlet路径补充证明 |

> 注：Lean工程基于 Mathlib v4.28.0，所有核心定理零 `sorry`。公理化组件为 Mathlib 尚未提供的标准结论（Hermite多项式基础设施、Mazur–Ulam定理等）。

---

## 💡 核心洞见（一句话总结）

> **LeJEPA 将经典 ICA 的叙事完全颠倒：**
> - 在线性 ICA 中，高斯分布是源分离**失败**的唯一情况
> - 在 LeJEPA 的非线性设置中，高斯分布恰恰是使线性可识别性**成立**的唯一情况

---

## 📖 延伸阅读与相关文件

| 资源 | 路径 | 说明 |
|------|-----|------|
| [计划文档](../../plans/lejepa_math_lecture_plan.md) | `../plans/lejepa_math_lecture_plan.md` | 六大专题详细设计计划（2026-06更新）|
| [论文完整笔记](../lejepa_world_model_notes.md) | `../lejepa-identifiability/` 上级目录 | 综合分析（含代码实现、官网图示）|
| [资源汇总](../lejepa_resources.md) | 同上 | 视频、论文、代码、HuggingFace模型链接|
| [官方实现](../lejepa-identifiability/) | 本地 clone | Python实验 + Lean4形式化验证|
| [论文PDF](../LeJEPA/2605.26379v1.pdf) | `../LeJEPA/` | 原始论文（arXiv:2605.26379v1）|