从数值求解的香农型不等式中提取解析证明
信息论
2017-07-07 v1 math.IT
摘要
一类称为香农型不等式（Shannon-type inequalities, STIs）的信息不等式可以通过名为 ITIP 的计算机软件证明。在之前的工作中，我们展示了如何将该技术用于信息论不等式的傅里叶-莫茨金消去算法。本文中，我们提供一种提取信息不等式的解析证明的算法。香农型不等式通过求解优化问题来证明。我们将展示如何提取数值求解的信息不等式的形式证明。当某个不等式由 PMF 的若干约束隐含且证明不易显见时，此类证明可能很有用。更复杂的情况是，不等式成立既由于来自 PMF 的约束，也由于统计模型产生的其他约束。此类情况包括信息论容量域、率失真函数和无损压缩率。我们首先给出香农型信息不等式的形式化定义。然后我们回顾优化问题的最优解以及如何提取对用户可读的证明。
引用
@article{arxiv.1707.01656,
title = {Extracting analytic proofs from numerically solved Shannon-type Inequalities},
author = {Ido B. Gattegno and Haim H. Permuter},
journal= {arXiv preprint arXiv:1707.01656},
year = {2017}
}