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.
Type de document :
Rapport
[Research Report] RR-7228, INRIA. 2010
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00463150
Contributeur : Ioana Pasca <>
Soumis le : mardi 14 décembre 2010 - 16:56:01
Dernière modification le : jeudi 11 janvier 2018 - 16:44:44
Document(s) archivé(s) le : vendredi 2 décembre 2016 - 17:43:56

Fichier

RR-7228.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

280

Téléchargements de fichiers

235