
TL;DR
This paper details the formalization of Haar measure within the Lean theorem prover, including measure theory concepts like product measures and Fubini's theorem, enhancing formal verification in abstract harmonic analysis.
Contribution
It introduces the first formalization of Haar measure in a proof assistant and expands Lean's measure theory library with key theorems.
Findings
Formalization of Haar measure existence and uniqueness
Implementation of product measures and Fubini's theorem in Lean
Enhanced measure theory library in Lean's mathlib
Abstract
We describe the formalization of the existence and uniqueness of 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 \textsf{mathlib}, and discuss the construction of product measures and the proof of Fubini's theorem for the Bochner integral.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
