← All papers
Formalized Haar Measure
cs.LO
Feb 4, 2021 · v1
TL;DR
First formalization of the existence and uniqueness of Haar measure in any proof assistant.
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 this is the first formalization of this result in a proof assistant. We also discuss the measure theory library in Lean's mathematical library mathlib, including the construction of product measures and the proof of Fubini's theorem for the Bochner integral.
Problem
The Haar measure is a fundamental object in analysis and algebra, providing an invariant regular measure on locally compact groups. No formalization of its existence and uniqueness existed in any proof assistant.
Approach
The authors formalize the existence and uniqueness of Haar measure in the Lean theorem prover. The work builds on and extends the measure theory library in Lean's Mathlib, including the construction of product measures and the proof of Fubini's theorem for the Bochner integral.
Results
This is the first formalization of the existence and uniqueness of Haar measure in any proof assistant. The accompanying measure theory infrastructure (product measures, Fubini's theorem for the Bochner integral) is contributed to Mathlib.