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

TL;DR

This paper details the formalization of the change of variables formula for integrals within the mathlib library for Lean, emphasizing its generality and integration across multiple mathematical domains.

Contribution

It introduces a highly general formalization of the change of variables formula in mathlib, connecting linear algebra, analysis, measure theory, and descriptive set theory.

Findings

The formalization is highly general and comprehensive.

The development demonstrates effective integration of multiple mathematical domains.

The work enhances the capabilities of mathlib for formal reasoning about integrals.

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.