Rigorous numerics aims at providing certified representations for solutions of various problems, notably in functional analysis, e.g., differential equations or optimal control. Indeed, specific domains like safety-critical engineering or computer-assisted proofs in mathematics have stronger reliability requirements than what can be achieved by resorting to standard numerical analysis algorithms.
Our goal consists in developing efficient algorithms, which are also validated / certified in the sense that all numerical errors (method or rounding) are taken into account. Specifically, a central contribution is to combine polynomial approximations with a posteriori fixed-point validation techniques. A C code library for rigorous polynomial approximations (RPAs) is provided, together with a Coq formal proof development, offering the highest confidence at the implementation level.
After providing basic operations on RPAs, we focus on a new validation algorithm for Chebyshev basis solutions of D-finite functions, i.e., solutions of linear ordinary differential equations (LODEs) with polynomial coefficients. We give an in-depth complexity analysis, as well as an extension to general LODEs, and even coupled systems of them.
These symbolic-numeric methods are finally used in several related problems: a new lower bound on the Hilbert number for quartic systems; a validation of trajectories arising in the linearized spacecraft rendezvous problem; the design of evaluation error efficient polynomial approximations; and the support and density reconstruction of particular measures using algebraic techniques.
Gratuit
Disciplines