Formalized Haar Measure

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.