We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:


Current browse context:


Change to browse by:

References & Citations

DBLP - CS Bibliography


(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Lebesgue integration. Detailed proofs to be formalized in Coq

Authors: François Clément (SERENA, CERMICS), Vincent Martin (LMAC)
Abstract: To obtain the highest confidence on the correction of numerical simulation programs implementing the finite element method, one has to formalize the mathematical notions and results that allow to establish the soundness of the method. Sobolev spaces are the mathematical framework in which most weak formulations of partial derivative equations are stated, and where solutions are sought. These functional spaces are built on integration and measure theory. Hence, this chapter in functional analysis is a mandatory theoretical cornerstone for the definition of the finite element method. The purpose of this document is to provide the formal proof community with very detailed pen-and-paper proofs of the main results from integration and measure theory.
Subjects: Logic in Computer Science (cs.LO); Classical Analysis and ODEs (math.CA); Functional Analysis (math.FA)
Cite as: arXiv:2101.05678 [cs.LO]
  (or arXiv:2101.05678v2 [cs.LO] for this version)

Submission history

From: Francois Clement [view email]
[v1] Thu, 14 Jan 2021 15:53:18 GMT (1132kb,D)
[v2] Fri, 2 Apr 2021 07:32:24 GMT (1185kb,D)

Link back to: arXiv, form interface, contact.