Comparing Euclidean and raw Hausdorff measures

Mathlib's Euclidean Hausdorff measure μHE[d] is the raw Hausdorff measure μH[d] rescaled by the constant that makes it agree with Lebesgue measure on d-dimensional Euclidean space. This constant is positive and finite, so the two normalizations have the same null sets and the same sets of finite measure; statements of either kind may be proved with either normalization. In dimension zero, Hausdorff measure is counting measure (TauCeti.hausdorffMeasure_zero_eq_count). In dimension one the normalizing constant is 1, because μH[1] already agrees with Lebesgue measure on ℝ. Hence μHE[1] = μH[1] on every extended metric space, so length statements may be proved with either normalization.

@[simp]

theorem MeasureTheory.Measure.euclideanHausdorffMeasure_eq_zero_iff {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {d : ℕ} {s : Set X} : (euclideanHausdorffMeasure d) s = 0 ↔ (hausdorffMeasure ↑d) s = 0

A set is null for the Euclidean Hausdorff measure μHE[d] if and only if it is null for the raw Hausdorff measure μH[d].

@[simp]

theorem MeasureTheory.Measure.euclideanHausdorffMeasure_lt_top_iff {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {d : ℕ} {s : Set X} : (euclideanHausdorffMeasure d) s < ⊤ ↔ (hausdorffMeasure ↑d) s < ⊤

A set has finite Euclidean Hausdorff measure μHE[d] if and only if it has finite raw Hausdorff measure μH[d].

theorem MeasureTheory.Measure.euclideanHausdorffMeasure_one {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] : euclideanHausdorffMeasure 1 = hausdorffMeasure 1

The one-dimensional Euclidean Hausdorff measure is the raw one-dimensional Hausdorff measure, on every extended metric space.