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.
interval
, coquelicot
, and mathcomp
)
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
example_abs
:
rigorous approximations of the absolut valu function
example_h16
:
evaluation of Abelian integrals related to Hilbert's 16th problem