Real root isolation for exp-log-arctan functions (Q765861)

Using the set of exp-log-arctan functions -- defined as the smallest set of partial functions \(\mathbb{R}\longrightarrow \mathbb{R}\) containing exp, log, arctan, identity and constant functions that are closed under addition, multiplication and composition of functions -- the author proposes a real root isolation procedure which is an extension of an algorithm defined by \textit{A. Strzeboński} [Real root isolation for exp-log functions, Proceedings of the twenty-first international symposium on symbolic and algebraic computation 2008, Linz/Hagenberg, Austria, July 20--23, 2008. New York, NY: Association for Computing Machinery (ACM). 303--314 (2008; Zbl 1236.65057)] for exp-log functions. Basically, the algorithm RootInInterval (defined in Section 5 together with several examples and a detailed study of complexity) offers a new proof of the claim: \textit{The domain of an exp-log-arctan function consists of a finite number of open intervals and an exp-log-arctan function has a finite number of real roots}. The algorithm uses the notion of semi-Fourier sequence and its applicability in root isolation proposed in an unpublished paper by \textit{D. Richardson} [Recognising zero among implicitly defined elementary numbers. (submitted for publication)]. The theoretical construction offered by the paper is finally verified by an implementation using a C source code and Mathematica system. All experimental results confirm the validity of the RootInInterval algorithm proposed.