二进制删除信道容量的一个新上界
A New Upper Bound on the Binary Deletion Channel Capacity
浏览论文内容
中文总结 AI 辅助
本文证明二进制删除信道容量在删除概率 $d\ge 13/20$ 时满足 $C(d)\le (1-d)/4$，通过六比特上下文描述长度与势函数望远镜求和给出上界，并附带有限块修正与Lean形式化验证。
中文摘要 AI 辅助
我们证明二进制删除信道的容量满足：对于每个 $13/20\le d<1$，有 $C(d)\le (1-d)/4$。证明从右到左描述输出，使用六比特上下文来分配描述长度。我们限制了当添加一个输入比特时期望描述长度减去输出熵的增加量。一个相对熵恒等式将该界限简化为有限多个线性不等式。长度为26的输入窗口上的一个势函数使这些不等式形成望远镜求和，从而对每个输入词给出界限。删除复合将结果从 $d=13/20$ 扩展到所有更大的删除概率。我们还获得了互信息和译码误差的有限块界限，带有显式的 $O(\log n/n)$ 修正项。有限证书使用精确整数算术进行验证，并且证明在Lean中端到端形式化。
英文摘要
We prove that the capacity of the binary deletion channel satisfies $C(d)\le (1-d)/4$ for every $13/20\le d<1$. The proof describes the output from right to left, using a six-bit context to assign a description length. We bound the increase in expected description length minus output entropy when one input bit is added. A relative-entropy identity reduces this bound to finitely many linear inequalities. A potential on input windows of length 26 makes the inequalities telescope, giving a bound for every input word. Deletion composition extends the result from $d=13/20$ to all larger deletion probabilities. We also obtain finite-block bounds on mutual information and decoding error, with explicit $O(\log n/n)$ corrections. The finite certificate is checked using exact integer arithmetic, and the proof is formalized end to end in Lean.
