A procedure for proving special function inequalities involving a discrete parameter

ABSTRACT

We define a class of special function inequalities that contains many classical examples, such as the Cauchy-Schwarz inequality, and introduce a proving procedure based on induction and Cylindrical Algebraic Decomposition. We present an array of non-trivial examples that can be done by our method. Most of them have not been proven automatically before. Some difficult well-known inequalities such as the Askey-Gasper inequality and Vietoris's inequality lie in our class as well, but we do not know if our proving procedure terminates for them.

REFERENCES

• 1: G. E. Andrews, R. Askey, and R. Roy. Special Functions, volume 71 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1999.
• 2: R. Askey and G. Gasper. Positive Jacobi polynomial sums II. American Journal of Mathematics, 98:709--737, 1976.
• 3: P. R. Beesack. On certain discrete inequalities involving partial sums. Canadian Journal of Mathematics, 21:222--234, 1969.
• 4: J. W. S. Cassels. An Introduction to Diophantine Approximation. Cambridge University Press, 1957.
• 5: B. Caviness and J. R. Johnson, editors. Quantifier Elimination and Cylindrical Algebraic Decomposition, Texts and Monographs in Symbolic Computation. Springer, 1998.
• 6: R. M. Cohn. Difference Algebra. Interscience Publishers, John Wiley & Sons, 1965.
• 7: George E. Collins, Hauptvortrag: Quantifier elimination for real closed fields by cylindrical algebraic decomposition, Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages, p.134-183, May 20-23, 1975
• 8: George E. Collins , Hoon Hong, Partial cylindrical algebraic decomposition for quantifier elimination, Journal of Symbolic Computation, v.12 n.3, p.299-328, Sept. 1991 [doi>10.1016/S0747-7171(08)80152-6]
• 9: L. de Branges. A proof of the Bieberbach conjecture. Acta Mathematica, 154:137--152, 1985.
• 10: Shalosh B. Ekhad, A short, elementary, and easy, WZ proof of the Askey-Gasper inequality that was used by de Branges in his proof of the Bieberbach conjecture, Theoretical Computer Science, v.117 n.1-2, p.199-202, Aug. 30, 1993
• 11: S. Gerhold and M. Kauers. A procedure for proving special function inequalities involving a discrete parameter -- Mathematica notebook with examples. Technical Report 2005-02, SFB F013, Johannes Kepler Universität, 2005. http://www.risc.uni-linz.ac.at/research/combinat/publications/.
• 12: G. Hardy, J. E. Littlewood, and G. Pólya. Inequalities. Cambridge Mathematical Library. Cambridge University Press, second edition, 1952.
• 13: M. Kauers. An algorithm for deciding zero equivalence of nested polynomially recurrent sequences. Technical Report 2003-48, SFB F013, Johannes Kepler Universität, 2003. (submitted).
• 14: Manuel Kauers, Computer proofs for polynomial identities in arbitrary many variables, Proceedings of the 2004 international symposium on Symbolic and algebraic computation, p.199-204, July 04-07, 2004, Santander, Spain [doi>10.1145/1005285.1005315]
• 15: D. S. MitrinoviĆ. Elementary Inequalities. P. Noordhoff Ltd., 1964.
• 16: D. S. MitrinoviĆ. Analytic Inequalities. Springer, 1970.
• 17: T. S. Nanjundiah. Problem 10347. The American Mathematical Monthly, 100(10), 1993.
• 18: P. Paule. A proof of a conjecture of Knuth. Experimental Mathematics, 5:83--89, 1996.
• 19: P. Paule. A computerized proof of ζ(2)=π2/6. In preparation, 2005.
• 20: Peter Paule , Markus Schorn, A Mathematica version of Zeilberger's algorithm for proving binomial coefficient identities, Journal of Symbolic Computation, v.20 n.5-6, p.673-698, Nov./Dec. 1995 [doi>10.1006/jsco.1995.1071]
• 21: M. Petkovšek, H. Wilf, and D. Zeilberger. A=B. AK Peters, Ltd., 1997.
• 22: I. Schur and K. Knopp. Über die Herleitung der Gleichung Σ n=1 ∞ 1/n 2= π 2/6. Archiv der Mathematik und Physik, 3(27):174--176, 1918.
• 23: J. Michael Steele, The Cauchy-Schwarz Master Class: An Introduction to the Art of Mathematical Inequalities, Cambridge University Press, New York, NY, 2004
• 24: Adam Strzeboński, Solving systems of strict polynomial inequalities, Journal of Symbolic Computation, v.29 n.3, p.471-480, March 2000 [doi>10.1006/jsco.1999.0327]

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.2 Algorithms

Additional Classification:
  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS
      G.2.1 Combinatorics
          Subjects: Recurrences and difference equations

General Terms:
Algorithms

Keywords:
computer proofs, cylindrical algebraic decomposition, inequalities, special functions