Formalized Haar Measure

2021/02/04 by van Doorn, Floris · 1 citation
#28C10 #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Functional Analysis (math.FA) #G.3 #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2102.07636

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 \textsfmathlib, and discuss the construction of product measures and the proof of Fubini's theorem for the Bochner integral.

Cited by

• A Formalization of the Ionescu-Tulcea Theorem in Mathlib

Related

• Haar Measures
• Haar measure for non-Hausdorff locally compact groups
• The Haar Measure Problem
• The Haar measure of a profinite n-ary group
• Computing Haar Measures