10.1. Existence🔗

A locally compact group admits a unique left-invariant measure which is unique up to scale (subject to mild additional hypotheses). This is known as the Haar measure. Mathlib contains the theory of Haar measure, including existence and uniqueness.

As the Haar measure is only unique up to scale, to obtain a Haar measure, one must supply a compact subset K (with non-empty interior) which is deemed to have unit measure. The following demonstrates this in action:

variable {G : Type*}
  [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [MeasurableSpace G] [BorelSpace G]
  (K : TopologicalSpace.PositiveCompacts G)

MeasureTheory.Measure.haarMeasure K : MeasureTheory.Measure G#check MeasureTheory.Measure.haarMeasure K

Note that the existence of K ensures that G is locally compact:

example : LocallyCompactSpace G :=
  K.locallyCompactSpace_of_group

If G is compact then the unique measure for which the entire group has unit measure can be obtained as:

variable [CompactSpace G]

MeasureTheory.Measure.haarMeasure ⊤ : MeasureTheory.Measure G#check MeasureTheory.Measure.haarMeasure (G := G) ⊤