Computer Algebra for Special Functions Inequalities

In the past decades computer algebra has evolved to an essential tool for finding and proving summation and integration identities for special functions. Methods for proving inequalities, however, are at present rare to nonexistent even though special functions inequalities arise in many areas of mathematics and physics. A first major breakthrough is marked by the work of Gerhold and Kauers (2005) who discovered an approach to automatically prove inequalities for a large class of special functions inequalities using cylindrical algebraic decomposition (CAD). While this method launched a new field of applications for computer algebra, there are still important open questions such as a priori criteria for termination. The goal of this project is the development, implementation and application of new algorithms for proving inequalities on special functions. We plan to follow and combine different approaches: turning ad hoc techniques in the spirit of classical proofs into algorithmic approaches, which is closely related to extending symbolic summation algorithms to both assisting tools and stand-alone inequality provers, as well as pushing further the CAD-based approach coined by Gerhold and Kauers.

This project has contributed to the further development and understanding of automatic techniques to handle (special functions) inequalities and to the dissemination of these techniques to areas of mathematics not usually using computer algebra.Special functions are interesting as they arise in many different applications in mathematics or physics. They are considered special in part because of their usefulness and in part because of nice ways to represent them, such as defining them using difference or differential equations.Inequalities are problems that are easily formulated but typically difficult to be proven. In classical mathematics many different approaches are used in these proofs. Inequalities involving special functions have been investigated for centuries, but even in classical analysis there is no streamlined way to deal with them, and usually they are treated on a case-by-case basis. For handling (systems of) polynomial inequalities computer algebra tools such as Cylindrical Algebraic Decomposition (CAD) are nowadays available. Algorithms for dealing with special functions inequalities are still rare and were until recently non-existent.Essentially the only available method so far was introduced by Gerhold and Kauers (2005). Their method was one of the starting points of this project: it was applied to solve specific problems in collaboration with mathematicians working in classical areas of mathematics. Furthermore its applicability was analysed and in the course of this a variation of the procedure was introduced. The method of Gerhold and Kauers relies on CAD computations and those suffer from high computational complexity. When working on special functions inequalities often the limits of computational power are reached in terms of time and memory. Large scale inequalities from different areas of mathematics, such as Numerical Mathematics or Fuzzy Logic, have been treated successfully in this project. Besides being interested in the solution of the problem at hand, studying them allowed to obtain more expertise on how to deal with problems that are known to be treatable in theory by CAD, but seem to be out of reach in practice.Despite being the most powerful known automatic approach these days, the method of Gerhold and Kauers proceeds in a black box fashion and solely returns the truth value of a given inequality, but no human-readable proof or further insight. A different approach was developed in this project that is based on solving a given difference equation in terms of a finite linear combination of squares of special functions with rational function coefficients. Tools such as CAD can be applied to determine positivity of these coefficients (or at least the domain where these coefficients are positive). This way a representation is obtained that allows to read off positivity for the given input. This algorithm has been implemented in the computer algebra system Maple and is available for download.