# mathlibdocumentation

measure_theory.hausdorff_measure

# Hausdorff measure and metric (outer) measures #

In this file we define the d-dimensional Hausdorff measure on an (extended) metric space X and the Hausdorff dimension of a set in an (extended) metric space. Let μ d δ be the maximal outer measure such that μ d δ s ≤ (emetric.diam s) ^ d for every set of diameter less than δ. Then the Hausdorff measure μH[d] s of s is defined as ⨆ δ > 0, μ d δ s. By Caratheodory theorem measure_theory.outer_measure.is_metric.borel_le_caratheodory, this is a Borel measure on X.

The value of μH[d], d > 0, on a set s (measurable or not) is given by

μH[d] s = ⨆ (r : ℝ≥0∞) (hr : 0 < r), ⨅ (t : ℕ → set X) (hts : s ⊆ ⋃ n, t n)
(ht : ∀ n, emetric.diam (t n) ≤ r), ∑' n, emetric.diam (t n) ^ d


For every set s for any d < d' we have either μH[d] s = ∞ or μH[d'] s = 0, see measure_theory.measure.hausdorff_measure_zero_or_top. The Hausdorff dimension dimH s : ℝ≥0∞ of a set s is the supremum of d : ℝ≥0 such that μH[d] s = ∞. Then μH[d] s = ∞ for d < dimH s and μH[d] s = 0 for dimH s < d.

We also define two generalizations of the Hausdorff measure. In one generalization (see measure_theory.measure.mk_metric) we take any function m (diam s) instead of (diam s) ^ d. In an even more general definition (see measure_theory.measure.mk_metric') we use any function of m : set X → ℝ≥0∞. Some authors start with a partial function m defined only on some sets s : set X (e.g., only on balls or only on measurable sets). This is equivalent to our definition applied to measure_theory.extend m.

We also define a predicate measure_theory.outer_measure.is_metric which says that an outer measure is additive on metric separated pairs of sets: μ (s ∪ t) = μ s + μ t provided that ⨅ (x ∈ s) (y ∈ t), edist x y ≠ 0. This is the property required for the Caratheodory theorem measure_theory.outer_measure.is_metric.borel_le_caratheodory, so we prove this theorem for any metric outer measure, then prove that outer measures constructed using mk_metric' are metric outer measures.

## Notations #

We use the following notation localized in measure_theory.

• μH[d] : measure_theory.measure.hausdorff_measure d

## Implementation notes #

There are a few similar constructions called the d-dimensional Hausdorff measure. E.g., some sources only allow coverings by balls and use r ^ d instead of (diam s) ^ d. While these construction lead to different Hausdorff measures, they lead to the same notion of the Hausdorff dimension.

## Tags #

Hausdorff measure, Hausdorff dimension, dimension, measure, metric measure