Formally verified approximations of definite integrals

DOI10.1007/978-3-319-43144-4_17MaRDI QIDQ2829263zbMATH OpenOpenAlexFDO

Authors Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote

Publication date 27 October 2016

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-01289616v2/file/main.pdf

Mathematics Subject Classification ID

Numerical integration (65D30) Interval and finite arithmetic (65G30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Formally verified approximations of definite integrals
• Proving tight bounds on univariate expressions with elementary functions in Coq
• Proving Bounds on Real-Valued Functions with Computations
• scientific article; zbMATH DE number 1927426
• An adaptive numerical integration algorithm with automatic result verification for definite integrals

Cites work

• A computer-verified monadic functional implementation of the integral
• Coquelicot: a user-friendly library of real analysis for Coq
• Double bubbles minimize
• Formally verified certificate checkers for hardest-to-round computation
• Introduction to Interval Analysis
• The Picard Algorithm for Ordinary Differential Equations in Coq
• Validated numerics. A short introduction to rigorous computations.
• Verification methods: rigorous results using floating-point arithmetic

Cited in

(9)

• Antiderivatives and integration
• Formally-verified round-off error analysis of Runge-Kutta methods
• Extensional constructive real analysis via locators
• Formally verified approximations of definite integrals
• A verified ODE solver and the Lorenz attractor
• Verified interactive computation of definite integrals
• Two adaptive Gauss-Legendre type algorithms for the verified computation of definite integrals
• Principles of verified numerical integration
• Proving Bounds on Real-Valued Functions with Computations

Describes a project that uses

Uses Software

• Coquelicot
• INTLAB
• Octave
• Coq

This page was built for publication: Formally verified approximations of definite integrals

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2829263)