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.
References #
Tags #
Hausdorff measure, Hausdorff dimension, dimension, measure, metric measure
Metric outer measures #
In this section we define metric outer measures and prove Caratheodory theorem: a metric outer measure has the Caratheodory property.
We say that an outer measure μ in an (e)metric space is metric if μ (s ∪ t) = μ s + μ t
for any two metric separated sets s, t.
A metric outer measure is additive on a finite set of pairwise metric separated sets.
Caratheodory theorem. If m is a metric outer measure, then every Borel measurable set t is
Caratheodory measurable: for any (not necessarily measurable) set s we have
μ (s ∩ t) + μ (s \ t) = μ s.
Constructors of metric outer measures #
In this section we provide constructors measure_theory.outer_measure.mk_metric' and
measure_theory.outer_measure.mk_metric and prove that these outer measures are metric outer
measures. We also prove basic lemmas about map/comap of these measures.
Auxiliary definition for outer_measure.mk_metric': given a function on sets
m : set X → ℝ≥0∞, returns the maximal outer measure μ such that μ s ≤ m s
for any set s of diameter at most r.
Equations
- measure_theory.outer_measure.mk_metric'.pre m r = measure_theory.outer_measure.bounded_by (measure_theory.extend (λ (s : set X) (hs : emetric.diam s ≤ r), m s))
Given a function m : set X → ℝ≥0∞, mk_metric' m is the supremum of mk_metric'.pre m r
over r > 0. Equivalently, it is the limit of mk_metric'.pre m r as r tends to zero from
the right.
Equations
- measure_theory.outer_measure.mk_metric' m = ⨆ (r : ℝ≥0∞) (H : r > 0), measure_theory.outer_measure.mk_metric'.pre m r
Given a function m : ℝ≥0∞ → ℝ≥0∞ and r > 0, let μ r be the maximal outer measure such that
μ s = 0 on subsingletons and μ s ≤ m (emetric.diam s) whenever emetric.diam s < r. Then
mk_metric m = ⨆ r > 0, μ r. We add ⨆ (hs : ¬s.subsingleton) to ensure that in the case
m x = x ^ d the definition gives the expected result for d = 0.
Equations
- measure_theory.outer_measure.mk_metric m = measure_theory.outer_measure.mk_metric' (λ (s : set X), ⨆ (hs : ¬s.subsingleton), m (emetric.diam s))
An outer measure constructed using outer_measure.mk_metric' is a metric outer measure.
If c ∉ {0, ∞} and m₁ d ≤ c * m₂ d for 0 < d < ε for some ε > 0
(we use ≤ᶠ[𝓝[Ioi 0]] to state this), then mk_metric m₁ hm₁ ≤ c • mk_metric m₂ hm₂.
If m₁ d ≤ m₂ d for 0 < d < ε for some ε > 0 (we use ≤ᶠ[𝓝[Ioi 0]] to state this), then
mk_metric m₁ hm₁ ≤ mk_metric m₂ hm₂
Metric measures #
In this section we use measure_theory.outer_measure.to_measure and theorems about
measure_theory.outer_measure.mk_metric'/measure_theory.outer_measure.mk_metric to define
measure_theory.measure.mk_metric'/measure_theory.measure.mk_metric. We also restate some lemmas
about metric outer measures for metric measures.
Given a function m : set X → ℝ≥0∞, mk_metric' m is the supremum of μ r
over r > 0, where μ r is the maximal outer measure μ such that μ s ≤ m s
for all s. While each μ r is an outer measure, the supremum is a measure.
Equations
Given a function m : ℝ≥0∞ → ℝ≥0∞, mk_metric m is the supremum of μ r over r > 0, where
μ r is the maximal outer measure μ such that μ s ≤ m s for all sets s that contain at least
two points. While each mk_metric'.pre is an outer measure, the supremum is a measure.
Equations
If c ∉ {0, ∞} and m₁ d ≤ c * m₂ d for 0 < d < ε for some ε > 0
(we use ≤ᶠ[𝓝[Ioi 0]] to state this), then mk_metric m₁ hm₁ ≤ c • mk_metric m₂ hm₂.
If m₁ d ≤ m₂ d for 0 < d < ε for some ε > 0 (we use ≤ᶠ[𝓝[Ioi 0]] to state this), then
mk_metric m₁ hm₁ ≤ mk_metric m₂ hm₂
A formula for measure_theory.measure.mk_metric.
Hausdorff measure and Hausdorff dimension #
Hausdorff measure on an (e)metric space.
A formula for μH[d] s that works for all d. In case of a positive d a simpler formula
is available as measure_theory.measure.hausdorff_measure_apply.
A formula for μH[d] s that works for all positive d.
If d₁ < d₂, then for any set s we have either μH[d₂] s = 0, or μH[d₁] s = ∞.
Hausdorff measure μH[d] s is monotone in d.
Hausdorff dimension of a set in an (e)metric space.