One method for proving inequalities by computer

关于一种用计算机证明不等式的方法的注记

Some notes on a method for proving inequalities by computer

本文基于Remez算法，探讨了一种用计算机证明不等式的方法的数学基础，指出该方法在实践中通常成为验证不等式的启发式方法，并改进了现有定理中基于数值验证的不等式。

A new method for proving some inequalities related to several special functions

In this paper we present a new approach to proving some exponential inequalities involving the sinc function. Power series expansions are used to generate new polynomial inequalities that are sufficient to prove the given exponential inequalities.

A Numerical Procedure for Proving Specific Strict One-Variable Inequalities in Specific Finite Intervals

A numerical procedure and its MAPLE implementation capable of rigorously, albeit in a brute-force manner, proving specific strict one-variable inequalities in specific finite intervals is described. The procedure is useful, for instance, to affirm strict lower bounds of specific functions.

One method for proving some classes of exponential analytic inequalities

In this paper we propose a method for proving some exponential inequalities based on power series expansion and analysis of derivations of the corresponding functions. Our approach provides a simple proof and generates a new class of appropriate inequalities, as well as allows direct establishment of the dependence between (the exponent of) some functions that occur as bounds of the approximation and the interval in which the corresponding inequality holds true.

A Method of Proving a Class of Inequalities of Mixed Trigonometric Polynomial Functions

In this article we consider a method of proving a class of inequalities of the form (1). The method is based on the precise approximations of the sine and cosine functions by Maclaurin polynomials of given order. By using this method we present new proofs of some inequalities from the articles C.-P. Chen, W.-S. Cheung [J. Inequal. Appl. 2012:72 (2012)] and Z.-J. Sun, L. Zhu [ISRN Math. Anal. (2011)].

The natural algorithmic approach of mixed trigonometric-polynomial problems

The aim of this paper is to present a new algorithm for proving mixed trigonometric-polynomial inequalities by reducing to polynomial inequalities. Finally, we show the great applicability of this algorithm and as examples, we use it to analyze some new rational (Pade) approximations of the function $\cos^2(x)$, and to improve a class of inequalities by Z.-H. Yang. The results of our analysis could be implemented by means of an automated proof assistant, so our work is a contribution to the library of automatic support tools for proving various analytic inequalities.