Efficient and accurate computation of upper bounds of approximation errors

DOI10.1016/j.tcs.2010.11.052zbMath1211.65025OpenAlexW2092622802MaRDI QIDQ633637

J. Harrison, Ch. Lauter, Mioara Joldes, Sylvain Chevillard

Publication date: 29 March 2011

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://hal-ens-lyon.archives-ouvertes.fr/ensl-00445343/file/RRLIP2010-2.pdf

zbMATH Keywords

numerical examplestranscendental functionsapproximation errorsum of squaresvalidationformal proofmathematical functionscertificationTaylor modelssupremum normapproximation polynomialsautomated supremum norm algorithm

Mathematics Subject Classification ID

Computation of special functions and constants, construction of tables (65D20) Algorithms with automatic result verification (65G20) Elementary functions (26A09) Numerical approximation and evaluation of special functions (33F05) Exponential and trigonometric functions (33B10)

Related Items (12)

Sum of Squares Decompositions of Polynomials over their Gradient Ideals with Rational Coefficients ⋮ Dual Certificates and Efficient Rational Sum-of-Squares Decompositions for Polynomial Optimization over Compact Sets ⋮ Proving tight bounds on univariate expressions with elementary functions in Coq ⋮ Polynomials with bounds and numerical approximation ⋮ Floating-point arithmetic ⋮ A note on the computational complexity of the moment-SOS hierarchy for polynomial optimization ⋮ Pourchet’s theorem in action: decomposing univariate nonnegative polynomials as sums of five squares ⋮ Rigorous uniform approximation of D-finite functions using Chebyshev expansions ⋮ A validated real function calculus ⋮ Algorithms for weighted sum of squares decomposition of non-negative univariate polynomials ⋮ On exact Reznick, Hilbert-Artin and Putinar's representations ⋮ An algorithm for decomposing a non-negative polynomial as a sum of squares of rational functions

Uses Software

• ACETAF
• INTOPT_90
• TADIFF
• HOL Light
• GlobSol
• Cosy
• ISOLATE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Effective bounds for P-recursive sequences
• Rigorous global search: continuous problems
• Interval Newton iteration in multiple precision for the univariate case
• Efficient isolation of polynomial's real roots.
• Semidefinite programming relaxations for semialgebraic problems
• Taylor forms -- use and limits.
• Schwankung von Polynomen zwischen Gitterpunkten. (Oscillations of polynomials between lattice points)
• Motivations for an arbitrary precision interval arithmetic and the MPFI library
• Rigorous global search using taylor models
• Verifying Nonlinear Real Formulas Via Sums of Squares
• Formal Global Optimisation with Taylor Models
• Fast Algorithms for Manipulating Formal Power Series
• A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7^™ Processor
• A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
• Program result checking: A new approach to making programs more reliable
• The Arithmetic of Differentiation
• ACETAF

This page was built for publication: Efficient and accurate computation of upper bounds of approximation errors