Cette page présente mes activités de formalisation de preuves mathématiques, réalisées avec le logiciel Lean et la librairie Mathlib. La liste complète de mes contributions à Mathlib est disponible sur GitHub.
Volume des boules \(\ell^p\) dans Mathlib
Xavier Roblot, 2026
Description Nous décrivons la formalisation dans Mathlib de formules explicites pour le volume des boules \(\ell^p\), aussi bien dans \(\mathbb{R}^n\) que dans \(\mathbb{C}^n\), pour tout réel \(p \geq 1\). Plutôt que de traiter chaque cas séparément, toutes les formules se déduisent d'une identité unique exprimant le volume de la boule unité en termes d'une intégrale de type gaussien et de la fonction Gamma. Cette approche abstraite, valable pour tout espace normé de dimension finie muni d'une mesure de Haar, couvre également les espaces mélangeant coordonnées réelles et complexes, cas qui apparaît en théorie algébrique des nombres et qui était d'ailleurs la motivation initiale de ce travail.
Prépublication HAL