A formalization of the change of variables formula for integrals in mathlib
Logic in Computer Science
2022-07-27 v1
Abstract
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.
Keywords
Cite
@article{arxiv.2207.12742,
title = {A formalization of the change of variables formula for integrals in mathlib},
author = {Sébastien Gouëzel},
journal= {arXiv preprint arXiv:2207.12742},
year = {2022}
}