2026-07-22T22:13:56Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13913 2024-03-06T10:53:07Z ddc:004 open_access

Formalized Haar Measure van Doorn, Floris Haar measure measure theory Bochner integral Lean interactive theorem proving formalized mathematics 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Floris van Doorn 2021 Is Part Of LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2021.18 urn:nbn:de:0030-drops-139139 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.18 eng https://creativecommons.org/licenses/by/4.0/legalcode