License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2021.18
URN: urn:nbn:de:0030-drops-139139
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13913/
van Doorn, Floris
Formalized Haar Measure
Abstract
We describe the formalization of the existence and uniqueness of the Haar measure in the Lean theorem prover. The Haar measure is an invariant regular measure on locally compact groups, and it has not been formalized in a proof assistant before. We will also discuss the measure theory library in Lean’s mathematical library mathlib, and discuss the construction of product measures and the proof of Fubini’s theorem for the Bochner integral.
BibTeX - Entry
@InProceedings{vandoorn:LIPIcs.ITP.2021.18,
author = {van Doorn, Floris},
title = {{Formalized Haar Measure}},
booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)},
pages = {18:1--18:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-188-7},
ISSN = {1868-8969},
year = {2021},
volume = {193},
editor = {Cohen, Liron and Kaliszyk, Cezary},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/13913},
URN = {urn:nbn:de:0030-drops-139139},
doi = {10.4230/LIPIcs.ITP.2021.18},
annote = {Keywords: Haar measure, measure theory, Bochner integral, Lean, interactive theorem proving, formalized mathematics}
}
