worldmodel/JEPA/math

LeJEPA 数学证明专题讲解

本目录将论文 When Does LeJEPA Learn a World Model?（NeurIPS 2025）的数学证明拆分为 6 个专题，每个专题专注一个核心概念，循序渐进地展开严格数学推导。

建议阅读顺序： 专题 I → II → III → IV → V → VI（严格依赖关系见下方知识图）

🎬 交互式动画： 每个专题都配有可拖动参数的可视化，见 animations/ 🖥️ Lean 4 形式化： 所有核心定理均已零 sorry 验证，见 lejepa-identifiability/lean/

---

📚 专题列表与更新状态

#	文件	核心概念	对应定理	难度	状态
I	Hermite 多项式与谱分解理论	L^2(\gamma) 完备正交基、Rodrigues公式、生成函数推导	定理1基础工具	⭐⭐	✅ 已重写：严格数学证明
II	OU 过程与 Mehler 公式	SDE显式解、转移核推导、Mehler求和公式完整证明	定理1基础工具	⭐⭐⭐	✅ 已重写：严格数学推导
III	谱分解与线性可识别性	定理1完整证明（Hermite展开 + Mehler公式组合）	定理 1	⭐⭐⭐	📝 待更新为严格版本
IV	Sturm-Liouville 与高斯唯一性	SL特征值理论、得分函数分析、ICA对比	定理 2	⭐⭐⭐	📝 待更新为严格版本
V	近似可识别性界	对齐间隙δ、白化误差ε、Procrustes分析 + 严格四步证明	定理 3	⭐⭐⭐	✅ 已重写：严格数学推导
VI	正交不变性与最优规划	O(n)-不变代价函数、转移核推前 + 规划等价严格证明	定理 4	⭐⭐⭐	✅ 已重写：严格数学推导
VII	SIGReg 正则化——切片特征函数高斯约束	特征函数匹配、Cramér-Wold定理、切片技巧、代码逐行解析	定理1前提实现	⭐⭐⭐	✅ 新增：完整数学+代码讲解
VIII	线性 ICA——FastICA 与 JADE 算法深度分析	盲源分离、峰度/负熵/累积量、不动点迭代、联合对角化、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()
非线性混合 $g$（spiral/banana/sinusoid/coupling）	mixing.py
SIGReg 正则化（切片特征函数）	losses.py:SIGReg
对齐损失 + OU增强	data.py:ou_augment()
Reacher 像素渲染 / 数据集	reacher.py
训练循环（ lejepa / whiten / infonce）	engine.py:train_and_evaluate()

---

🔬 Lean 4 形式化验证状态

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

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

---

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

LeJEPA 将经典 ICA 的叙事完全颠倒：

• 在线性 ICA 中，高斯分布是源分离失败的唯一情况
• 在 LeJEPA 的非线性设置中，高斯分布恰恰是使线性可识别性成立的唯一情况

---

📖 延伸阅读与相关文件

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