超越函数不等式的证明：结合SDP和max-plus逼近
Certification of inequalities involving transcendental functions: combining SDP and max-plus approximation
摘要：
我们考虑证明形式为$f(x)\geq 0$，$\forall x\in K$的不等式的问题，其中$f$是多元超越函数，$K$是紧致半代数集.我们介绍了一种证明方法，结合半代数优化和最大加近似。我们假设$f$是由一个语法树，其成分涉及半代数运算，以及一些超越功能，如$\cos$，$\sin$，$\exp$等，我们绑定这些成分的上下限或二次型（最大加近似法，最初引入最优控制），导致半代数最优化问题，我们解决了半定松弛。最大加近似迭代细化，并结合分支定界技术，以减少松弛间隙。该算法的应用说明性的例子，解释我们如何解决紧不等式发出的Flyspeck项目（其主要目的之一是证明数字不等式中使用的证明开普勒猜想的托马斯黑尔斯）。
英文摘要：
We consider the problem of certifying an inequality of the form $f(x)\geq 0$, $\forall x\in K$, where $f$ is a multivariate transcendental function, and $K$ is a compact semialgebraic set. We introduce a certification method, combining semialgebraic optimization and max-plus approximation. We assume that $f$ is given by a syntaxic tree, the constituents of which involve semialgebraic operations as well as some transcendental functions like $\cos$, $\sin$, $\exp$, etc. We bound some of these constituents by suprema or infima of quadratic forms (max-plus approximation method, initially introduced in optimal control), leading to semialgebraic optimization problems which we solve by semidefinite relaxations. The max-plus approximation is iteratively refined and combined with branch and bound techniques to reduce the relaxation gap. Illustrative examples of application of this algorithm are provided, explaining how we solved tight inequalities issued from the Flyspeck project (one of the main purposes of which is to certify numerical inequalities used in the proof of the Kepler conjecture by Thomas Hales).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
