← All papers
A formalization of the change of variables formula for integrals in mathlib
cs.LO
Jul 26, 2022 · v1
TL;DR
Formalizes the general change of variables formula for integrals in Lean's mathlib.
Abstract
We report on a formalization of the change of variables formula in integrals, in the mathlib library for Lean. The theorem is extremely general, building 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.
Problem
The change of variables formula for integrals is a fundamental result in analysis that had not been formalized in the mathlib library for Lean. The theorem requires developments across multiple mathematical domains.
Approach
The authors formalize the change of variables formula in integrals in the mathlib library for Lean, building on developments in linear algebra, analysis, measure theory, and descriptive set theory. The highly integrated development model of mathlib makes the interplay between these domains transparent.
Results
A complete formalization of the change of variables formula for integrals is contributed to mathlib. The result is extremely general, leveraging mathlib's existing infrastructure across multiple mathematical domains.