Lean 4 对 JSD 收缩系数的形式化：核心定义与定理

Key Points

• 目标是在 Lean 4 中对与 Jensen-Shannon 散度收缩系数相关的定义和定理进行形式化。
• 利用 Lean 4 对数学定义进行形式验证。
• 引入 Mathlib 以支持数学库。
• 定义关键参数：s_m、λ_m、η_JSD 和 η_χ²。
• 建立并验证二元等式和 BSC 公式的定理。
• 使用形式化方法确认收缩系数的精确公式。
• 验证了 m=2 的二元等式案例。
• 用形式化证明增强了 m元对称信道公式。