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

Autor:	Gouëzel, Sébastien
Rok vydání:	2022
Předmět:	Computer Science - Logic in Computer Science
Druh dokumentu:	Working Paper
Popis:	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.
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2207.12742 Zobrazit plný text záznamu View this record from Arxiv