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$.

翻译：已知初等解析函数（指数函数、对数函数、三角函数、双曲函数及其反函数）的有理逼近可在弱复杂性类$\mathrm{TC}^0$中计算。我们展示了如何在相应的有界算术理论$\mathsf{VTC}^0$中形式化这些函数的构造及其基本性质。