Skip to Main content Skip to Navigation

Formal Proofs for Theoretical Properties of Newton's Method

Ioana Pasca 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : We discuss a formal development for the certification of Newton's method. We address several issues encountered in the formal study of numerical algorithms: developing the necessary libraries for our proofs, adapting paper proofs to suit the features of a proof assistant, and designing new proofs based on the existing ones to deal with optimizations of the method. We start from Kantorovitch's theorem that states the convergence of Newton's method in the case of a system of equations. To formalize this proof inside the proof assistant Coq we first need to code the necessary concepts from multivariate analysis. We also prove that rounding at each step in Newton's method still yields a convergent process with an accurate correlation between the precision of the input and that of the result. An algorithm including rounding is a more accurate model for computations with Newton's method in practice.
Document type :
Complete list of metadata

Cited literature [25 references]  Display  Hide  Download
Contributor : Ioana Pasca Connect in order to contact the contributor
Submitted on : Tuesday, December 14, 2010 - 4:56:01 PM
Last modification on : Thursday, January 20, 2022 - 5:30:47 PM
Long-term archiving on: : Friday, December 2, 2016 - 5:43:56 PM


Files produced by the author(s)


  • HAL Id : inria-00463150, version 2



Ioana Pasca. Formal Proofs for Theoretical Properties of Newton's Method. [Research Report] RR-7228, INRIA. 2010. ⟨inria-00463150v2⟩



Les métriques sont temporairement indisponibles