This page is a web appendix to the following paper.
Florent Bréhard, Assia Mahboubi, Damien Pous
We present a library to verify rigorous approximations of univariate
functions on real numbers, with the Coq proof assistant. Based on
interval arithmetic, this library also implements a technique of
validation a posteriori based on the Banach fixed-point
theorem. We illustrate this technique on the case of operations of
division and square root.
This library features a collection of abstract structures that organise the specfication of rigorous approximations, and modularise the related proofs. Finally, we provide an implementation of verified Chebyshev approximations, and we discuss a few examples of computations.
posreal_complements: utilities on positive and non negative reals
domfct: Completeness of functions with uniform convergence over a domain
cball: Closed balls
contraction: Banach fixed-point theorem in complete normed spaces
div: Newton-like operator for division
sqrt: Newton-like operator for square root
neighborhood: hierarchy of structures: basic operations, operations on functions, neighborhoods
vectorspace: operations on linear combinations (generalised polynomials), bases, validity of bases
approx: rigorous approximations (models) in a generic basis
chebyshev: operations on Chebyshev basis
taylor: operations on monomial basis
rescale: rescaling operation on bases
intervals: implementation of neighborhoods based on floating point intervals