mathlib 中积分变量替换公式的形式化
计算机科学中的逻辑
2022-07-27 v1
摘要
我们报告了在 Lean 的 mathlib 库中，对积分变量替换公式的形式化工作。我们这一版本的定理极为通用，建立在线性代数、分析、测度论与描述集合论等方面的发展之上。得益于 mathlib 高度集成的发展模式，这些领域之间的相互作用是透明的。
引用
@article{arxiv.2207.12742,
title = {A formalization of the change of variables formula for integrals in mathlib},
author = {Sébastien Gouëzel},
journal= {arXiv preprint arXiv:2207.12742},
year = {2022}
}