Reynald Affeldt¹ and Cyril Cohen² ¹ National Institute of Advanced Industrial Science and Technology (AIST), Tokyo, Japan ² Université Côte d'Azur, Inria, Sophia Antipolis, France, Motivation and Contribution  Our goal is to add integration theory to MathComp-Analysis [1, 2], an extension of M ATHC OMP dedicated to classical analysis (topology, real and complex analysis, etc.). In this abstract, we report on the construction of the Lebesgue measure, which is a necessary and difficult step in the formalization of Lebesgue integration and its variants. The originality of our approach is the use of the mathematical structure of algebras of sets as a ground for Carathéodory's extension theorem. This is how the construction is often taught in undergraduate classes (here, we follow [5]) and we believe that this approach improves the modularity of the formalization because it favors abstract lemmas.  Beside this contribution, our experiment 1 leads us to extend M ATH C OMP - A NALYSIS with reusable support for sequences, series, and extended real numbers. It also takes advantage of the Hierarchy-Builder [3] tool and MATHCOMP’s interval.v. Construction of the Lebesgue Measure  The main mathematical definitions we introduce are σ- algebra and measure.  A σ-algebra is a set of sets that contains the empty set, and is stable by complement and by countably infinite union. Sets from a σ -algebra are said to be measurable. A measure μ is a non-negative function defined over a σ -algebra such that the measure of the empty set is 0 and such that μ(∪ i F i ) = ∑ i " μ( F i ) for any sequence F of pairwise-disjoint measurable sets. σ -algebras are also algebras of sets. An algebra of sets is simpler than a σ -algebra: it is a set of sets stable by complement and union, formalized below using H ierarchy-B uilder: HB.factory Record isAlgebraOfSets T := { measurable : set (set T) ; measurable0 : measurable set0 ; measurableU : V A B, measurable A → measurable B → measurable (A '|' B) ; measurableC : ∀ A, measurable A → measurable (~' A) }. We formalize the construction of the Lebesgue measure as the composition of three main results. The first result builds a σ -algebra and a measure over it given an outer measure μ (an outer measure is intuitively a "relaxed" definition of measure). The resulting σ -algebra is formed of Caratheodory- measurable sets, i.e., sets A such that ∀ X , μ ( X ) = μ ( X ∩ A ) + μ ( X ∩ Ā ). In order to obtain the Lebesgue measure, it suffices to apply this result to the outer measure given by the next result. The second result builds an outer measure given a measure defined over an algebra of sets. More precisely, the outer measure in question of a set X is defined as the infimum of the measures of covers inf {∑ i  µ(F i )|(∀ i , measurable(F i )) ∧ X ⊆ ∪ i F i }: Definition measurable_cover X := [set F | (V i, measurable (F i)) ∧ X ⊆ \bigcup_i (F i)]. Definition mu_ext mu X := ereal_inf [set \sum_(i <oo) mu (F i) | F in measurable_cover X]. We show that this outer measure coincides with the input measure mu. We also show that the application of the first result above to this outer measure produces a σ -algebra that contains all the measurable sets of the smallest σ -algebra that contains the algebra of sets.  To complete the construction of the Lebesgue measure, it now suffices to exhibit the Borel measure on the algebra of sets of finite unions of intervals. The third result is the construction of this Borel measure. It starts with the formalization of the algebra of sets of simple sets ( sset ), i.e., sets that can be covered by a finite union of intervals. In proving that such sets indeed form an algebra of sets, the technical part is the stability by complement, since the complement of an interval is not an interval in general. For this purpose we provide a decomposition procedure Decompose that turns a sequence of (possibly overlapping) intervals into a sequence of non- overlapping intervals with the same cover. The length slength of a simple set is easily defined: call the decomposition procedure to produce an equivalent sequence of non-overlapping intervals and sum their lengths. We then prove that slength is additive (this is not difficult since it does not involve infinite sums) and σ-additive, i.e., (fun n ⇒ \sum_(i < n) slength (F i)) — → slength (\bigcup_i F i) (under appropriate measurability and pairwise-disjointness for the sequence F ). This is the last technical step of the construction of the Lebesgue measure which we get by first proving that the length is actually σ -subadditive on the subclass of simple sets that corresponds to intervals. This is the main lemma and it is no surprise that it is indeed the focus point of many lecture notes we explored for the purpose of this work. It uses as an intermediate step the Borel-Lebesgue theorem that M ATH C OMP-A NALYSIS conveniently already had. Useful extensions to MathComp-Analysis   Since a measure is potentially infinite, it is represented by extended real numbers.  A prerequisite for the construction of the Lebesgue measure we have explained above was therefore the development of the theory of extended real numbers and of their sequences. This actually called for a substantial extension of the M ATH C OMP - A NALYSIS library. The latter provides sev- eral mathematical structures (topological, uniform, pseudometric spaces, normed modules, etc.)  together with the expected lemmas. It was therefore important to first equip extended real numbers with the structures available in M ATH C OMP - A NALYSIS , so as to enjoy already proved lemmas.  On the topological side, extended real numbers form a pseudometric space. On the algebraic side, ∞ − ∞ is undefined in the mathematical practice, but defining it to be −∞ is crucial because it makes the extended real numbers a commutative monoid, which enables the use of the bigop library. There is no hope to get a better structure on the full type though. Establishing these facts was the first step of our formalization of sequences of extended real numbers, which goes on by proving the expected lemmas such as the fact that the limit of a sum is the sum of limits (assuming the quantities involved are properly defined), etc. The first two results of the construction of the Lebesgue measure form Carathéodory's extension theorem.  Given our newly developed theory of sequences of extended real numbers, the proofs of the first result are almost a direct translation of pencil-and-paper proofs. However, the proof of the rest of Carathéodory's extension theorem is more technical in that it requires new developments about sequences of extended real numbers, namely the definitions of sums (of non-negative terms) over general sets, i.e., the notation ∑ i ∈ S α i . The latter is defined by sup { ∑ i ∈ F α i | F non-empty finite subset of S } , and generalizes the notation for the limit of sequences of extended real numbers. An important aspect of the third result (the construction of a measure over the algebra of sets of simple sets) is the procedure that decomposes a simple sets into non-overlapping intervals. This procedure uses an ordering of intervals which takes advantage of path.v, order.v, and the recently updated interval.v of MATHCOMP. As already emphasized above, lecture notes about the construction of the Lebesgue measure seem to emphasize the lemma showing the σ -additivity for intervals.  We found the generalization of σ -additivity from intervals to simple sets technically interesting. Indeed, it exhibits for example technical reindexings due to the combined used of infinite sums and infinite unions (that come from M ATHC OMP - A NALYSIS ) and finite sums and finite unions from M ATHC OMP 's bigop library. Isabelle/HOL [4] and Lean ( https://github.com/leanprover-community/mathlib) Related Work have different constructions of the Lebesgue measure respectively based on the gauge integral and on the Lebesgue outer measure. Neither of which formally applies the Carathéodory's extension theorem to an algebra of sets.