Formally Verified Approximations of Definite Integrals - Archive ouverte HAL Access content directly
Conference Papers Year : 2016

Formally Verified Approximations of Definite Integrals

(1) , (2) , (1)
1
2

Abstract

Finding an elementary form for an antiderivative is often a difficult task, so numerical integration has become a common tool when it comes to making sense of a definite integral. Some of the numerical integration methods can even be made rigorous: not only do they compute an approximation of the integral value but they also bound its inaccuracy. Yet numerical integration is still missing from the toolbox when performing formal proofs in analysis. This paper presents an efficient method for automatically computing and proving bounds on some definite integrals inside the Coq formal system. Our approach is not based on traditional quadrature methods such as Newton-Cotes formulas. Instead, it relies on computing and evaluating antiderivatives of rigorous polynomial approximations, combined with an adaptive domain splitting. This work has been integrated to the CoqInterval library.
Fichier principal
Vignette du fichier
main.pdf (355.52 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01289616 , version 1 (17-03-2016)
hal-01289616 , version 2 (27-05-2016)

Licence

Attribution - CC BY 4.0

Identifiers

Cite

Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote. Formally Verified Approximations of Definite Integrals. Interactive Theorem Proving, Aug 2016, Nancy, France. ⟨10.1007/978-3-319-43144-4_17⟩. ⟨hal-01289616v2⟩
931 View
641 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More