# Towards the Fundamental Theorem of Calculus for the Lebesgue Integral in Coq

Reynald Affeldt, Zachary Stone

► To cite this version:

Reynald Affeldt, Zachary Stone. Towards the Fundamental Theorem of Calculus for the Lebesgue Integral in Coq. 35es Journées Francophones des Langages Applicatifs (JFLA 2024), Jan 2024, Saint-Jacut-de-la-Mer, France. hal-04406350

HAL Id: hal-04406350

https://inria.hal.science/hal-04406350v1

Submitted on 19 Jan 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Towards the Fundamental Theorem of Calculus for the Lebesgue Integral in Coq

Reynald Affeldt<fnref n="1" />,<fnref n="2" /> and Zachary Stone<fnref n="2" />

We report on an ongoing formalization of the Fundamental Theorem of Calculus (FTC) for the Lebesgue integral in the Coq proof assistant. To this aim, we formalize Lebesgue's differentiation theorem, which has other applications and whose proof can be decomposed in lemmas of independent interest. As a result, we significantly enrich the theories of MathComp-Analysis, an extension of the Mathematical Components library for analysis, and eventually relate its definitions of derivability and of integration.

## Motivation and contributions

The formalization of the Fundamental Theorem of Calculus (FTC) for the Lebesgue integral in the Coq proof assistant is an ongoing work part of the development of MATHCOMP-ANALYSIS [ABC$^+$23], a library for analysis that extends the Mathematical Components library [MT21] with classical axioms [ACR18, §5]. Besides mathematics, MATHCOMP-ANALYSIS has also been used to formalize programming languages [ACS23, ZBS$^+$23, SA23].

The first FTC for Lebesgue integration can be stated as follows: for $f$ integrable on $\mathbb{R}$, $F(x) \stackrel{\text{def}}{=} \int_{t\in[-\infty, x]} f(t)(\mathbf{d}\mu)$ is derivable and $F'(x) = f(x)$ a.e. (i.e., almost-everywhere) relatively to $\mu$, which is the Lebesgue measure. This is different from the statement for the Riemann integral, where $f$ is usually assumed to be continuous, making for a simple proof. In comparison, connecting derivation and Lebesgue integration under an integrability hypothesis is unwieldy, even more so in MATHCOMP-ANALYSIS whose formalizations of derivation [ACR18, §4.5] and of the Lebesgue integral [AC23, §6.4] have been unrelated so far. They can be bridged thanks to the Lebesgue differentiation theorem and this is appealing for two reasons. First, it is a useful theorem in itself: the FTC is a consequence, as well as other results such as Lebesgue's density theorem. Second, we can decompose its proof in several results: this provides a nice way to incrementally enrich the theories of MATHCOMP-ANALYSIS. We think that this approach is an instance of a more generic way to tackle formalization of mathematics: find a path through the literature to present many key results as easy consequences of a central, technical lemma with rather weak assumptions.

In terms of formalization in a proof assistant, our contributions are as follows. We provide the first formalization of the first FTC for Lebesgue integration in Coq. We also bring to Coq standard results of measure theory and topology: Vitali's lemmas and theorem, Hardy-Littlewood's operator, Urysohn's lemma, Ergorov's, Lusin's, Tietze's theorems, and the Lebesgue differentiation theorem. We also improve the MATHCOMP-ANALYSIS support

<footnote n="1">¹National Institute of Advanced Industrial Science and Technology (AIST), Tokyo, Japan</footnote>

<footnote n="2">²The MathComp-Analysis development team</footnote>
for real functions (extended lim sup / lim inf theory) and for topology (lower semicontinuity, normal spaces, etc.).

Lebesgue differentiation theorem and the FTC

Let us note $[f]_A \stackrel{\text{def}}{=} \frac{1}{\mu(A)} \int_{y \in A} |f(y)|(d\mu)$ the average of a real-valued function $f$ over the set $A$. We introduce the notation $\overline{f}_{B(x,r)} \stackrel{\text{def}}{=} [\lambda y.f(y) - f(x)]_{B(x,r)}$ where $B(x,r)$ is a ball centered at $x$ of radius $r$. Given a real-valued function $f$, a Lebesgue point is a real number $x$ s.t. $\overline{f}_{B(x,r)} \xrightarrow[r \to 0^+]{-} 0$. Reusing the Lebesgue measure (hereafter $\mu$) formalized in [AC23, §5.2] and notations from MATHCOMP-ANALYSIS, we formally define Lebesgue points:

*   **Definition iavg** ($f: R \to R$) ($A: \text{set } R$) := $(\text{fine } \mu A))^{-1}\%:E * \int_{\mu(A)} (y \text{ in } A)^{\wedge} (f y)\%:E |$.

*   **Definition favg** ($f: R \to R$) ($x, r: R$) := $iavg(\text{center}(f, x), \text{lo f})(\text{ball } x, r)$.

*   **Definition lebesgue pt** ($f: R \to R$) ($x: R$) := $\text{favg}(f, x, r \in [r \text{ -- } 0^{+}])$.

To inject/project between numeric values and their extended versions we use %:E/fine. The notation for convergence $f, x \in [x \text{ -- } a]$ --> 1 stands for $f(x) \xrightarrow{x \to a} \ell$. We use the notation $^{+}$ for the filters of neighborhoods of $x$ intersected with $]x, +\infty[$ to define the fact that $r$ tends to $0^+$. The Lebesgue differentiation theorem states that, for a real-valued, locally-integrable function $f$ (i.e., integrable on compact subsets of its domain), we have Lebesgue points a.e.:

*   **Lemma lebesgue_differentiation** ($f: R \to R$) : locally_integrable $\text{set } f \to \{\text{ae } \mu, \text{forall } x, \text{ lebesgue pt } f, x\}$.

The first step of the proof of the Lebesgue differentiation theorem is to reduce the problem to functions $f_k \stackrel{\text{def}}{=} f \mathbb{1}_{B_k}$ with $B_k \stackrel{\text{def}}{=} B(0, 2(k+1))$:

*   **Lemma lebesgue_differentiation_bounded** ($f: R \to R$) : $\text{let } B, k := \text{ball } 0, k + 1 \cdot 2\%:R \text{ in let } f_k := f \setminus \text{\`1}_-(B, k) \text{ in} \quad (\text{forall } k, \mu, \text{-integrable } \text{set } T \text{ (EFin } \lo f_k \text{))} \to \text{forall } k, \{\text{ae } \mu, \text{forall } x, B, k, x \to \text{lebesgue pt } f_k, x\}$.

This problem reduction is often hand-waved in lecture notes (one exception is [Sch97, (5.12.101)]). Second, instead of proving for all $k$ that we have a.e. over $B_k$ Lebesgue points, it is sufficient to prove that the set $A_k(a) \stackrel{\text{def}}{=} B_k \cap \{x | a < \limsup_{r \to 0} \overline{f_k}_{B(x,r)}\}$ is negligible for all $a > 0$. The idea is to exhibit a sequence of continuous functions $g_i$ such that $A_k(a) \subseteq \bigcap_n B_k \cap \underbrace{\{x | f_k(x) - g_n(x) \ge a/2\}}_{(a)} \cup \underbrace{\{x | \text{HL}(f_k(x) - g_n(x)) > a/2\}}_{(b)}$ where

$\text{HL}(f)(x) \stackrel{\text{def}}{=} \sup_{r>0} \{[f]_{B(x,r)}\}$ is the Hardy-Littlewood operator. We can show that the measure of the right-hand side is null. To deal with $(a)$, we use Markov's inequality and the fact that continuous functions are dense in $L^1$. To deal with $(b)$, we need the Hardy-Littlewood maximal inequality, which in turns relies on Vitali's covering lemma. Figure 1 shows the main lemmas that we add to MATHCOMP-ANALYSIS to formalize this proof.

As a consequence, we can prove the first FTC for Lebesgue integration:

*   **Theorem FTC1** ($f: R \to R$) : $\mu, \text{-integrable } \text{set } T \text{ (EFin } \lo f \text{)} \to \text{let } F, x := (\int_{\mu} [f]_{T(x,r)} \text{ (f t)})^{1/\mu} \text{ in} \quad (\text{forall } x, \text{ lebesgue pt } f, x \to \text{derivable } (F: R^\infty \to R^\infty, x \in \mathbb{R}) \text{ (f: R \to R^\infty) })$.

The predicate derivable is for derivability (1 is the direction) and the notation $^{\wedge}()$ is for derivatives with domain $\mathbb{R}$ [ACR18, §4.5]. The theorem above connects these notions with the Lebesgue integral [AC23, §6.4]. The proof goes through a generalization of the Lebesgue differentiation theorem where balls are replaced with nicely shrinking sets [Li22, II.4.1].
<figure><img src="image_2.png" /><figcaption>**Figure 1.** Development overview [AS23]</figcaption></figure>

## Related work

We have been using various documents to formalize the Lebesgue differentiation theorem. In particular, the main lines are drawn from [Bow14]. For the proofs of the Hardy-Littlewood maximal inequality and the proof of the Lebesgue differentiation theorem we used books by Li [Li22] and Schwartz [Sch97]. Surely, the same contents can be found elsewhere.

The FTC has already been the target of formalizations in proof assistants. It can be found in Coq but for the Riemann integral in a constructive setting [Cru02, §6]. NASAlib does not feature the first FTC for Lebesgue integration but an elementary proof (for a $C^1$ function) of the second FTC [NAS23a, file lebesgue_fundamental.pvs]. Isabelle/HOL features the first FTC for Lebesgue integration but for continuous functions whereas we prove it for integrable functions [AHS17, §3.7]. Mathlib has a number of variants of the first FTC that require integrability and continuity at the endpoints but that establish strict differentiability [Mat23c]. They stem from a lemma analogous to a strengthening of the Lebesgue differentiation theorem with nicely shrinking sets [Mat23d]. Mathlib also contains a formalization of the Lebesgue differentiation theorem [Mat23b] which is used to prove a generic version of Lebesgue's density theorem [Mat23a][Nas23b, §3.2]. In other words, we are able to match our lemmas with Mathlib lemmas but statements are slightly different and proofs are organized in a different way.

## Perspectives

MATHCOMP-ANALYSIS is still under development in the sense that not all notions are formalized as we would like them to be. Yet, the proof of the Lebesgue differentiation theorem shows that it is a rich library and already a useful tool to formalize mathematics. Indeed, we could use it to revisit Urysohn's lemma by producing an original proof. We are now working on the second FTC for Lebesgue integration whose most general form deals with absolutely continuous functions [Moh21], using as the main ingredient the Radon-Nikodým theorem already available in MATHCOMP-ANALYSIS [IA23].

**Acknowledgments** The authors are grateful to A. Bruni, C. Cohen, Y. Ishiguro, and T. Saikawa for their inputs. This work has benefited from feedback gained during the MATHCOMP-ANALYSIS development meetings. The first author acknowledges support of the JSPS KAKENHI Grant Number 22H00520.
## References

[ABC$^{+}$23] Reynald Affeldt, Yves Bertot, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Pierre Roux, Kazuhiko Sakaguchi, Zachary Stone, Pierre-Yves Strub, and Laurent Théry. MathComp-Analysis: Mathematical Components compliant analysis library. https://github.com/math-comp/analysis, 2023. Since 2017. Version 0.6.6.

[AC23] Reynald Affeldt and Cyril Cohen. Measure construction by extension in dependent type theory with application to integration. *J. Autom. Reason.*, 67(3):28:1–28:27, 2023.

[ACR18] Reynald Affeldt, Cyril Cohen, and Damien Rouhling. Formalization techniques for asymptotic reasoning in classical analysis. *J. Formaliz. Reason.*, 11(1):43–76, 2018.

[ACS23] Reynald Affeldt, Cyril Cohen, and Ayumu Saito. Semantics of probabilistic programs using s-finite kernels in Coq. In *12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2023) Boston, MA, USA, January 16–17, 2023*, pages 3–16. ACM, 2023.

[AHS17] Jeremy Avigad, Johannes Hölzl, and Luke Serafin. A formally verified proof of the central limit theorem. *J. Autom. Reason.*, 59(4):389–423, 2017.

[AS23] Reynald Affeldt and Zachary Stone. Lebesgue differentiation theorem and applications. Available at https://github.com/math-comp/analysis/pull/1065, 2023. Pull request to [ABC$^{+}$23].

[Bow14] Lewis Bowen. Lecture notes in real analysis. Available at https://web.ma.utexas.edu/users/lpbowen/m381c/lecture-notes.pdf, Dec 2014. University of Texas at Austin.

[Cru02] Luís Cruz-Filipe. A constructive formalization of the fundamental theorem of calculus. In *Selected Papers of the 2nd International Workshop on Types for Proofs and Programs (TYPES 2002)*, Berg en Dal, The Netherlands, April 24-28, 2002, volume 2646 of *Lecture Notes in Computer Science*, pages 108–126. Springer, 2002.

[IA23] Yoshihiro Ishiguro and Reynald Affeldt. A progress report on formalization of measure theory with MathComp-Analysis. In *25th Workshop on Programming and Programming Languages (PPL2023), Nagoya University, March 6–8, 2023*. Japan Society for Software Science and Technology, Mar 2023. 15 pages.

[Li22] Daniel Li. *Notions fondamentales d'analyse réelle et complexe*. Ellipses, 2022.

[Mat23a] Mathlib 4. File MeasureTheory/Covering/DensityTheorem.lean. url, Dec 2023.

[Mat23b] Mathlib 4. File MeasureTheory/Covering/Differentiation.lean. url, Dec 2023.

[Mat23c] Mathlib 4. File MeasureTheory/Integral/FundThmCalculus.lean. url, Dec 2023.

[Mat23d] Mathlib 4. File MeasureTheory/Integral/SetIntegral.lean. url, Dec 2023.

[Moh21] Maran Mohanarangan. The fundamental theorem of calculus for Lebesgue integration. Technical report, ETH Zürich, 2021. Exercise Class 13, Measure and Integration, Spring 2021, available at https://metaphor.ethz.ch/x/2021/fs/401-2284-00L/sc/notes_exclass13.pdf.

[MT21] Assia Mahboubi and Enrico Tassi. *Mathematical Components*. Zenodo, Jan 2021.
[NAS23a] NASA Lib. NASA PVS library of formal developments. Current version: 7.1.1.
Available at https://github.com/nasa/pvslib., 2023.

[Nas23b] Oliver Nash. A Formalisation of Gallagher's Ergodic Theorem. In *14th International Conference on Interactive Theorem Proving (ITP 2023)*, volume 268 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 23:1–23:16, Dagstuhl, Germany, 2023. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.

[SA23] Ayumu Saito and Reynald Affeldt. Experimenting with an intrinsically-typed probabilistic programming language in Coq. In *21st Asian Symposium on Programming Languages and Systems (APLAS 2023), November 26–29, 2023, Taipei, Taiwan*, volume 14405, pages 182–202. Springer, 2023.

[Sch97] Laurent Schwartz. *Analyse III: Calcul intégral*. Hermann, 1997.

[ZBS+23] Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, and Mingsheng Ying. Coq: Foundational verification of quantum programs. *Proc. ACM Program. Lang., 7(POPL):833–865, 2023.*