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! 🐙