Formal Proofs for Theoretical Properties of Newton's Method - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2010

Formal Proofs for Theoretical Properties of Newton's Method

Ioana Pasca
  • Function : Author
  • PersonId : 845903


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.
Fichier principal
Vignette du fichier
RR-7228.pdf (521.97 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

inria-00463150 , version 1 (11-03-2010)
inria-00463150 , version 2 (14-12-2010)


  • 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⟩
150 View
2763 Download


Gmail Facebook Twitter LinkedIn More