A formalization of the change of variables formula for integrals in mathlib
| Autor: | Sébastien Gouëzel |
|---|---|
| Přispěvatelé: | Institut de Recherche Mathématique de Rennes (IRMAR), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-École normale supérieure - Rennes (ENS Rennes)-Université de Rennes 2 (UR2)-Centre National de la Recherche Scientifique (CNRS)-Institut Agro Rennes Angers, Institut national d'enseignement supérieur pour l'agriculture, l'alimentation et l'environnement (Institut Agro)-Institut national d'enseignement supérieur pour l'agriculture, l'alimentation et l'environnement (Institut Agro) |
| Jazyk: | angličtina |
| Rok vydání: | 2022 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science Formalization Integral mathlib [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] [MATH.MATH-CA]Mathematics [math]/Classical Analysis and ODEs [math.CA] Change of variables Logic in Computer Science (cs.LO) |
| Zdroj: | Lecture Notes in Computer Science 15th Conference on Intelligent Computer Mathematics 15th Conference on Intelligent Computer Mathematics, Sep 2022, Tbilisi, Georgia. pp.3-18, ⟨10.1007/978-3-031-16681-5_1⟩ Lecture Notes in Computer Science ISBN: 9783031166808 |
| DOI: | 10.1007/978-3-031-16681-5_1⟩ |
| Popis: | International audience; 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: | OpenAIRE |
| Externí odkaz: |
|