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.

翻译：为了对采用有限元素方法的数值模拟程序进行校正获得最高信任,人们必须正式确定数学概念和结果,以便确定该方法的健全性。 Sobolev空间是一个数学框架,在这个框架中,可以说明部分衍生方程式最弱的配方,并寻求解决办法。这些功能空间建立在集成和计量理论之上。因此,功能分析中的本章是确定有限元素方法的强制性理论基石。本文件的目的是向正式证据界提供非常详细的笔纸证据,说明整合和计量理论的主要结果。