11.4. Hausdorff dimension🔗

Mathlib also contains a theory of Hausdorff dimension. It is called dimH.

Given a subset s of a metric space X, its Hausdorff dimension can be defined as the supremum of dimensions such that the correpsonding Hausdorff measure is infinite. Mathlib knows this:

open ENNReal NNReal in
example (s : Set X) :
    dimH s = ⨆ (d : ℝ≥0) (_ : μH[d] s = ∞), (d : ℝ≥0∞) :=
  dimH_def s

Alternatively the Hausdorff dimension can be defined as the infimum of dimensions such that the corresponding Hausdoff measure is zero. Mathlib knows this too:

open ENNReal NNReal in
example (s : Set X) :
    dimH s = ⨅ (d : ℝ≥0) (_ : μH[d] s = 0), (d : ℝ≥0∞) :=
  dimH_eq_iInf s