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



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.