11.3. Connection to Lebesgue and Haar🔗

In Mathlib, the real numbers carry the Lebesgue measure as their canonical measure. It is called (volume : Measure ℝ). Mathlib knows that this coincides with the 1-dimensional Hausdorff measure and we can witness this as follows:

example :
    μH[1] = (volume : Measure ℝ) :=
  hausdorffMeasure_real

More generally, Mathlib knows that the Hausdorff measure may be a Haar measure. For example if E is a finite-dimensional normed real vector space then Mathlib knows that the top-dimensional Hausdorff measure is a Haar measure:

open Module in
example {E : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E]
    [MeasurableSpace E] [BorelSpace E] :
    IsAddHaarMeasure (G := E) μH[finrank ℝ E] :=
  inferInstance