A Formal Verification for Kantorovitch's Theorem

Ioana Pasca 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : Kantorovitch's theorem gives sufficient conditions for the convergence of Newton's method. We present a full formalization of this theorem in the case of a real function. The work is accomplished inside the Coq proof assistant and it is based on the Reals library provided by the theorem prover. For the general case of the theorem we first describe a way to represent concepts from multivariate analysis, as Coq does not offer such a library. We then discuss the proof of Kantorovitch's theorem based on this representation.
Type de document :
Communication dans un congrès
JFLA (Journées Francophones des Langages Applicatifs), Jan 2008, Etretat, France. pp.15-30, 2008
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00202808
Contributeur : Sandrine Blazy <>
Soumis le : mardi 8 janvier 2008 - 11:20:37
Dernière modification le : jeudi 11 janvier 2018 - 16:19:56
Document(s) archivé(s) le : jeudi 27 septembre 2012 - 13:51:07

Fichier

pasca.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00202808, version 1

Collections

Citation

Ioana Pasca. A Formal Verification for Kantorovitch's Theorem. JFLA (Journées Francophones des Langages Applicatifs), Jan 2008, Etretat, France. pp.15-30, 2008. 〈inria-00202808〉

Partager

Métriques

Consultations de la notice

224

Téléchargements de fichiers

593