Skip to Main content Skip to Navigation
Reports

Lebesgue integration. Detailed proofs to be formalized in Coq

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 correct framework in which most partial derivative equations may be stated and solved. 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.
Complete list of metadatas

https://hal.inria.fr/hal-03105815
Contributor : Francois Clement <>
Submitted on : Thursday, January 14, 2021 - 4:27:05 PM
Last modification on : Wednesday, January 27, 2021 - 4:35:41 PM

Files

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

Identifiers

  • HAL Id : hal-03105815, version 1
  • ARXIV : 2101.05678

Citation

François Clément, Vincent Martin. Lebesgue integration. Detailed proofs to be formalized in Coq. [Research Report] RR-9386, Inria Paris. 2021, pp.284. ⟨hal-03105815⟩

Share

Metrics

Record views

110

Files downloads

165