Commit 2021-12-18 20:11 ee17ab3a

refactor(measure_theory/measure/hausdorff): change Hausdorff measure definition at 0 (#10859) Currently, our definition of the Hausdorff measure ensures that it has no atom. This differs from the standard definition of the 0-Hausdorff measure, which is the counting measure -- and this convention is better behaved in many respects, for instance in a d-dimensional space the d-Hausdorff measure is proportional to Lebesgue measure, while currently we only have this for d > 0. This PR refactors the definition of the Hausdorff measure, to conform to the standard definition.