# LeJEPA 数学证明分解导航

> 本目录将论文 *When Does LeJEPA Learn a World Model?* 的数学证明拆分为 6 个独立 topic，每个 topic 专注一个概念，循序渐进。
>
> **建议阅读顺序：** Topic 1 → 2 → 3 → 4 → 5 → 6

---

## 📚 Topic 列表

| # | 文件 | 核心概念 | 对应定理 | 难度 |
|---|------|---------|---------|------|
| 1 | [Hermite 多项式](01_hermite_polynomials.md) | 高斯分布下的函数分解工具 | 定理1基础 | ⭐⭐ |
| 2 | [OU 过程与 Mehler 公式](02_ou_process_mehler.md) | 正样本对生成 + 高阶衰减 | 定理1基础 | ⭐⭐ |
| 3 | [谱分解与线性可识别性](03_spectral_identifiability.md) | 定理1完整证明 | **定理 1** | ⭐⭐⭐ |
| 4 | [Sturm-Liouville 与高斯唯一性](04_sturm_liouville_uniqueness.md) | 为什么只有高斯分布有效 | **定理 2** | ⭐⭐⭐ |
| 5 | [近似可识别性界](05_approximate_identifiability.md) | 误差如何优雅降级 | **定理 3** | ⭐⭐ |
| 6 | [正交不变性与最优规划](06_planning_equivalence.md) | 潜空间规划等价于真实规划 | **定理 4** | ⭐⭐ |

---

## 🗺️ 知识依赖图

```
Topic 1: Hermite 多项式
    │
    ↓
Topic 2: OU 过程 + Mehler 公式
    │
    ↓
Topic 3: 谱分解 → 线性可识别性（定理1）
    │                    │
    ↓                    ↓
Topic 4: 高斯唯一性    Topic 5: 近似界    Topic 6: 最优规划
（定理2）              （定理3）           （定理4）
```

---

## 🎯 四大定理速查

### 定理 1：线性可识别性（正向）
> 高斯世界 + LeJEPA 最优 → `h(z) = Qz`（正交矩阵）

**核心工具：** Hermite 谱分解 + OU 衰减 + 最优性条件

### 定理 2：高斯唯一性（逆向）
> 高斯分布是**唯一**使线性可识别性成立的分布

**核心工具：** Sturm-Liouville 特征值理论 + 得分函数分析

### 定理 3：近似可识别性
> 条件近似满足时，误差 `≤ D + (ε+D)²`，其中 `D = δ/(2ρ(1-ρ))`

**核心工具：** 三角不等式 + Procrustes 分析

### 定理 4：最优潜空间规划
> 线性可识别性 → O(n)-不变代价函数下的规划完全等价

**核心工具：** 正交不变性 + 轨迹推前

---

## 🔑 关键公式速查

### LeJEPA 训练目标
```
L(h) = λ · L_SIG + (1-λ) · L_align

L_align = E[‖h(z') - h(z)‖²]     # 对齐损失
L_SIG = SIGReg(h(z), N(0,I))      # 高斯正则化
```

### OU 过程（正样本对生成）
```
z' = ρz + √(1-ρ²) η,   η ~ N(0, I_n),   ρ ∈ (0,1)
```

### Mehler 公式（核心不等式）
```
E[h_i(z') · h_i(z)] = Σ_d w_{i,d} · ρᵈ ≤ ρ
等号 ⟺ w_{i,1} = 1（纯线性）
```

### 近似界
```
E[‖h(z) - Qz‖²] ≤ D + (ε + D)²
D = δ / (2ρ(1-ρ))
δ = L_align - 2(1-ρ)n（对齐间隙）
ε = ‖Cov(h(z)) - I‖_F（白化误差）
```

---

## 🔧 代码对应关系

| 数学概念 | 代码实现 |
|---------|---------|
| 非线性混合 `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) |
| 对齐损失 | [`losses.py:alignment_loss`](../lejepa-identifiability/experiments/lejepa_id/losses.py) |
| OU 增强 | [`data.py:ou_augment`](../lejepa-identifiability/experiments/lejepa_id/data.py) |
| R²、正交误差、近似界、Procrustes | [`metrics.py:compute_all_metrics`](../lejepa-identifiability/experiments/lejepa_id/metrics.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 文件 | 验证状态 |
|------|----------|---------|
| 定理1 / Thm 4.1（Hermite 路径） | [`lean/LeJEPA/Hermite.lean`](../lejepa-identifiability/lean/LeJEPA/Hermite.lean) | ✅ 零 sorry |
| 定理2（高斯唯一性） | [`lean/LeJEPA/Uniqueness.lean`](../lejepa-identifiability/lean/LeJEPA/Uniqueness.lean) | ✅ 零 sorry |
| 定理3 / Prop 4.3（近似界） | [`lean/LeJEPA/Approx.lean`](../lejepa-identifiability/lean/LeJEPA/Approx.lean) | ✅ 零 sorry |
| 定理4 / Corollary（规划等价） | [`lean/LeJEPA/Planning.lean`](../lejepa-identifiability/lean/LeJEPA/Planning.lean) | ✅ 零 sorry |
| 附录E（Dirichlet 路径） | [`lean/LeJEPA/Dirichlet.lean`](../lejepa-identifiability/lean/LeJEPA/Dirichlet.lean) | ✅ 零 sorry |

> 注：Lean 工程使用 Mathlib v4.28.0，零 `sorry`；公理化组件为 Mathlib 尚未提供的标准结论（Hermite 多项式基础设施、Mazur–Ulam、等权 AM–GM 等）。

---

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

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

---

## 📖 相关文件

- [论文完整笔记](../lejepa_world_model_notes.md) — 综合分析（含代码实现、官网图示）
- [资源汇总](../lejepa_resources.md) — 视频、论文、代码、HuggingFace 模型
- [代码仓库](../lejepa-identifiability/) — 本地 clone 的官方实现