Computer calculations in a paper 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?
 A: I suggest glancing at two papers:
Hagedorn, Thomas. "Computation of Jacobsthal’s function $h(n)$ for $n< 50$." Mathematics of Computation 78.266 (2009): 1073-1087.
Hajdu, L., and N. Saradha. "Disproof of a conjecture of Jacobsthal." Mathematics of Computation 81.280 (2012): 2461-2471.
Both of them describe somewhat massive projects which involve a lot of computation.  They give algorithmic descriptions as well as some sample computations.  Although I personally want more, they provide enough detail that I do not question the validity of their work.  You might use them as examples for how to write up your results.
Gerhard "The Computer Says So, QED" Paseman, 2015.07.25
A: 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.

A: Look at interval arithmetic. Warwick Tucker used this to prove Smale's fourteenth problem, which is a pretty good precedent for its use in a proof.
A: This is a problem that I have faced also. One approach is to try to prove rational polynomial bounds on the relevant functions (by Taylor series with remainder, for example) that are accurate enough to satisfy the same inequalities. Then you can prove the inequalities rigorously by various methods; the paper of Solovyev and Hales that Joseph links to describes free software better than I knew of before.  If the functions vary too much you might need to subdivide the domain and apply the method separately to each part.
You will then face the problem of what to put in the paper, as nobody wants to see page-long intermediate expressions.  But at least you can describe how you went about constructing a rigorous proof.
