Automated Proof of Mixed Trigonometric-polynomial Inequalities in the Unbounded Case

TL;DR

This paper extends an existing algorithm to determine the sign of mixed trigonometric-polynomials from a bounded interval to an unbounded one, addressing challenges related to root boundedness and factorization.

Contribution

It introduces a novel procedure for analyzing the sign of mixed trigonometric-polynomials over unbounded intervals, expanding the applicability of prior methods.

Findings

Successfully extended the algorithm to unbounded intervals

Addressed root boundedness and factorization challenges

Enhanced the tool for applications in physics and engineering

Abstract

Mixed trigonometric-polynomials frequently occur in applications in physics, numerical analysis and engineering, the algorithm has been already proposed to determine its sign on (0,{pi}/2]. This paper proposes a procedure to extend the interval to (0, +{\inf}). Such generalization is by no means trivial, for the process depends on boundedness of roots and square-free factorization of mixed trigonometric-polynomials.