# mathlibdocumentation

measure_theory.haar_measure

# Haar measure #

In this file we prove the existence of Haar measure for a locally compact Hausdorff topological group.

For the construction, we follow the write-up by Jonathan Gleason, Existence and Uniqueness of Haar Measure. This is essentially the same argument as in https://en.wikipedia.org/wiki/Haar_measure#A_construction_using_compact_subsets.

We construct the Haar measure first on compact sets. For this we define (K : U) as the (smallest) number of left-translates of U are needed to cover K (index in the formalization). Then we define a function h on compact sets as lim_U (K : U) / (K₀ : U), where U becomes a smaller and smaller open neighborhood of 1, and K₀ is a fixed compact set with nonempty interior. This function is chaar in the formalization, and we define the limit formally using Tychonoff's theorem.

This function h forms a content, which we can extend to an outer measure and then a measure (haar_measure). We normalize the Haar measure so that the measure of K₀ is 1. We show that for second countable spaces any left invariant Borel measure is a scalar multiple of the Haar measure.

Note that μ need not coincide with h on compact sets, according to [halmos1950measure, ch. X, §53 p.233]. However, we know that h(K) lies between μ(Kᵒ) and μ(K), where ᵒ denotes the interior.

## Main Declarations #

• haar_measure: the Haar measure on a locally compact Hausdorff group. This is a left invariant regular measure. It takes as argument a compact set of the group (with non-empty interior), and is normalized so that the measure of the given set is 1.
• haar_measure_self: the Haar measure is normalized.
• is_left_invariant_haar_measure: the Haar measure is left invariant.
• regular_haar_measure: the Haar measure is a regular measure.
• Paul Halmos (1950), Measure Theory, §53
• Jonathan Gleason, Existence and Uniqueness of Haar Measure
• Note: step 9, page 8 contains a mistake: the last defined μ does not extend the μ on compact sets, see Halmos (1950) p. 233, bottom of the page. This makes some other steps (like step 11) invalid.
• https://en.wikipedia.org/wiki/Haar_measure