Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [2 references]  Display  Hide  Download
Contributor : Sandrine Blazy Connect in order to contact the contributor
Submitted on : Tuesday, January 8, 2008 - 11:20:37 AM
Last modification on : Thursday, January 20, 2022 - 5:30:45 PM
Long-term archiving on: : Thursday, September 27, 2012 - 1:51:07 PM


Files produced by the author(s)


  • HAL Id : inria-00202808, version 1



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



Record views


Files downloads