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 :
Reports
Complete list of metadatas

Cited literature [25 references]  Display  Hide  Download

https://hal.inria.fr/inria-00463150
Contributor : Ioana Pasca <>
Submitted on : Tuesday, December 14, 2010 - 4:56:01 PM
Last modification on : Thursday, January 11, 2018 - 4:44:44 PM
Long-term archiving on : Friday, December 2, 2016 - 5:43:56 PM

File

RR-7228.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00463150, version 2

Collections

Citation

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

Share

Metrics

Record views

341

Files downloads

644