package coq-approx-models

This is a Coq library to verify rigorous approximations of univariate functions on real numbers. Based on interval arithmetic, this library also implements a technique of validation a posteriori based on the Banach fixed-point theorem. We moreover provide an implementation of verified Chebyshev approximations.