Elementary analytic functions in $VTC^0$

TL;DR

This paper formalizes the construction and properties of elementary analytic functions within the weak complexity class  and its corresponding bounded arithmetic theory, , demonstrating their computability.

Contribution

It provides a formal framework in  for elementary analytic functions, extending prior knowledge of their computational properties.

Findings

Elementary analytic functions are formalizable in .

These functions are computable within .

The paper bridges computational complexity and formal arithmetic for these functions.

Abstract

It is known that rational approximations of elementary analytic functions (exp, log, trigonometric, and hyperbolic functions, and their inverse functions) are computable in the weak complexity class $\mathrm{TC}^0$. We show how to formalize the construction and basic properties of these functions in the corresponding theory of bounded arithmetic, $\mathsf{VTC}^0$.