Measure Construction by Extension in Dependent Type Theory with Application to Integration

Abstract

We report on an original formalization of measure and integration theory in the Coq proof assistant. We build the Lebesgue measure following a standard construction that had not yet been formalized in proof assistants based on dependent type theory: by extension of a measure over a semiring of sets. We achieve this formalization by leveraging on existing techniques from the Mathematical Components project. We explain how we extend Mathematical Components’ iterated operators and mathematical structures for analysis to provide support for infinite sums and extended real numbers. We introduce new mathematical structures for measure theory and incidentally provide an illustrative, concrete application of Hierarchy-Builder, a generic tool for the formalization of hierarchies of mathematical structures. This formalization of measure theory provides the basis for a new formalization of the Lebesgue integration compatible with the Mathematical Components project.

1 Introduction

Measure theory and integration theory are major topics in mathematics with practical applications. For example, they serve as the foundation of probability theory whose formalization in proof assistants is used to verify information security (e.g., [1]) or artificial intelligence (e.g., [39]). It is therefore no wonder that the topic of formalization of measure and integration theory in proof assistants has already been tackled several times (e.g., [11, 12, 17, 26, 27]). In fact, experiments are still going on [45], some still dealing with the basics [14, 22].

Our motivation is to develop measure and integration theory on top of MathComp [33], a library of formalized mathematics developed using the Coq proof assistant [41]. The MathComp library consists of several algebraic theories that made it possible to formalize the Odd Order theorem¹ by following its published, revised proof [24, Sect. 6]. There are now several libraries that are built on top of MathComp, the main ones being made available as parts of the Mathematical Components project². Among them, MathComp-Analysis [2, 3] aims at taking advantage of the algebraic theories provided by MathComp to develop classical analysis (topology, real and complex analysis, etc.).

In this paper, we report on an original formalization of measure and integration theory. Our approach is to extend MathComp-Analysis with reusable theories while following textbook presentations [29, 32]. The best illustration is the construction of the Lebesgue measure that we formalize. This is a standard construction from a semiring of sets, using the Measure Extension theorem. To the best of our knowledge, it has never been formalized with the abstraction of ring of sets or semiring of sets in a proof assistant based on dependent type theory. Yet, its formalization is the occasion to develop new mathematical structures of general interest for Coq users. Similarly, the construction of the Lebesgue integral gives us the opportunity to develop a generic formalization of simple functions and to extend the formalization of the iterated operators of MathComp [10], one key to the successful formalization of the Odd Order theorem.

Our contribution in this paper is twofold. First, we bring to the Coq proof assistant a formalization of measure and integration theory that is compatible with the algebraic theories of MathComp. Second, we demonstrate recent formalization techniques developed in the context of the Mathematical Components project. In particular, we use Hierarchy-Builder [19] to formalize a hierarchy of mathematical structures for measure theory and to provide a compositional formalization of simple functions. Our technical contributions materialize as extensions to MathComp-Analysis in the form of reusable formal theories about sequences (of reals and of extended real numbers) and about sums over general sets and over finitely-supported functions.

1.1 Paper Outline

In Sect. 2, we explain how we develop the theory of extended real numbers by extending MathComp and MathComp-Analysis. In Sect. 3, we explain how we encode the basic definitions of measure theory, demonstrating the use of Hierarchy-Builder. In Sect. 4, we formalize the Measure Extension theorem which shows how to extend a measure over a semiring of sets to a $\sigma$-algebra. This is a standard and generic approach to the construction of measures. In Sect. 5, we obtain the Lebesgue measure by extending a measure over the semiring of sets of intervals. In Sect. 6, we show that the framework developed so far allows for a formalization of the Lebesgue integral up to the dominated convergence and Fubini’s theorems. We review related work in Sect. 7 and conclude in Sect. 8.

1.2 Note on Notation

The Mathematical Components project have been favoring ASCII notations. Most of them are unsurprising because they are inspired by LaTeX commands. This paper follows this tradition; ASCII notations will be explained in the prose or in Tables 1 and 2. As a consequence, we can display the Coq code almost verbatim; we allow pretty-printing only for a few standard symbols (such as instead of , instead of , instead of , instead of , instead of , instead of , Ł!/ instead of !/, etc.). The accompanying development [42] can be found online and we will refer to it as a citation possibly indicating the name of the relevant file (as in [42, file filename.v] ).

2 Support for Extended Real Numbers

Since a measure is potentially infinite, it is represented by extended real numbers. A prerequisite for the construction of measures is therefore the development of the theory of extended real numbers and of their sequences. This actually calls for a substantial extension of MathComp-Analysis [3].

Our starting point is the hierarchy of numeric and real interfaces provided by MathComp and MathComp-Analysis. It contains (among others) the type for numeric integral domains, the type for numeric fields, the type for real fields (see [18, Chapter 4]), and the type for real numbers. They form an inheritance chain as depicted in Fig. 1.

Fig. 1

Numeric types provided by MathComp and MathComp-Analysis used in this paper

The definition of extended real numbers is unsurprising (and predates the work presented in this paper):

Hereafter, the notation (resp. ) is for the constructor (resp. ). The constructor injects a real number into the set of extended real numbers; we also use the notation Ł!r

2.1 Algebraic Aspects of Extended Real Numbers

The expression $\infty -\infty$ is undefined in the mathematical practice. How to deal with this is a crucial aspect of our formalization. We define it to be $-\infty$ because it makes the extended real numbers a commutative monoid, so we can use MathComp’s iterated operators [10].

Furthermore, we can combine the iterated operators of MathComp with the notion of limit, which comes from MathComp-Analysis [3], to introduce a notation for infinite sums. On the one hand, MathComp comes with a generic definition of iterated operators

where is a function whose domain corresponds to the list of indices and is a boolean predicate. Depending on the properties of the binary operator and the element , many lemmas are available that have been key to important formalizations in Coq (e.g., [24]).

The notation

is a special case where the indices are the natural numbers less than . As for the notation

, it is a special case for the iterated addition when is a numerical type-valued function. On the other hand, MathComp-Analysis comes with a definition of limit [3, Sect. 2.3]. It can be applied to sequences, i.e., functions of type (notation ). Given a sequence , is the limit of the sequence $\texttt {u}_n$ when $n \rightarrow \infty$. We combine these two notations into a family of notations

, which is simply defined as

. Of course, these new notations need to be instrumented with many lemmas, the rest of this paper will provide several examples.

Table 1 contains a summary of the notations for iterated operators we have discussed so far.³

Table 1 Summary of iterated operators and alike used or newly introduced in this paper

2.2 Topological Aspects of Extended Real Numbers

MathComp-Analysis provides several mathematical structures (topological, uniform, pseudometric spaces, etc.) together with generic lemmas. To enjoy these lemmas, it is necessary to equip extended real numbers with these structures by showing they meet their interfaces.

Extended real numbers form a pseudometric space. The instantiation of the mathematical structures essentially relies on the definition and properties of an order-preserving bijective function from the set of extended real numbers to $[-1;1]$ (see [42, file constructive$\_$ereal.v] for details):

There is no hope to get a richer structure (say, MathComp’s Ł!zmodType!) on the full type though, because as we already discussed above $\infty -\infty$ is taken to be $-\infty$.

2.3 Sequences of Extended Real Numbers

The preparatory steps (Sects. 2.1 and 2.2) we briefly overviewed above are necessary to produce a theory about sequences of extended real numbers that blends in MathComp-Analysis in a satisfactory way. For the sake of illustration, let us present two sample lemmas. The first one shows that the limit of a sum is the sum of limits:

We already explained the notation in Sect. 2.1. See Fig. 1 for . The definition ( is for “convergence”) states that exists without naming it explicitly. The notation is a predicate that checks whether the addition of and is well-defined; the notation is for the pointwise addition of two functions.

The second illustrative lemma shows the commutation of finite and infinite sums of sequences of non-negative terms:

There are many lemmas dealing with sequences of extended real numbers that have been added to MathComp-Analysis for the purpose of this work (see [42, file sequences.v] and [42, file normedtype.v]). These are reusable lemmas that make the rest of our formalization possible.

2.4 Iterated Operators Over Finite Supports

To be able to succinctly formalize some proofs relying on iterated operators, we also extend the library of iterated operators of MathComp-Analysis with iterated operators over finite supports. They take the form of the notation

for the iterated application of the operator Ł!op! to Ł!f i!’s where ranges over and as a finite support.

The definition of the finite support of a function relies on a theory about the cardinality properties of sets that was also triggered by the work presented in this paper. From this theory, we use in particular the function ( returns a list when the set is indeed finite and the empty list otherwise) to define the finite support of a function:

The notation for iterated operators over finite supports combines this definition with MathComp’s iterated operators:

The integral of simple functions in Sect. 6.3 will provide a concrete use of this new notation.

Table 2 Summary of the set-theoretic notations used in this paper

2.5 Sums Over General Sets

Last, we extend MathComp-Analysis with sums over general sets, i.e.:

$$\begin{aligned} \sum _{i \in S} a_i \overset{\text {def}}{=}\sup \left\{ \sum _{i \in A} a_i \,\Big |\, A \text { finite subset of } S \right\} . \end{aligned}$$

For that purpose, we introduce the definition for the finite sets included in Ł!S!. It is defined using the predicate which is defined in such a way that when there is a natural number n such that there is bijection between and the set , i.e., when the set  is finite (see [42, file cardinality.v] for details). Using and the notation for iterated operators over finite supports from Sect. 2.4, the pencil-and-paper definition of sums over general sets translates directly:

The type is one of the numeric types of MathComp (see Fig. 1). The identifier corresponds to the supremum of a set of extended real numbers. The definition is equipped with the notation

of Table 1. It generalizes the notation for the limit of sequences of extended real numbers of Sect. 2.1. As an illustration of the theory of sums over general sets, let us consider the following partition property:

$$\begin{aligned} J_k \text { pairwise-disjoint} \rightarrow (\forall j, j \in \bigcup _{k \in K} J_k \rightarrow 0 \le a_j) \rightarrow \\ \sum _{i \in \bigcup _{k \in K} J_k} a_i = \sum _{k \in K} \left( \sum _{j \in J_k} a_j\right) . \end{aligned}$$

Here follows the corresponding formal statement, where the hypothesis about the pairwise-disjointness of the sets $J_k$ is slightly generalized (see Table 2 for notations):

This property will turn out to be useful when developing the Measure Extension theorem later in this paper.

3 Basic Definitions of Measure Theory

The main mathematical definitions for measure theory are $\sigma$-algebra and measure. The goal of the construction of the Lebesgue measure is to build a function that satisfies the properties of a measure. This is not trivial because such a function does not exist in general when the domain is an arbitrary powerset, hence the introduction of $\sigma$-algebras.

This section proposes a formalization of the basic definitions of measure theory using Hierarchy-Builder [19], a tool that automates the writing of packed classes [23], a methodology to build hierarchies of mathematical structures that is used pervasively in the Mathematical Components project.

3.1 Overview of Hierarchy-Builder

Hierarchy-Builder extends Coq with commands to define hierarchies of mathematical structures and functions. It is designed so that hierarchies can evolve (for example by splitting a structure into smaller structures) without breaking existing code. These commands are compiled to packed classes [23], but the technical details of their implementation in Coq (modules, records, coercions, implicit arguments, canonical structures instances, notations, etc.) are hidden to the user.

The main concept of Hierarchy-Builder is the one of factory. This is a record defined by the command that packs a carrier, operations, and properties. This record usually corresponds to the standard definition of a mathematical structure. Mixins are factories used as the default definition for a mathematical structure; they are defined by the command . Structures defined by the command are essentially sigma-types with a carrier paired with one or more factories. A mixin often extends a structure, so it typically takes as parameters a carrier and other structures.

Factories are instantiated using the command . Instances are built with an function which is automatically generated for each factory.

A builder is a function that shows that a factory is sufficient to build one or several mixins. To add builders, one uses the command that opens a Coq section which starts with postulating a factory instance and lets the user declare several instances of mixins as builders.

In addition to commands to build hierarchies, Hierarchy-Builder also checks their validity by detecting missing interfaces or competing inheritance paths [2]. More than an inheritance mechanism, Hierarchy-Builder therefore provides help in the design of hierarchies of structures.

3.2 Mathematical Structures for Measure Theory

A $\sigma$-algebra is a mathematical structure that comprises a set of sets that contains the empty set, and is stable by complement and by countable union. It is best defined as a hierarchy of mathematical structures because more general structures actually play a key role in the construction by extension of the Lebesgue measure.

3.2.1 Inheritance Chain from Semiring of Sets

The hierarchy of mathematical structures for measure theory starts with semirings of sets. They are formalized using Hierarchy-Builder (see Sect. 3.1) as follows:

The declaration of the mixin starts at line 1. The parameter  is what we call a display parameter. It can be ignored on a first reading because it is not used in the definition; it is used to implement user-friendly notations as will be explained in Sect. 3.4 where we will have enough material to demonstrate its use with a concrete example. Line 2 corresponds to the carrier. A semiring of sets contains the empty set (line 3). It is also stable by finite intersection; this is captured by line 4, where is formally defined as . At line 5, means that the relative complement of two sets in can be partitioned into a finite number of sets in :

The definition of semiring of sets is completed at line 8 by declaring the structure (as explained in Sect. 3.1) and providing a conventional notation for the corresponding type (line 7). Hereafter, we call measurable sets the sets that form a semiring of sets.

A ring of sets is a non-empty set of sets that is closed under union and difference. It can be defined by extending a semiring of sets with the axiom that it is stable by finite union. Its interface can be defined using Hierarchy-Builder as follows:

This declaration provides a new mixin that extends the mixin for semiring of sets (note the declaration at line 2). At line 3, the expression means that the class is stable by finite unions and is formally defined as . The modifier at line 3 is Coq syntax to enforce the explicit input of implicit arguments. The corresponding structure is declared at line 6 where it is marked as satisfying the mixin and extending the structure of semiring of sets (line 7).

An algebra of sets is a set of sets that contains the empty set and is stable by (finite) union and complement. Algebras of sets are defined as extending rings of sets with the axiom that the full set belongs to the set of measurable sets. The Hierarchy-Builder declaration is similar to the one of semiring of sets and ring of sets:

Finally, $\sigma$-algebras are defined by extending algebras of sets with the axiom of stability by countable union:

These definitions form an inheritance chain (Fig. 2), so that $\sigma$-algebras are also algebras of sets, which are also rings of sets, and therefore semirings of sets.

Fig. 2

Inheritance chain from semiring of sets to $\sigma$-algebra’s

3.2.2 Direct Definition of Mesurable Spaces

The set of interfaces provided by the hierarchy of mathematical structures for measure theory is not the only way to instantiate structures. We also provide factories (introduced in Sect. 3.1). For example, the following factory provides an alternative interface for $\sigma$-algebras:

It is arguably closer to the textbook definition that we gave at the beginning of Sect. 3.2. In fact, though it may seem at first sight that mixins provide the definition of mathematical structures, we have observed in practice that the standard textbook definition often ought better be sought in factories provided afterwards.

3.3 Generated $\sigma$-algebras

The notion of generated $\sigma$-algebra will come in handy to define the Measure Extension theorem and to develop the theory of measurable functions. The generated $\sigma$-algebra is the smallest $\sigma$-algebra that contains the set of sets , such that the complement is taken w.r.t. a set . This is defined using a generic Ł+smallest+ predicate:

Below, the notation is for the measurable sets of the $\sigma$-algebra generated from the set of sets with complement take w.r.t. the full set.

Note that the definition is well-defined (i.e., is indeed the smallest set in the class ) whenever the smallest fixpoint of the class indeed exists. This is why the definition of a generated $\sigma$-algebra can also be found elsewhere [14, Sect. 4.2] defined as an inductive predicate instead. The choice of using the predicate rather than an inductive definition is for the sake of genericity: we have a unique function symbol and a common theory to deal with all generated classes (Dynkin, $\sigma$-algebra, etc.), and since itself is monotonous, we can reduce comparison of generated classes to the extent of the classes themselves. However, this has the drawback that the elimination principle and correctness lemmas are not automatically proven by Coq as they would with the command.

Since the set of sets of type forms a $\sigma$-algebra we can equip it with the structure of from Sect. 3.2.1. The temptation would be to give a definition to the measurable type generated by . However, for the sake of modularity it is a common practice in the MathComp libraries to define a type alias of (of type , i.e., it contains at least one element) with  as a phantom argument and provide a inferable instance of measurable type on this alias. Hence we introduce a dedicated identifier (line 1 below) to alias and a dedicated display parameter (line 7) (remember from Sect. 3.2.1 that mathematical structures for measure theory are parameterized by a display parameter to be explained in Sect. 3.4). Let us furthermore assume that we are given the proofs

corresponding to the $\sigma$-algebra properties of a generated $\sigma$-algebra. To associate to the identifier a structure of $\sigma$-algebra, we use the Hierarchy-Builder command . At line 8, it equips with a structure of pointed type ( replicates the pointed type structure of the underlying type, here ). At line 9, it is used with the constructor of the factory of Sect. 3.2.2. The corresponding display appears at line 10 and the proofs of the $\sigma$-algebra properties appear at lines 12–13.

3.4 Displays for Measurable Types

We saw in the previous sections that the structures for measure theory are parameterized by a display parameter. Its purpose is to disambiguate the printing of expressions of the (input) form Ł!measurable A!. This is useful when several of them appear in the same local context or when does not provide enough information to infer the right measurable type.

More concretely, let us consider the basic case of a measurable type  with display  (e.g., ). To assert that a set is measurable, one can always write . Yet, the display mechanism is such that Coq prints back . This is achieved by providing a type for displays (line 1) and a notation (line 6):

The display mechanism can be used to disambiguate expressions. Let us consider the case of generated $\sigma$-algebra’s. We saw that the display for generated $\sigma$-algebra’s is parameterized by the generator set ( in the previous section—Sect. 3.3). We can therefore introduce a notation for the display associated with the generator set and a notation for the measurable sets of the $\sigma$-algebra generated by :

For example, we can use these notations to regard the empty set as a member of the $\sigma$-algebra generated by any set :

In comparison, the input would not type check, because does not have a default instance to give a meaning to .

3.5 Functions on Classes of Sets

There are several notions of functions from classes of sets to the real numbers (or, implicitly, extended reals) which fall under the umbrella name of “measure”. In the literature, they are named contents (a.k.a. additive measures), premeasures, outer measures, $\sigma$-subadditive measures, and $\sigma$-additive measures (a.k.a. measures). We define predicates for all of these notions, but we only define structures for the three most useful: contents, measures, and outer measures.

3.5.1 Contents

A content (or an additive measure) $\mu$ is a non-negative function defined over a semiring of sets such that the measure of the empty set is 0 and such that $\mu (\cup _{k=1}^n F_k) = \sum _{k=1}^n \mu (F_k)$ for a finite number of pairwise-disjoint measurable sets F. We first provide a definition for the latter condition:

The pairwise-disjointness of sets is captured by the generic predicate (Table 2). Asking $\cup _{k=1}^n F_k$ to be measurable is superfluous when taken on a ring of sets. Contents are eventually defined by the following mixin and structure:

See Fig. 1 for the type . In the Coq code, the type of contents is denoted by

.

An essential property of contents is that they can be extended from a semiring of sets $\mathcal {S}$ to its generated ring of sets $R(\mathcal {S})$. We can define the latter similarly to how we defined generated $\sigma$-algebras in Sect. 3.3:

The predicate is for stability by set difference and is defined by

.

A generated ring of sets can be equipped with a canonical structure of ring of sets. It happens that the measurable sets of these generated rings of sets can in fact be expressed as the finite disjoint unions of (non-empty) sets from the original semiring of sets $\mathcal {S}$ ( in the lemma below indicates sets from the generated ring of sets):

Thanks to this lemma, we can make this decomposition explicit by the following function , which given a set A in $R(\mathcal {S})$ returns a finite set of sets in $\mathcal {S}$ that cover A:

The function is written in an idiomatic way to retrieve in Coq a witness from an existential proof. The identifier comes from MathComp-Analysis and is a strong version of the law of excluded middle [3, Sect. 5.2]; is the axiom of constructive indefinite description.

Using , we can extend the function over the original semiring of sets by summing the components:

We thus have a function for all functions , which is equal to on the sets of the semiring of sets where is defined, and which is a content on the generated ring of sets when is a content (section in [42, file measure.v]), and which is $\sigma$-additive if is $\sigma$-subadditive (lemma ). Furthermore, using the latter fact we prove that when is $\sigma$-subadditive on a semiring of sets, it is in fact $\sigma$-additive (lemma ).

3.5.2 Measures

A measure $\mu$ is defined similarly to a content. The difference is the additivity axiom: it is such that $\mu (\cup _k F_k) = \sum _k \mu (F_k)$ for any sequence F of pairwise-disjoint measurable sets. We provide a definition for the latter condition, but generalizing it for semirings of sets by requiring the union $\cup _k F_k$ to be measurable as a precondition, thus merging the notions of measure and premeasure into one:

The notation is a notation for convergence of functions that comes from MathComp-Analysis [3]. In particular, when holds, we have using the notation of Sect. 2 (provided that the range of the function is a separated space, which is the case for the functions considered in this section). Note that in the definition above the precondition

holds unconditionally whenever we know that the underlying type is a $\sigma$-algebra.

We use this definition to define the mixin corresponding to measures, which extends the one for contents:

In practice, to construct a measure, one would rather use the following factory (we introduced the notion of factory in Sect. 3.2.2) whose interface is closer to the textbook definition of measure:

The notation

corresponds to the type of measures.

3.5.3 Outer Measures

Outer measures are the object of study of the measure extension theorems. Contrarily to a measure, an outer measure is $\sigma$-subadditive on the full powerset rather than on a specific class of sets.

Compared to $\sigma$-additivity, in $\sigma$-subadditivity the relation between the measure of the countable union and the sum of the measures is an inequality, there are no conditions on the sequence of sets, and the support type need not be a $\sigma$-algebra. Like for contents and measures (Sects. 3.5.1 and 3.5.2), we encode an outer measure as a Hierarchy-Builder mixin:

The notation

is a generic MathComp notation for homomorphisms with respect to the relations and . The type of outer measures comes with the notation

.

4 Measure Extension

A standard approach to the construction of measures is to extend a function over a semiring of sets, a ring of sets, or an algebra of sets to a measure over an enclosing $\sigma$-algebra. These extension theorems are known under different names (Carathéodory/Carathéodory-Fréchet/Carathéodory-Hopf/Hopf/Hahn/Hahn-Kolmogorov/etc. extension theorems). In the following, we explain the formalization of a version starting from semiring of sets and refer to it as the Measure Extension theorem.

As in the textbooks we follow [29, 32], we decompose the Measure Extension theorem in reusable constructions and lemmas. The first, which we refer to as the outer measure construction, extends a non-negative function $\mu$ such that $\mu (\emptyset ) = 0$ over a semiring of sets $\mathcal {S}$ to an outer measure (Sect. 4.1). This is then shown to be a measure over the $\sigma$-algebra of Carathéodory-measurable sets (Sect. 4.2). When restricted to this $\sigma$-algebra, we call it the Carathéodory measure. Now, if $\mu$ was a $\sigma$-subadditive content on $\mathcal {S}$, the $\sigma$-algebra of Carathéodory-measurable sets contains the $\sigma$-algebra generated by $\mathcal {S}$, and the Carathéodory measure is uniquely determined on it, by the values of $\mu$ on $\mathcal {S}$ (Sect. 4.3).

4.1 Outer Measure Construction

The first part of the Measure Extension theorem builds an outer measure (Sect. 3.5.3) given a function defined over a semiring of sets. In textbooks it is often stated in a weaker form starting from a ring of sets or an algebra of sets. The outer measure in question is more precisely defined as the infimum of the measures of covers, i.e., $\inf _F\left\{ \sum _{k=0}^\infty \mu (F_k) \,\text {|}\, (\forall k, \texttt {measurable}(F_k) ) \wedge X \subseteq \bigcup _k F_k\right\} .$ The definition of these coverable measures translates directly in MathComp-Analysis:

We use to define the desired outer measure:

The identifier corresponds to the infimum of a set of extended real numbers. In the following, is noted .

The difficulty to show that is an outer measure is to show that it is $\sigma$-subadditive (remember that we are working under the hypotheses that and that is non-negative). A typical textbook proof [32, Sect. X.1] [29, Lemma 1.47] translates to a proof script of 54 lines of code (lemma , [42, file measure.v]). The main technical point is the use of sums over general sets. Precisely, in the course of proving $\sigma$-subadditivity, we run into a subgoal of the following shape ($\mu ^*$ is the outer measure under construction):

$$\begin{aligned} \mu ^*(\cup _i F_i) \le \sum _i^\infty \left( \mu ^*(F_i) + \frac{\varepsilon }{2^i}\right) . \end{aligned}$$

The proof goes on by showing $\mu ^*(\cup _i F_i) \le \sum _{i,j} \mu (G_i j) \le \sum _i \sum _j \mu (G_i \, j)$ for some well-chosen G, such that $F_i \subseteq \cup _j G_i j$ and $\sum _j \mu (F_i j) \le \mu ^*(F_i) + \varepsilon /2^i$. This proof can be completed with the partition property using sums over general sets from Sect. 2.5.

Coming back to , we also show that it coincides with the input measure  (lemma in [42, file measure.v]).

4.2 From an Outer Measure to a Measure

The second part of the Measure Extension theorem builds, given an outer measure, a $\sigma$-algebra and a measure over it. The resulting $\sigma$-algebra is formed of Carathéodory measurable sets, i.e., sets A such that $\forall X, \mu ^*(X)=\mu ^*(X\cap A) + \mu ^*(X\cap \bar{A})$ where $\mu ^*$ is an outer measure. Hereafter, the set of Carathéodory measurable sets for an outer measure will appear as the notation .

Given our newly developed theory of sequences of extended real numbers (Sect. 2.3), proving, for an outer measure , that is actually a $\sigma$-algebra is essentially a translation of standard pencil-and-paper proofs (see lemmas in [42, file measure.v]). Hereafter, the $\sigma$-algebra of Carathéodory measurable sets is denoted by (this notation is implemented using the display mechanism explained in Sect. 3.4).

Similarly, proving that the restriction of the outer measure to the $\sigma$-algebra is a measure is also essentially a direct translation of standard pencil-and-paper proofs (see lemmas

).

Finally, we formally prove a number of properties about the resulting measure, in particular that it is complete, i.e., negligible sets are measurable. Let  be a semiring of sets and be a . A set N is negligible for $\mu$ when there exists a measurable set A such that $\mu (A)=0$ and $N \subseteq A$:

Let    be a notation for “  is negligible”. The formal definition of a complete measure follows:

4.3 The Measure Extension Theorem

Finally, we show that a measure over a semiring of sets can be extended to a measure over a $\sigma$-algebra that contains all the measurable sets of the smallest $\sigma$-algebra containing the semiring of sets. We place ourselves in the following context:

In this context, we can build an outer measure using the results of Sect. 4.1 and its $\sigma$-algebra using the results of Sect. 4.2. We can show that this $\sigma$-algebra contains all the measurable sets generated from the semiring of sets:

Recall from Sect. 3.4 that corresponds to the $\sigma$-algebra generated from and that in our context corresponds to the measurable sets of the semiring of sets . As for , we saw in Sect. 4.2 that it corresponds to the $\sigma$-algebra of Carathéodory measurable sets for the outer measure .

We use this last fact to build a measure over the $\sigma$-algebra generated from the semiring of sets: this is the final result of the Measure Extension theorem (recall from Sect. 3.3 that is the measurable type generated by ):

The proofs

correspond to the properties of a measure as explained in Sect. 3.5.2. See [42, file measure.v] for details.

Furthermore, we prove that the measure extension is unique. This requires to prove beforehand the uniqueness of measures [42, lemma measure$\_$unique]. We use monotone classes for that purpose [32, Sect. V.2.1]. This can also be proved using the equivalent notion of Dynkin systems (as mentioned in [26], which we also formalized in [42, file measure.v]). The uniqueness of measure extension is under the condition that the measure is $\sigma$-finite, i.e., the full set can be covered by a countable union of sets of finite measure:

When this holds for the measure of the measure extension, any other measure that coincides with on the original semiring of sets also coincides with the measure extension over the generated $\sigma$-algebra:

Since $\sigma$-finite measures are actually pervasive in measure theory, we extend using Hierarchy-Builder the hierarchy of structures for contents and measures of Sects. 3.5.1 and 3.5.2 with a structure for contents that are $\sigma$-finite and a structure for measures that are $\sigma$-finite. In particular, hereafter,

is a notation for the type of $\sigma$-finite measures.

5 Construction of the Lebesgue Measure over a Semiring of Sets

In this section, we explain how we derive the Lebesgue measure from the semiring of sets of intervals of the form ]a, b] using the measure extension from the previous section.

5.1 The Semiring of Sets of Intervals

In MathComp, the type , where is typically an ordered type, is defined as the pairs of bounds of type :

The constructor is for open or closed bounds, is for infinite bounds. How the boolean parameter distinguishes between open and closed bounds is better explained with illustrations. For example, the left bounds of the intervals and are respectively and , while the right bound of the interval is .

Let us define a type alias for of type and the following set of open-closed intervals:

This set forms a semiring of sets. Indeed, it contains , it is closed under finite intersection, and it satisfies the predicate from Sect. 3.2.1 (proofs $\texttt {ocitv\{0,I,D\}}$ below):

5.2 Construction of the Lebesgue Measure

The length of an interval is defined by subtracting its left bound from its right bound. For the sake of generality, this is formally defined over arbitrary sets for which we take the hull using (see [42, file normedtype.v] for the definition of ):

Now, the function is a content on the semiring of sets of intervals. Indeed, it is non-negative (proof below), and, more importantly, it is additive over :

Moreover, is also $\sigma$-subadditive over , and hence a measure:

We obtain the Lebesgue measure as an application of the measure extension from Sect. 4.3. More precisely, we use the generic definition to define the function corresponding to the Lebesgue measure, and it is directly a measure from Sect. 4.3.

The above construction provides a unique measure that applies to a $\sigma$-algebra generated from open-closed intervals (remember the use of in Sect. 4.3), which include the Borel sets: this is the definition of the Lebesgue measure.

We have not introduced an explicit definition for Borel sets but their $\sigma$-algebra can be denoted by which is a notation that combines the definition of the set of open-closed intervals and the notation that we introduced in Sect. 3.4. This $\sigma$-algebra can easily be shown to be the same as the one generated by open intervals:

Similarly, it can be shown to be the same as the one generated by open rays, etc. Furthermore, it can also be easily extended to a $\sigma$-algebra over extended real numbers. These facts (whose formal proofs can be found in [42, file lebesgue_measure.v]) are useful to establish the properties of measurable functions in the next section.

6 Construction of the Lebesgue Integral

We now show that the infrastructure we have developed for the Lebesgue measure can be used to develop the theory of the Lebesgue integral up to Fubini’s theorem, which covers the typical set of properties that demonstrate the usefulness of such a formalization. This experiment improves in particular on related work in Coq by providing theorems for functions that are not necessary non-negative and that are extended-real valued, and also be experimenting with simpler encodings, in particular the one of simple functions. Hereafter, we shorten code snippets with the following convention: has type for some display parameter , has type , and is a measure of type

.

6.1 Mesurable Functions

Ultimately, the Lebesgue integral is about measurable functions. A function is measurable when any preimage of a measurable set is measurable. We defined it for functions with domain  as follows:

Note that when in the above definition or are actually or

with , a concrete instance of $\sigma$-algebra need to have been declared beforehand as explained in Sect. 5.2.

6.2 Simple Functions

The construction of the Lebesgue integral starts with simple functions. A simple function f is typically defined by a sequence of pairwise-disjoint and measurable sets $A_0, \ldots , A_{n-1}$ and a sequence of elements $a_0, \ldots , a_{n-1}$ such that $f(x) = \sum _{k=0}^{n-1} a_k{\textbf {1}}_{A_k}(x)$. It might be tempting (in particular for a computer scientist) to encode this definition using lists to represent the range of simple functions. This actually turns out to be detrimental to formalization (see Sect. 7). Instead, we strive for modularity by obtaining simple functions from even more basic functions. For that purpose, we again put Hierarchy-Builder to good use. We first define functions with a finite image (notation ):

We then package measurable functions (notation ):

As a consequence, simple functions (notation ) can be defined by combining both functions with a finite image and measurable functions:

Similarly, we introduce non-negative functions (notation ) and define non-negative simple functions (notation ) resulting in the hierarchy displayed in Fig. 3.

Fig. 3

Definition of non-negative simple functions

The introduction for the above collection of types is a fertile ground for the formalization of the properties of simple functions. We show in particular that simple functions form a ring structure (a Ł!comRingType! in MathComp’s parlance) and thus that they can be combined accordingly (see [42, file lebesgue_integral.v]).

Among all the simple functions, indicator functions (notation , where is a set) are of particular interest because they are used pervasively in the theory of integration:

(Ł+In particular, any function with a finite image (and thus any simple function) is a linear combination of indicator functions:

This fact is instrumental in proofs using the monotone convergence theorem, such as Fubini’s theorem (Sect. 6.5).

6.3 The Integral of Simple Functions

The integral of a simple function is the sum of its images multiplied by the measure of the associated preimage. In textbooks, the corresponding formula can be written in two ways. One can make explicit the finite image of the simple function and sum w.r.t. the indices, i.e., as $\sum _{k=0}^{n-1} a_k\mu (A_k)$ using the notations from the previous section and some measure $\mu$. Since the image of a simple function is finite, one can alternatively use sums over finite supports (Sect. 2.4) and write: $\sum _{x \in \mathbb {R}} x \, \mu (f^{-1}\{x\})$. From the viewpoint of formalization, the former reveals implementation details while the latter is more compact and allows for the following simple definition of the integral of simple functions:

See Fig. 1 for . The development of the properties of the integral of simple functions goes on by establishing the properties of the integral of non-negative simple functions such as semi-linearity, monotonicity, etc. Among them, the fact that the integral of the sum of simple functions is the sum of the integrals is the most technical result. Yet, it can be proved within 23 lines of script using generic properties of sums over finite supports (see ⁴ [42, file lebesgue_integral.v]).

6.4 Integral of Measurable Functions

The integral of a measurable function is defined as the difference between its non-negative part and its non-positive part, both considered as non-negative functions. We therefore first temporarily define the integral of a non-negative measurable function, as the supremum of the integrals of smaller non-negative simple functions:

Regarding the definition of the integral of a measurable function, we make the design choice to have it parameterized with the domain of integration. For that purpose, we introduce the notation

for the function that behaves as over the set and 0 elsewhere. The definition of the integral follows (notation

):

In the code just above, the notation is for $\lambda x. \max (\texttt {f}(x),0)$ and the notation is for $\lambda x. \max (-\texttt {f}(x),0)$.

See [42, file lebesgue_measure.v] for the development of the theory of integration as presented in [32], and the next section for two illustrative examples.

6.5 Dominated Convergence and Fubini’s Theorem

The dominated convergence theorem establishes the convergence of a sequence of integrals of functions $f_n$ given an hypothesis of pointwise convergence of the functions $f_n$ and an hypothesis of domination by an integrable function; these two hypotheses are true “almost everywhere”. The standard presentation (e.g., [32, Sect. IV.2]) is to first prove the theorem when the hypotheses are unconditionally true, in which case the proof is essentially a consequence of Fatou’s lemma and of the linearity properties of the integral. As for the generalization to hypotheses that are true “almost everywhere”, it is almost always only sketched in textbooks. The complete statement of the dominated convergence theorem follows. The notation {} means that holds almost everywhere for the measure , i.e., that the complement of the set defined by is negligible as defined in Sect. 4.2.

Note that in this version of the dominated convergence theorem we assume that is measurable; this hypothesis is not needed when is complete.

Fubini’s theorem is a commutation result about integration. It is a good testbed for a combined formalization of measure and integration theory because, on the one hand, it requires the construction of the product measure, and, on the other hand, its proof relies on several lemmas about integration. Given two measures and respectively over two measurable types and , being $\sigma$-finite, the product measure

is defined as

where is the set of pairs in . In virtue of the uniqueness of measures (Sect. 4.3), inverting the role of and actually gives rise to the same measure. For the proof of Fubini’s theorem, we follow the presentation by Li [32, Sect. V.3], which is standard. The first step is to prove Fubini-Tonelli’s theorem, which is essentially Fubini’s theorem for non-negative functions. The decomposition of functions with a finite image into a linear combination of indicator functions (Sect. 6.2) comes in handy to prove Fubini-Tonelli’s theorem because the latter is first established for indicator functions, then for simple functions, and finally for measurable functions. The second main ingredient is the monotone convergence theorem [42, file lebesgue_integral.v]. Fubini’s theorem is then essentially an application of Fubini-Tonelli’s theorem:

7 Related Work

7.1 About Measure and Integration Theory in Proof Assistants Based on Dependent Type Theory

We are not aware of any formalization of the measure extension theorem for general semirings of sets in a proof assistant based on dependent type theory (neither Coq nor Lean).

There is a formalization in Coq, based on the Coquelicot library, of the Lebesgue integral of non-negative functions [14]. This development is driven by detailed pencil-and-paper proofs written for the purpose of formalization [16]. The theory of Lebesgue integration has been limited to non-negative functions and stops at Tonelli’s theorem [13] but it has recently been extended with a formalization of the Bochner integral [15]. The authors have communicated to us that there is work in progress on the Lebesgue measure but that it is not a modular construction like ours.

The difference between the work by Boldo et al. and our work lies more in the sustaining infrastructure than in the gallery of theorems. First, we cannot reuse their framework because of many diverging choices of conventions, one of them is assuming that $\infty - \infty = 0$, which results in the addition of the extended real numbers being non-associative, which prevents the use of iterated operators à la MathComp [14, Sect. 3.2]. We also insist on developing abstractions and components developed along MathComp-Analysis so as to find the best encodings. For example, Boldo et al. use a very concrete encoding of simple functions whose ranges are represented by sorted lists [14, Sect. 6.3]. Notwithstanding the fact that sorting is not essential to develop integration theory, it appears that this makes for longer proofs. For example, we already discussed the benefits of the infrastructure of iterated operators over finite supports (Sect. 2.4) regarding the proof that the integral of the sum of simple functions is the sum of the integrals (Sect. 6.3). The approach by Boldo et al. seems to make for a five times longer script (118 vs. 23 lines of codes, see ⁵ [30, file simple$\_$fun.v]). Another example having a predicate or a Ł+measurableType+ structure while Boldo et al. use the fact that a class of sets is a $\sigma$-algebra if and only if it is equal to the smallest $\sigma$-algebra generated by its elements. We found this characterization impractical in the presence of the hierarchy of classes of sets, for which we need inheritance to work in order to share theorem across structures. With an inductive characterization, theorems defined on a larger class of sets (e.g., semiring of sets) could not be applied to a $\sigma$-algebra. On a related note, our definition of generated $\sigma$-algebra in Sect. 3.3 generalizes the one by Boldo et al. by defining the complement with respect to an arbitrary set instead of the full set. This is very useful in practice to develop the theory of measurable partial functions and in fine define the Lebesgue integral as parameterized by a domain (Sect. 6.4).

The C-Corn library also deals with the formalization of integration in Coq as it has a formalization of the fundamental theorem of calculus [21] but this is about the Riemann integral and it is in a constructive setting.

The coq-proba library [38] provides a formalization of the Lebesgue measure and integral but limited to real-valued functions and closed intervals.

Lean has an extensive formalization of measure and integration theory. The main source of documentation is the code of mathlib [43]. To our understanding, measures are defined as a special case of outer measures [45], following the idea than any non-negative function can generate an outer measure which in turn can generate the $\sigma$-algebra of its Carathéodory measurable sets. Hence mathlib does not have a hierarchy of classes of sets reflecting the literature, as we did (Sect. 3.2), even though we believe that they naturally occur inside the proofs. mathlib provides the Lebesgue integral and its standard lemmas up to Fubini’s theorem and the Radon-Nikodým theorem (which we have also recently proved using our framework [28]), and is actually further generalized to the Bochner integral. It has also supported the formalization of the Haar measure [45], which generalizes the Lebesgue measure.

We are not aware of a formalization of the Lebesgue measure or integral in Nuprl [20] or Agda [40] which are also proof assistants based on dependent type theory.

7.2 About Measure and Integration Theory in Proof Assistants of the HOL Family

The HOL family of proof assistants has several formalizations of measure and integration theory. It can be traced back to a formalization of measure theory in HOL in 2002 [27, Sect. 2.2.2] (work actually inspired by earlier work in Mizar [11]). It was generalized in HOL4 in 2010 [17, Sect. 2.3] and used to formalize Lebesgue integration [17, 35]. Work in HOL4 triggered a port in Isabelle/HOL that was eventually reworked in 2011 [26, Sect. 4.2]. The Lebesgue measure is defined in Isabelle/HOL using the gauge integral that was already available in Isabelle/HOL, i.e., it is not built as an extension of a premeasure [26, Sect. 4.6]. This approach results from a port from HOL-Light [25].

7.3 Measure and Integration Theory in Other Proof Assistants

Proof assistants we have discussed so far are based on the LCF approach which consists in having a small kernel to ensure the soundness of proof checking. Other proof assistants based on an augmented trusted base providing more automation have also been used to formalize measure and integration theory.

The Mizar Mathematical Library (MML) [9] provides a formalization of measure theory that can be traced back to 1992 [11]. The Lebesgue measure in MML has recently been reconstructed [22] using an approach by extension from a semialgebra of intervals to fix an earlier formalization [12]. This is of course in a very different setting compared to our work in Coq since the Mizar proof assistant relies on the Tarski-Grothendieck set theory instead of dependent type theory.

NASALib [44] also provides a construction of the Lebesgue measure by extension but where extension is carried out from an algebra of sets [44, file hahn$\_$kolmogorov.pvs] instead of a semiring of sets as we do. NASALib is written in PVS [36], an interactive and automated prover based on higher-order logic that provides predicate subtyping and dependent types [37]. The formalization of measure theory and Lebesgue integration has been initiated in 2007 [31].

To the best of our understanding, in Metamath [34], the Lebesgue measure is not defined by extension.⁶

We did not find a formalization of the Lebesgue measure or integration in other mainstream theorem provers such as ACL2 or ProofPower, which seems to be confirmed by the “Formalizing 100 Theorems” list [46].

8 Conclusion

This paper introduced a Coq formalization of measure theory and Lebesgue integration that is compatible with MathComp and that extends MathComp-Analysis. This includes an original formalization of mathematical structures for measure theory (Sect. 3.2), an original formalization of the construction of measures using the Measure Extension theorem (Sect. 4.3), whose application to a measure over a semiring of intervals yields the Lebesgue measure (Sect. 5). This also allows for the construction of the Lebesgue integral and the formalization of its theory up to Fubini’s theorem (Sect. 6).

We argued about technical aspects of this formalization that we believe improve on related work (Sect. 7). At the beginning of this experiment, much work was dedicated to the formalization of structures for measure theory and to enrich the foundations (in particular, extended real numbers). Our development now provides new reusable libraries of general interest, in particular for extended real numbers and their sequences (Sect. 2), sums over finite supports (Sect. 2.4) and over general sets (Sect. 2.5). As concrete applications that illustrate the reusability of our formalization, we can mention the Lebesgue-Stieltjes measure, which could be formalized using the same approach we used for the Lebesgue measure in Sect. 5 [7], more standard results about measure theory such as the Radon-Nikodým theorem [8], and the formalization of the semantics of a probabilistic programming language [4].

8.1 Current and Future Work

The Coq community now has several formalizations of integration, that rely on different grounds. We have been exchanging with the members of the MILC project [30] to look for ways to share the development effort. As a next step of our formalization, we plan to formalize the fundamental theorem of calculus for the Lebesgue integral to connect with the theory of derivatives of MathComp-Analysis. We have also started formalizing probability theory and in particular discrete random variables to generalize existing work on the formalization of discrete probabilities on top of MathComp (e.g., [6]) and to apply it to the formalization of equational reasoning for probabilistic programming languages (e.g., to extend [5] to continuous probabilities).