A formalization of the change of variables formula for integrals in mathlib - Institut de Recherche Mathématique de Rennes Accéder directement au contenu
Communication Dans Un Congrès Année : 2022

A formalization of the change of variables formula for integrals in mathlib

Résumé

We report on a formalization of the change of variables formula in integrals, in the mathlib library for Lean. Our version of this theorem is extremely general, and builds on developments in linear algebra, analysis, measure theory and descriptive set theory. The interplay between these domains is transparent thanks to the highly integrated development model of mathlib.
Fichier principal
Vignette du fichier
samplepaper.pdf (212.29 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03737714 , version 1 (25-07-2022)

Identifiants

Citer

Sébastien Gouëzel. A formalization of the change of variables formula for integrals in mathlib. 15th Conference on Intelligent Computer Mathematics, Sep 2022, Tbilisi, Georgia. pp.3 - 18, ⟨10.1007/978-3-031-16681-5_1⟩. ⟨hal-03737714⟩
30 Consultations
80 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More