# [isabelle] New AFP entry: Real-Valued Special Functions: Upper and Lower Bounds

*To*: Isabelle Users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] New AFP entry: Real-Valued Special Functions: Upper and Lower Bounds
*From*: Tobias Nipkow <nipkow at in.tum.de>
*Date*: Fri, 29 Aug 2014 16:52:45 +0200
*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:24.0) Gecko/20100101 Thunderbird/24.6.0

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

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*