Certification of inequalities involving transcendental functions: combining SDP and max-plus approximation

TL;DR

This paper presents a novel certification method for inequalities involving multivariate transcendental functions by combining semialgebraic optimization, max-plus approximation, and branch-and-bound techniques, demonstrated on Flyspeck project inequalities.

Contribution

It introduces a new approach that integrates max-plus approximation with semidefinite relaxations to certify inequalities with transcendental functions.

Findings

Successfully certified tight inequalities from the Flyspeck project.

Demonstrated iterative refinement reduces relaxation gaps effectively.

Applicable to complex inequalities involving transcendental functions.

Abstract

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).