A proof of concept tool to verify estimates

Summary

This post was inspired by some recent discussions with Bjoern Bringmann. Symbolic math software packages are highly developed for many mathematical tasks in areas such as algebra, calculus, and numerical analysis. However, to my knowledge we do not have similarly sophisticated tools for verifying asymptotic estimates – inequalities that are supposed to hold for arbitrarily large parameters, with constant losses. Particularly important are functional estimates, where the parameters involve an unknown function or sequence (living in some suitable function space, such as an space); but for this discussion I will focus on the simpler situation of asymptotic estimates involving a finite number of positive real numbers, combined using arithmetic operations such as addition, multiplication, division, exponentiation, and minimum and maximum (but no subtraction). A typical inequality here might be the weak arithmetic mean-geometric mean inequality where are arbitrary positive real numbers, and the here indicates that we are willing to lose an unspecified constant in the estimates. I have wished in the past (e.g., in this MathOverflow answer) for a tool that could automatically determine whether such an estimate was true or not (and provide a proof if true, or an asymptotic counterexample if false). In principle, simple inequalities of this form could be automatically resolved by brute force case splitting. For instance, with (1), one first observes that is comparable to up to constants, so it suffices to determine if Next, to resolve the maximum, one can divide into three cases: ; ; and . Suppose for instance that . Then the estimate to prove simplifies to and this is (after taking logarithms) a positive linear combination of the hypotheses , . The task of determining such a linear combination is a standard linear programming task, for which many computer software packages exist. Any single such inequality is not too difficult to resolve by hand, but there are applications i...