11.2. Normalisation
The informal mathematical literature contains differing conventions for the overall scale
of the Hausdorff measure. Mathlib's definition uses the unnormalised convention. This can
be seen by the absence of any scale factors in the formula appearing in
hausdorffMeasure_apply: the measure is just an infimum of sums of powers of diameters.
Another way to witness the choice of scaling is to note that in \mathbb{R}^n with the sup norm,
the unit cube has measure 1 for the n-dimensional Hausdorff measure:
open Fintype Set in
example {n : ℕ} :
μH[n] (Icc 0 1 : Set (Fin n → ℝ)) = 1 := X:Type u_1inst✝²:MetricSpace Xinst✝¹:MeasurableSpace Xinst✝:BorelSpace Xd:ℝn:ℕ⊢ μH[↑n] (Icc 0 1) = 1
X:Type u_1inst✝²:MetricSpace Xinst✝¹:MeasurableSpace Xinst✝:BorelSpace Xd:ℝn:ℕthis:↑n = ↑(card (Fin n))⊢ μH[↑n] (Icc 0 1) = 1
All goals completed! 🐙
Mathlib also provides a normalized version for Euclidean space under the name
euclideanHausdorffMeasure and notation μHE[d]. While it is defined for all Borel metric
space, it is mostly useful for inner product affine spaces.
variable (V X : Type*)
[NormedAddCommGroup V] [InnerProductSpace ℝ V]
[MetricSpace X] [MeasurableSpace X] [BorelSpace X]
[NormedAddTorsor V X]
(d : ℕ)
#check euclideanHausdorffMeasure (X := X) d
#check (μHE[d] : Measure X)
The normalization is witnessed by the area of the unit disk
open EuclideanSpace Metric Real in
example :
μHE[2] (ball 0 1 : Set (EuclideanSpace ℝ (Fin 2))) =
ENNReal.ofReal π := X✝:Type u_1inst✝⁸:MetricSpace X✝inst✝⁷:MeasurableSpace X✝inst✝⁶:BorelSpace X✝d✝:ℝV:Type u_2X:Type u_3inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Xinst✝²:MeasurableSpace Xinst✝¹:BorelSpace Xinst✝:NormedAddTorsor V Xd:ℕ⊢ μHE[2] (ball 0 1) = ENNReal.ofReal π
X✝:Type u_1inst✝⁸:MetricSpace X✝inst✝⁷:MeasurableSpace X✝inst✝⁶:BorelSpace X✝d✝:ℝV:Type u_2X:Type u_3inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Xinst✝²:MeasurableSpace Xinst✝¹:BorelSpace Xinst✝:NormedAddTorsor V Xd:ℕ⊢ ENNReal.ofReal 1 ^ Fintype.card (Fin 2) *
ENNReal.ofReal (√π ^ Fintype.card (Fin 2) / Gamma (↑(Fintype.card (Fin 2)) / 2 + 1)) =
ENNReal.ofReal π
All goals completed! 🐙