worldmodel/plans/lejepa_math_lecture_plan.md

LeJEPA 数学定理专题讲解计划

📋 任务概述

对 LeJEPA（When Does LeJEPA Learn a World Model?）论文中的四大数学定理进行分专题的系统性讲解与严格推理证明。

---

🗺️ 知识依赖图

专题1: Hermite多项式与谱分解理论
    │
    ├──→ 预备知识: L²空间, 正交基, 高斯测度
    │
    ↓
专题2: OU过程与Mehler公式的严格推导
    │
    ├──→ 预备知识: 随机过程, 条件期望, 转移核
    │
    ↓
专题3: 定理1 — 线性可识别性（完整证明）
    │
    ├──→ 组合专题1+2的工具 + Procrustes分析
    │
    ↓                    ↘
专题4: 定理2 — 高斯唯一性   专题5: 定理3 — 近似可识别界
    │                        （组合专题1+2 + 三角不等式）
    ↓                        
专题6: 定理4 — 最优潜空间规划
    │
    └──→ O(n)-不变性 + 轨迹推前论证

---

📚 六大专题详细设计

专题 I：Hermite多项式与谱分解理论（定理1的基础）

目标： 建立高斯测度下函数展开的完整数学框架

内容大纲：

1. Hermite多项式的严格定义

   • 显式公式：Heₙ(x) = (-1)ⁿ eˣ²/² (dⁿ/dxⁿ)e^{-x²/2}
   • 递推关系证明：He_{n+1}(x) = x·Heₙ(x) - n·He_{n-1}(x)
   • 前6个多项式的显式计算

2. 正交性的严格证明

   • 在概率测度 γ = N(0,1) 下的内积定义：⟨f,g⟩_γ = E[f(z)g(z)]
   • 证明：⟨Heₘ, Heₙ⟩_γ = δ_{mn} · n!
   • 多变量推广：He_α(z) = ∏ᵢ He_{αᵢ}(zᵢ)，⟨He_α, He_β⟩ = δ_{αβ} · α!

3. 完备性定理

   • L²(γ) 是 Hilbert 空间
   • Hermite多项式构成完备正交基
   • Parseval 恒等式：‖f‖² = Σ_α |⟨f, Heₐ⟩|² / α!

4. 谱权重与方差分解

   • 定义：w_{f,d} = Σ_{|α|=d} cₐ² · α! / ‖f‖²
   • 证明：Σ_d w_{f,d} = 1，w_{f,0} = 0（零均值时）
   • 谱权重作为"非线性程度"的度量

Lean 4 对应： Hermite.lean

---

专题 II：Ornstein-Uhlenbeck过程与Mehler公式（定理1的基础）

目标： 严格推导OU过程的谱性质和Mehler求和公式

内容大纲：

1. OU过程的严格定义与性质

   • 连续时间 SDE：dz_t = -θz_t dt + σdW_t
   • 平稳分布：证明 z_t ~ N(0, σ²/(2θ)) 是平稳分布
   • 离散时间版本：z' = ρz + √(1-ρ²)η
   • 平稳性证明：若 z ~ N(0,I)，则 z' ~ N(0,I)

2. 转移核的显式形式

   • 条件分布：z'|z ~ N(ρz, (1-ρ²)I)
   • 转移密度：p(z'|z) = φ((z'-ρz)/√(1-ρ²)) / (1-ρ²)^{n/2}
   • 其中 φ 是标准高斯密度

3. Mehler公式的严格推导

   • 生成函数法：Σ_{n=0}^{∞} (tⁿ/n!) Heₙ(x) = e^{xt - t²/2}
   • 核心恒等式：Σ_{n=0}^{∞} (ρⁿ/n!) Heₙ(x)Heₙ(y) = exp((xyρ - ρ²x²/2 - ρ²y²/2)/(1-ρ²)) / √(1-ρ²)
   • Mehler公式：p(z'|z) = φ(z') · Σ_{α} ρ^{|α|} He_α(z)He_α(z') / α!

4. 相关性公式与谱衰减

   • 定理：对任意 f,g ∈ L²(γ)，E[f(z)g(z')] = Σ_α ρ^{|α|} ⟨f,Heₐ⟩⟨g,Heₐ⟩/α!
   • 推论：对编码器分量 h_i，corr_i = Σ_{d=1}^{∞} w_{i,d} · ρᵈ
   • 关键不等式：corr_i ≤ Σ w_{i,d} · ρ = ρ，等号 ⟺ w_{i,1}=1

Lean 4 对应： Hermite.lean 中的 mehler_summability

---

专题 III：定理1 — 线性可识别性（完整证明）

目标： 组合前两个专题的工具，完成定理1的严格证明

内容大纲：

1. 定理陈述与假设梳理

   • 世界模型：z ~ N(0, Iₙ)，正样本对由OU过程生成
   • 编码器约束：h: ℝⁿ → ℝⁿ，h(z) ~ N(0, Iₙ)
   • 优化目标：最小化 L_align(h) = E[‖h(z')-h(z)‖²]
   • 结论：最优 h 满足 h(z) = Qz，Q ∈ O(n)

2. 证明步骤1-3：Hermite展开与相关性上界

   • 对每个分量 h_i，Hermite展开：h_i(z) = Σ_α c_{i,α} Heₐ(z)
   • 高斯约束的谱含义：Σ_{|α|≥1} c_{i,α}² · α! = 1
   • Mehler公式：corr_i = Σ_{d=1}^{∞} w_{i,d} · ρᵈ
   • 不等式：corr_i ≤ ρ，等号 ⟺ w_{i,1} = 1

3. 证明步骤4：最优性条件

   • L_align = 2n - 2Σᵢ corr_i ≥ 2(1-ρ)n
   • 最优值 L_align* = 2(1-ρ)n ⟺ 每个 corr_i = ρ
   • 等号条件：每个 h_i 只有 d=1 的 Hermite 成分

4. 证明步骤5-6：线性性与正交性

   • 线性性：h_i(z) = Σⱼ a_{ij} z_j，即 h(z) = Az
   • 高斯约束：若 z ~ N(0,I)，则 Az ~ N(0, AA^T)
   • 正交性：AA^T = Iₙ ⟺ A ∈ O(n)
   • 结论：h(z) = Qz，Q ∈ O(n)

5. 唯一性讨论

   • 正交等价类：h(z) = Qz，Q ∈ O(n) 都是最优解
   • 为什么不能进一步识别（需要额外约束）

Lean 4 对应： Hermite.lean 中的 hermite_identifiability

---

专题 IV：定理2 — 高斯唯一性（Sturm-Liouville方法）

目标： 证明高斯分布是唯一使线性可识别性成立的分布

内容大纲：

1. 定理陈述与背景

   • 世界假设：独立性、平稳性、加性噪声 z' = m(z) + η
   • 结论：高斯是唯一使线性可识别性成立的分布

2. 转移算子与Sturm-Liouville理论

   • 条件期望作为转移算子：T[f](z) = E[f(z')|z]
   • 在 L²(p) 中的自伴性证明
   • Sturm-Liouville方程的推导：T[φ] = λ·φ ⟺ -(Kpφ')' = -λ₁ p φ
   • 显式形式：K·score(z)·φ(z) + K·φ'(z) = -λ₁·φ(z)

3. 从仿射特征函数到高斯分布

   • 假设：φ₁(z) = az + b（仿射）
   • 代入SL方程：K·score(z)·a = -λ₁(az+b)
   • 解得分函数：score(z) = -(λ₁/K)·z - (λ₁b)/(Ka)
   • 积分：log p(z) = -(λ₁/2K)·z² + ...
   • 结论：p(z) 是高斯分布

4. 反向证明（高斯 → Hermite多项式）

   • 对 p = N(0,1)，得分函数为 -z
   • SL方程变为：-φ'(z) + z·φ(z) = -(λ₁/K)·φ(z)
   • 验证：Heₙ(z) 是特征函数，对应 λ_{n+1} = n·K
   • 第一非常数特征函数：He₁(z) = z（仿射）

5. 双条件定理

   p 是高斯分布 ⟺ φ₁(z) = az+b ⟺ LeJEPA实现线性可识别性
   

6. 与经典ICA的对比分析

   • 线性 ICA：高斯是"最难分离"的情况（旋转不变性）
   • LeJEPA：高斯是"最容易识别"的分布（Mehler公式）
   • 根本原因：ICA利用高阶统计量，LeJEPA利用时间结构

Lean 4 对应： Uniqueness.lean

---

专题 V：定理3 — 近似可识别性界

目标： 量化假设只近似满足时的恢复误差上界

内容大纲：

1. 定理陈述与动机

   • 精确版本（定理1）：完美条件下 h(z) = Qz
   • 近似版本：条件只近似满足时，误差有界

2. 两个误差参数的严格定义

   • 对齐间隙：δ = L_align(h) - 2(1-ρ)n ≥ 0
   • 白化误差：ε = ‖Cov(h(z)) - Iₙ‖_F
   • 归一化量：D = δ / (2ρ(1-ρ))

3. 谱间隙的严格分析

   • 线性成分与二次成分的差距：ρ¹ - ρ² = ρ(1-ρ)
   • 一般情况：ρᵈ⁻¹ - ρᵈ = ρ^{d-1}(1-ρ)
   • 谱间隙最小值在 d=2：ρ(1-ρ)

4. 从δ到D的转换

   • L_align = 2n - 2Σᵢ Σ_d w_{i,d} ρᵈ
   • δ = 2Σᵢ Σ_{d≥2} w_{i,d}(ρ - ρᵈ)
   • 下界：δ ≥ 2Σᵢ Σ_{d≥2} w_{i,d} · ρ(1-ρ)
   • 结论：Σᵢ Σ_{d≥2} w_{i,d} ≤ δ/(2ρ(1-ρ)) = D

5. 从D到恢复误差

   • 线性近似：取 A 为 h 的 d=1 成分
   • E[‖h(z) - Az‖²] = Σᵢ Σ_{d≥2} w_{i,d} · ‖h‖² ≤ D

6. Procrustes分析：从A到Q

   • 定义 Q = argmin_{O∈O(n)} ‖A - O‖_F（正交Procrustes问题）
   • SVD分解：A = UΣV^T ⟹ Q = UV^T
   • 误差界：‖A-Q‖_F ≤ ε + D（需要详细推导）

7. 最终组合

   • E[‖h(z) - Qz‖²] ≤ E[‖h(z)-Az‖²] + ‖A-Q‖_F²
   • ≤ D + (ε+D)²

8. 数值分析与实验验证

   • 不同 ρ, δ, ε 水平下的界值计算表

Lean 4 对应： Approx.lean

---

专题 VI：定理4 — O(n)-不变性与最优规划等价性

目标： 证明线性可识别性足以保证O(n)-不变代价函数下的最优规划等价

内容大纲：

1. 定理陈述与背景

   • 设 h(z) = Qz，Q ∈ O(n)（由定理1保证）
   • 控制问题：有限时域 T，状态空间 ℝⁿ
   • 代价函数条件：O(n)-不变性

2. O(n)群与不变函数的严格定义

   • 正交群 O(n) = {Q ∈ ℝ^{n×n} : Q^TQ = I}
   • O(n)-不变函数：ℓ(Qz, a) = ℓ(z,a) 对所有 Q ∈ O(n)
   • 常见例子与反例的详细分析

3. 代价等价引理

   • 证明：ℓ(Qz, a) = ℓ(z,a)（由O(n)-不变性）
   • 对任意轨迹 z_{0:T}，ℓ(Qz_t, a) = ℓ(z_t, a)

4. 轨迹推前（Trajectory Pushforward）

   • 真实动力学：p(z'|z, a)
   • 潜空间动力学：p̂(ẑ'|ẑ, a) = p(Q^T ẑ' | Q^T ẑ, a)
   • 验证：p̂(Qz'|Qz, a) = p(z'|z, a)

5. 总代价等价

   • 对任意动作序列 a_{1:T}：

     J(a; z₀) = E[Σ_t ℓ(z_t, a_t)]
     Ĵ(a; Qz₀) = E[Σ_t ℓ(Qz_t, a_t)]
     

   • 由O(n)-不变性：J(a; z₀) = Ĵ(a; Qz₀)

6. 最优性等价

   • V*(z₀) = inf_a J(a; z₀)
   • V̂*(Qz₀) = inf_a Ĵ(a; Qz₀)
   • 由于对所有 a，J = Ĵ：V*(z₀) = V̂*(Qz₀)
   • 最优动作序列相同

7. 实验验证：DMC Reacher

   • OU采样 vs RL轨迹的规划质量对比

8. 局限性与扩展方向

   • 非O(n)-不变代价函数（如坐标依赖）
   • 动作条件转移的可识别性
   • 无限时域折扣MDP

Lean 4 对应： Planning.lean

---

📊 各专题交付物清单

专题	数学文件	Lean验证对应	核心定理/公式数
I	01_hermite_polynomials.md	Hermite.lean (零sorry)	4个定理, 2个恒等式
II	02_ou_process_mehler.md	Hermite.lean (零sorry)	3个定理, Mehler公式
III	03_spectral_identifiability.md	Hermite.lean (零sorry)	定理1完整证明
IV	04_sturm_liouville_uniqueness.md	Uniqueness.lean (零sorry)	定理2完整证明
V	05_approximate_identifiability.md	Approx.lean (零sorry)	定理3完整证明
VI	06_planning_equivalence.md	Planning.lean (零sorry)	定理4完整证明

---

🎯 讲解风格与深度控制

每个专题的标准结构

1. 问题动机（白话翻译）
2. 严格定义与假设
3. 核心定理陈述
4. 逐步证明推导（每步标注逻辑依据）
5. 几何/物理直觉图示
6. 数值例子与实验验证
7. Lean 4形式化对应
8. 小结与下一步指引

数学深度级别标记

• ⭐⭐：本科水平（需要线性代数、概率论基础）
• ⭐⭐⭐：研究生入门级（需要泛函分析、随机过程基础）

---

📅 建议执行顺序与依赖关系

Phase 1: 基础工具（专题 I + II）
    ↓
Phase 2: 核心定理（专题 III → V，可并行 II→III, I→IV）
    ↓
Phase 3: 应用定理（专题 VI，依赖 III + V）

---

🔗 与现有资源的对应关系

资源	路径	用途
论文PDF	2605.26379v1.pdf	定理原始来源
Lean工程	lejepa-identifiability/lean/	形式化验证（零sorry）
Python实验	lejepa-identifiability/experiments/	数值验证与可视化
动画工具	lejepa-identifiability/animations/	交互式参数演示
论文笔记	[lejepa_world_model_notes.md](JEPA/ achieve/)	综合分析参考