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: https://drops.dagstuhl.de/opus/volltexte/2021/13913/
Go to the corresponding LIPIcs Volume Portal


van Doorn, Floris

Formalized Haar Measure

pdf-format:
LIPIcs-ITP-2021-18.pdf (0.8 MB)


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}
}

Keywords: Haar measure, measure theory, Bochner integral, Lean, interactive theorem proving, formalized mathematics
Collection: 12th International Conference on Interactive Theorem Proving (ITP 2021)
Issue Date: 2021
Date of publication: 21.06.2021
Supplementary Material: Software (Source Code): https://github.com/leanprover-community/mathlib/tree/master/src/measure_theory archived at: https://archive.softwareheritage.org/swh:1:dir:4b232212fa94778af7c966340636fd0e061d9598


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI