10.2. Further API and uniqueness🔗

The typeclass MeasureTheory.Measure.IsMulLeftInvariant expresses that a measure is left invariant and we can witness that a Haar measure is left invariant as follows:

open MeasureTheory.Measure in
example : (haarMeasure K).IsMulLeftInvariant :=
  inferInstance

In addition to the construction of the Haar measure, Mathlib has API characterising it. This is encoded using the typeclass MeasureTheory.Measure.IsHaarMeasure. One can use this to author lemmas which will apply to any Haar measure by beginning:

variable (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure]

We can witness that Mathlib knows such lemmas apply to types such as the reals and the circle as follows:

open MeasureTheory MeasureTheory.Measure in
example : IsAddHaarMeasure (G := ℝ) volume :=
  inferInstance

open MeasureTheory MeasureTheory.Measure in
example : IsAddHaarMeasure (G := UnitAddCircle) volume :=
  inferInstance

There are several uniqueness statements for Haar measures. Of particular note is MeasureTheory.Measure.isMulLeftInvariant_eq_smul.