[Math] Computer calculations in a paper

Question

I think I can improve the current upper bound concerning an open problem. The ideas are purely combinatorial, but in the end I have to calculate the maximum of a really ugly, non elementary function with four variables. I did this with a computer, and the output was good so that's why I think I can improve the bound. (In the most precise sense, as this is not a real proof, but clearly not nothing.)

My first question is: What kind of computer calculations can be included in a paper?

To be a little bit more specific, my function includes the inverse of the binary entropy function (actually both inverses). This is not an elementary function and it is not implemented in Wolfram Mathematica (the program I am working in). So I had to calculate its values numerically. My function sometimes involves two of such functions nested in each other, but only at most 3 times. During the process I had to obtain upper bounds on complicated functions with two variables, I did this by plotting them and plotting the plane of the corresponding constant, and observing that the graph of the function is under the plane.

To elaborate a bit further, I saw in other papers, that if you prove that the required constant is a solution of a certain equation, it is okay to stop there and say that "and this constant is approximately 2,32", as this can be calculated easily with arbitrarily small error. But I feel like my proof is not complete, as I do not know the error of the approximation of my function, and somehow I am also not satisfied by the "plotting and observing" type bounds. I believe them to be true, but this method lacks rigour. On the other hand, I feel that my real contributions to the subject are the combinatorial ideas. It is of course important to prove that they really improve the current bounds. But I feel that this should be easy. But non elementary functions are making it not that easy. My second question is: What would be the best solution, if my goal is to write a good paper?

Answer 1

I suggest that Thomas Hales' work on the Kepler Conjecture can serve as a model. In particular, in this paper,

Solovyev, Alexey, and Thomas C. Hales. "Formal verification of nonlinear inequalities with Taylor interval approximations." NASA Formal Methods. Springer Berlin Heidelberg, 2013. 383-397. (link to arXiv abstract.)

they show how to prove inequalities such as

---

         
          ^{(from p.11 of the arXiv version.)}

---

Their abstract begins:

We present a formal tool for verification of multivariate nonlinear inequalities. Our verification method is based on interval arithmetic with Taylor approximations. Our tool is implemented in the HOL Light proof assistant and it is capable to verify multivariate nonlinear polynomial and non-polynomial inequalities on rectangular domains.