发表机构
Chapman University; University of Massachusetts Lowell（查普曼大学; 马萨诸塞大学洛厄尔分校）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对二元对称信道，证明了 Hellinger 猜想的一个弱形式，即独裁者函数在所有布尔函数及一位输出统计量中最大化 Hellinger Φ-熵，通过显式不等式与计算机辅助验证完成证明。
AI 中文摘要
本文证明了 Anantharam、Bogdanov、Chakrabarti、Jayram 和 Nair 针对二元对称信道提出的 Hellinger 猜想的一个弱形式：在所有关于输入变量的布尔函数以及噪声信道输出的一位统计量中，独裁者函数最大化 Hellinger Φ-熵。该问题的技术核心是一个涉及三个实参数的显式不等式，其证明利用了显式多项式逼近和计算机辅助的正性检验。研究结果还在 Lean 4 中得到了形式化验证。
英文摘要
A weak form of the Hellinger conjecture of Anantharam, Bogdanov, Chakrabarti, Jayram, and Nair for the binary symmetric channel is proved: dictator functions maximize Hellinger $Φ$-entropy among all Boolean functions of the input and all one-bit statistics of the output of a noisy channel. The technical heart of the matter is an explicit inequality in three real parameters, which is proved using explicit polynomial approximations and computer-assisted positivity checks. The results are also formally verified in Lean 4.
Commentsv2: 20 pages; additional references and remarks; associated formalization available at https://github.com/roos-j/lean-weakhellinger
