
RealValued
Special
Functions:
Upper
and
Lower
Bounds
Title: 
RealValued Special Functions: Upper and Lower Bounds 
Author:

Lawrence C. Paulson

Submission date: 
20140829 
Abstract: 
This development proves upper and lower bounds for several familiar realvalued 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 realvalued special functions. Crucial to MetiTarski's operation is the provision of upper and lower bounds for each function of interest. 
BibTeX: 
@article{Special_Function_BoundsAFP,
author = {Lawrence C. Paulson},
title = {RealValued Special Functions: Upper and Lower Bounds},
journal = {Archive of Formal Proofs},
month = aug,
year = 2014,
note = {\url{https://isaafp.org/entries/Special_Function_Bounds.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
Sturm_Sequences 
Status: [ok] 
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.

