gaojie
6.8 KiB
Topic 3：谱分解与线性可识别性（定理 1 完整证明）
前置知识： Topic 1：Hermite 多项式、Topic 2：OU 过程与 Mehler 公式 目标： 把前两个 topic 的工具组合起来，完整理解定理1的证明逻辑
🎯 定理 1 的完整陈述
定理 1（线性可识别性）： 在高斯世界中，设编码器
h : ℝⁿ → ℝⁿ满足：
- 高斯约束：
h(z) ~ N(0, Iₙ)（嵌入分布是各向同性高斯）- 最优对齐：
h最小化对齐损失L_align = E[‖h(z') - h(z)‖²]则
h(z) = Qz，其中Q ∈ O(n)是正交矩阵。
白话翻译： 如果你强制嵌入是高斯的，并且最大化正样本对的相似度，那么编码器必然是线性的（且保持距离）。
🗺️ 证明路线图
高斯约束 + 最优对齐
↓
[步骤1] Hermite 展开：h_i(z) = Σ cₐ Heₐ(z)
↓
[步骤2] Mehler 公式：corr_i = Σ wₐ ρᵈ
↓
[步骤3] 关键不等式：corr_i ≤ ρ（等号 ⟺ w₁=1）
↓
[步骤4] 最优性条件：L_align = 2(1-ρ)n → 每个 corr_i = ρ
↓
[步骤5] 线性性：每个 h_i 是线性函数
↓
[步骤6] 正交性：高斯约束 + 线性 → Q ∈ O(n)
📐 步骤 1：Hermite 展开
由 Topic 1，任意满足 E[h_i(z)²] < ∞ 的函数可以展开：
h_i(z) = Σ_{α} c_{i,α} He_α(z)
其中 α = (α₁, ..., αₙ) 是多指标，|α| = α₁ + ... + αₙ 是总阶数。
高斯约束的含义：
E[h_i(z)] = 0→c_{i,0} = 0（零均值，排除常数项）E[h_i(z)²] = 1→Σ_{|α|≥1} c_{i,α}² |α|! = 1（单位方差）
定义谱权重：
w_{i,d} = Σ_{|α|=d} c_{i,α}² d! / E[h_i(z)²]
则 w_{i,d} ≥ 0，w_{i,0} = 0，Σ_d w_{i,d} = 1。
📐 步骤 2：用 Mehler 公式计算相关性
由 Topic 2 的 Mehler 公式：
corr_i := E[h_i(z') · h_i(z)] = Σ_{d=1}^{∞} w_{i,d} · ρᵈ
这是一个加权平均：用谱权重 w_{i,d} 对 ρᵈ 求加权和。
📐 步骤 3：关键不等式
引理（已在 Lean 4 中验证）：
corr_i = Σ_{d=1}^{∞} w_{i,d} · ρᵈ ≤ Σ_{d=1}^{∞} w_{i,d} · ρ = ρ
等号成立的条件：
等号成立 ⟺ 对所有 d ≥ 2，w_{i,d} · ρᵈ = w_{i,d} · ρ
由于 ρᵈ < ρ（当 d ≥ 2, 0 < ρ < 1），这要求 w_{i,d} = 0 对所有 d ≥ 2。
又因为 Σ_d w_{i,d} = 1 且 w_{i,0} = 0，所以 w_{i,1} = 1。
结论： corr_i = ρ ⟺ h_i 是纯线性函数（只有 d=1 的 Hermite 成分）。
📐 步骤 4：最优性条件
对齐损失可以写成：
L_align = E[‖h(z') - h(z)‖²]
= Σᵢ E[(h_i(z') - h_i(z))²]
= Σᵢ (E[h_i(z')²] + E[h_i(z)²] - 2E[h_i(z')h_i(z)])
= Σᵢ (1 + 1 - 2·corr_i)
= 2n - 2 Σᵢ corr_i
由步骤3，corr_i ≤ ρ，所以：
L_align = 2n - 2 Σᵢ corr_i ≥ 2n - 2nρ = 2(1-ρ)n
最优值 L_align = 2(1-ρ)n 当且仅当每个 corr_i = ρ。
由步骤3的等号条件，这要求每个 h_i 都是线性的。
📐 步骤 5：线性性
每个 h_i 只有 d=1 的 Hermite 成分，即：
h_i(z) = Σⱼ aᵢⱼ zⱼ
写成矩阵形式：h(z) = Az，其中 A ∈ ℝⁿˣⁿ。
📐 步骤 6：正交性
现在利用高斯约束 h(z) ~ N(0, Iₙ)：
如果 h(z) = Az 且 z ~ N(0, Iₙ)，则：
h(z) ~ N(0, AA^T)
要使 h(z) ~ N(0, Iₙ)，需要：
AA^T = Iₙ
这正是 A ∈ O(n)（正交矩阵）的定义！
结论： h(z) = Qz，Q ∈ O(n)。 □
🔍 为什么叫"线性可识别性"？
可识别性（Identifiability）的含义
在表示学习中，"可识别性"指：从观测数据 x = g(z) 中，能否恢复出真实的潜变量 z？
- 完全可识别：
h(x) = z（精确恢复） - 线性可识别：
h(x) = Qz（恢复到正交变换等价） - 置换可识别：
h(x) = Pz（恢复到置换等价，ICA 的结果） - 不可识别：无法从
h(x)恢复z的任何信息
为什么"正交等价"已经足够？
正交变换保持：
- 距离：
‖Qz₁ - Qz₂‖ = ‖z₁ - z₂‖ - 内积：
⟨Qz₁, Qz₂⟩ = ⟨z₁, z₂⟩ - 范数：
‖Qz‖ = ‖z‖
对于旋转不变的代价函数（如欧氏距离、LQR），在 Qz 空间中规划与在 z 空间中规划完全等价（见 Topic 6）。
🎨 几何直觉
真实潜空间 z: 学到的表示 h(z) = Qz:
z₂ h₂
↑ ↑
│ ● ● │ ● ●
│● ● │ ● ●
│ ●● │ ●●
└──────→ z₁ └──────→ h₁
两个空间的点云形状完全相同，只是旋转了角度 θ。
所有距离、角度关系都被保留。
⚠️ 证明的假设条件
定理1成立需要以下条件：
| 假设 | 含义 | 如果违反？ |
|---|---|---|
| 潜变量是高斯的 | z ~ N(0, I_n) |
定理2说明：非高斯时线性可识别性失败 |
| OU 转移 | z' = ρz + √(1-ρ²)η |
其他转移可能不满足 Mehler 公式 |
| 高斯约束 | h(z) ~ N(0, I_n) |
没有约束则编码器可能坍塌 |
| 最优对齐 | h 达到全局最优 |
局部最优可能不是线性的 |
🔧 Lean 4 验证状态
在 Hermite.lean 中：
| 步骤 | 对应定理 | 状态 |
|---|---|---|
| 步骤3（不等式） | correlation_le_rho |
✅ 机器验证 |
| 步骤3（等号条件） | equality_forces_degree_one |
✅ 机器验证 |
| 步骤4（损失下界） | loss_lower_bound |
✅ 机器验证 |
| 步骤4（最优性） | hermite_identifiability（主定理） |
✅ 机器验证 |
| 步骤1（Hermite 基） | mehler_summability |
公理化（Mathlib 尚未收录） |
| 步骤5（线性性） | linear_of_degree_one |
公理化 |
| 步骤6（正交性） | orthogonal_of_gaussian_linear |
公理化 |
✅ 小结
定理1的证明是一个优化论证：
- 把编码器用 Hermite 多项式展开（谱分解）
- 用 Mehler 公式计算正样本对的相关性
- 证明相关性 ≤ ρ，等号 ⟺ 纯线性
- 最优对齐要求每个分量都达到等号
- 因此编码器必须是线性的
- 高斯约束进一步要求线性映射是正交的
核心洞见： OU 过程对高阶非线性成分的"惩罚"（衰减）比线性成分更强，所以最优编码器会"放弃"所有非线性成分。
➡️ 下一步
→ Topic 4：Sturm-Liouville 理论与高斯唯一性——为什么只有高斯分布才能保证线性可识别性？