Email Gateway (Aug 19 2022 at 15:40): Email Gateway (Aug 19 2022 at 15:40):From: Tobias Nipkow <nipkow@in.tum.de>
Real-Valued Special Functions: Upper and Lower Bounds
Lawrence C. Paulson
This development proves upper and lower bounds for several familiar real-valued
functions. For sin, cos, exp and sqrt, it defines and verifies infinite families
of upper and lower bounds, mostly based on Taylor series expansions. For arctan,
ln and exp, it verifies a finite collection of upper and lower bounds,
originally obtained from the functions' continued fraction expansions using the
computer algebra system Maple. A common theme in these proofs is to take the
difference between a function and its approximation, which should be zero at one
point, and then consider the sign of the derivative. The immediate purpose of
this development is to verify axioms used by MetiTarski, an automatic theorem
prover for real-valued special functions. Crucial to MetiTarski's operation is
the provision of upper and lower bounds for each function of interest.
http://afp.sourceforge.net/entries/Special_Function_Bounds.shtml
Last updated: Apr 23 2024 at 20:15 UTC