A Coq Formalization of the Bochner integral

Sylvie Boldo (1) , François Clément (2, 3) , Louise Leclerc (4)

1 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
2 SERENA - Simulation for the Environment: Reliable and Efficient Numerical Algorithms
3 CERMICS - Centre d'Enseignement et de Recherche en Mathématiques et Calcul Scientifique
4 DMA - Département de Mathématiques et Applications - ENS Paris

The Bochner integral is a generalization of the Lebesgue integral, for functions taking their values in a Banach space. Therefore, both its mathematical definition and its formalization in the Coq proof assistant are more challenging as we cannot rely on the properties of real numbers. Our contributions include an original formalization of simple functions, Bochner integrability defined by a dependent type, and the construction of the proof of the integrability of measurable functions under mild hypotheses (weak separability). Then, we define the Bochner integral and prove several theorems, including dominated convergence and the equivalence with an existing formalization of Lebesgue integral for nonnegative functions.

Mots clés: Bochner integral; Formal proof; Coq

Domaines: Logique en informatique [cs.LO]; Analyse classique [math.CA]; Analyse fonctionnelle [math.FA]

Sylvie Boldo, François Clément, Louise Leclerc. A Coq Formalization of the Bochner integral. 2022. ⟨hal-03516749v1⟩