Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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

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.
Complete list of metadata

https://hal.archives-ouvertes.fr/hal-03737714
Contributor : Sebastien Gouezel Connect in order to contact the contributor
Submitted on : Monday, July 25, 2022 - 12:38:11 PM
Last modification on : Wednesday, July 27, 2022 - 3:47:49 AM

Files

samplepaper.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03737714, version 1
  • ARXIV : 2207.12742

Citation

Sébastien Gouëzel. A formalization of the change of variables formula for integrals in mathlib. 2022. ⟨hal-03737714⟩

Share

Metrics

Record views

0

Files downloads

0