# 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

### Metric outer measures #

In this section we define metric outer measures and prove Caratheodory theorem: a metric outer measure has the Caratheodory property.

def measure_theory.outer_measure.is_metric {X : Type u_2}  :
Prop

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.

Equations
theorem measure_theory.outer_measure.is_metric.finset_Union_of_pairwise_separated {ι : Type u_1} {X : Type u_2} (hm : μ.is_metric) {I : finset ι} {s : ι → set X} (hI : ∀ (i : ι), i I∀ (j : ι), j Ii jis_metric_separated (s i) (s j)) :
μ (⋃ (i : ι) (H : i I), s i) = ∑ (i : ι) in I, μ (s i)

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.

def measure_theory.outer_measure.mk_metric'.pre {X : Type u_2} (m : set Xℝ≥0∞) (r : ℝ≥0∞) :

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
def measure_theory.outer_measure.mk_metric' {X : Type u_2} (m : set Xℝ≥0∞) :

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

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
theorem measure_theory.outer_measure.mk_metric'.le_pre {X : Type u_2} {m : set Xℝ≥0∞} {r : ℝ≥0∞}  :
∀ (s : set X), μ s m s
theorem measure_theory.outer_measure.mk_metric'.pre_le {X : Type u_2} {m : set Xℝ≥0∞} {r : ℝ≥0∞} {s : set X} (hs : r) :
theorem measure_theory.outer_measure.mk_metric'.mono_pre {X : Type u_2} (m : set Xℝ≥0∞) {r r' : ℝ≥0∞} (h : r r') :
theorem measure_theory.outer_measure.mk_metric'.mono_pre_nat {X : Type u_2} (m : set Xℝ≥0∞) :
monotone (λ (k : ),
theorem measure_theory.outer_measure.mk_metric'.tendsto_pre {X : Type u_2} (m : set Xℝ≥0∞) (s : set X) :
theorem measure_theory.outer_measure.mk_metric'.trim_pre {X : Type u_2} (m : set Xℝ≥0∞) (hcl : ∀ (s : set X), m (closure s) = m s) (r : ℝ≥0∞) :
theorem measure_theory.outer_measure.mk_metric'_is_metric {X : Type u_2} (m : set Xℝ≥0∞) :

An outer measure constructed using outer_measure.mk_metric' is a metric outer measure.

theorem measure_theory.outer_measure.mk_metric_mono_smul {X : Type u_2} {m₁ m₂ : ℝ≥0∞ℝ≥0∞} {c : ℝ≥0∞} (hc : c ) (h0 : c 0) (hle : m₁ ≤ᶠ[𝓝[] 0] c m₂) :

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₂.

theorem measure_theory.outer_measure.mk_metric_mono {X : Type u_2} {m₁ m₂ : ℝ≥0∞ℝ≥0∞} (hle : m₁ ≤ᶠ[𝓝[] 0] m₂) :

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₂

theorem measure_theory.outer_measure.isometry_comap_mk_metric {X : Type u_2} {Y : Type u_3} (m : ℝ≥0∞ℝ≥0∞) {f : X → Y} (hf : isometry f) (H : monotone (λ (d : {d : ℝ≥0∞ | d 0}), m d) ) :
theorem measure_theory.outer_measure.isometry_map_mk_metric {X : Type u_2} {Y : Type u_3} (m : ℝ≥0∞ℝ≥0∞) {f : X → Y} (hf : isometry f) (H : monotone (λ (d : {d : ℝ≥0∞ | d 0}), m d) ) :
theorem measure_theory.outer_measure.isometric_comap_mk_metric {X : Type u_2} {Y : Type u_3} (m : ℝ≥0∞ℝ≥0∞) (f : X ≃ᵢ Y) :
theorem measure_theory.outer_measure.isometric_map_mk_metric {X : Type u_2} {Y : Type u_3} (m : ℝ≥0∞ℝ≥0∞) (f : X ≃ᵢ Y) :

### 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.

def measure_theory.measure.mk_metric' {X : Type u_2} [borel_space X] (m : set Xℝ≥0∞) :

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
@[simp]
theorem measure_theory.measure.mk_metric_mono_smul {X : Type u_2} [borel_space X] {m₁ m₂ : ℝ≥0∞ℝ≥0∞} {c : ℝ≥0∞} (hc : c ) (h0 : c 0) (hle : m₁ ≤ᶠ[𝓝[] 0] c m₂) :

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₂.

theorem measure_theory.measure.mk_metric_mono {X : Type u_2} [borel_space X] {m₁ m₂ : ℝ≥0∞ℝ≥0∞} (hle : m₁ ≤ᶠ[𝓝[] 0] m₂) :

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₂

theorem measure_theory.measure.mk_metric_apply {X : Type u_2} [borel_space X] (m : ℝ≥0∞ℝ≥0∞) (s : set X) :
= ⨆ (r : ℝ≥0∞) (hr : 0 < r), ⨅ (t : set X) (hts : s ⋃ (n : ), t n) (ht : ∀ (n : ), emetric.diam (t n) r), ∑' (n : ), ⨆ (ht : ¬(t n).subsingleton), m (emetric.diam (t n))

A formula for measure_theory.measure.mk_metric.

### Hausdorff measure and Hausdorff dimension #

def measure_theory.measure.hausdorff_measure {X : Type u_2} [borel_space X] (d : ) :

Hausdorff measure on an (e)metric space.

Equations
theorem measure_theory.measure.hausdorff_measure_apply' {X : Type u_2} [borel_space X] (d : ) (s : set X) :
μH[d] s = ⨆ (r : ℝ≥0∞) (hr : 0 < r), ⨅ (t : set X) (hts : s ⋃ (n : ), t n) (ht : ∀ (n : ), emetric.diam (t n) r), ∑' (n : ), ⨆ (ht : ¬(t n).subsingleton), emetric.diam (t n) ^ d

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.

theorem measure_theory.measure.hausdorff_measure_apply {X : Type u_2} [borel_space X] {d : } (hd : 0 < d) (s : set X) :
μ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

A formula for μH[d] s that works for all positive d.

theorem measure_theory.measure.hausdorff_measure_zero_or_top {X : Type u_2} [borel_space X] {d₁ d₂ : } (h : d₁ < d₂) (s : set X) :
μH[d₂] s = 0 μH[d₁] s =

If d₁ < d₂, then for any set s we have either μH[d₂] s = 0, or μH[d₁] s = ∞.

theorem measure_theory.measure.hausdorff_measure_mono {X : Type u_2} [borel_space X] {d₁ d₂ : } (h : d₁ d₂) (s : set X) :
μH[d₂] s μH[d₁] s

Hausdorff measure μH[d] s is monotone in d.

@[instance]
def measure_theory.dimH {X : Type u_2} [borel_space X] (s : set X) :

Hausdorff dimension of a set in an (e)metric space.

Equations
theorem measure_theory.dimH_subsingleton {X : Type u_2} [borel_space X] {s : set X} (h : s.subsingleton) :
theorem set.subsingleton.dimH_eq {X : Type u_2} [borel_space X] {s : set X} (h : s.subsingleton) :

Alias of dimH_subsingleton.

@[simp]
theorem measure_theory.dimH_empty {X : Type u_2} [borel_space X] :
@[simp]
theorem measure_theory.dimH_singleton {X : Type u_2} [borel_space X] (x : X) :
= 0
theorem measure_theory.hausdorff_measure_of_lt_dimH {X : Type u_2} [borel_space X] {s : set X} {d : ℝ≥0} (h : d < ) :
theorem measure_theory.le_dimH_of_hausdorff_measure_eq_top {X : Type u_2} [borel_space X] {s : set X} {d : ℝ≥0} (h : μH[d] s = ) :
theorem measure_theory.hausdorff_measure_of_dimH_lt {X : Type u_2} [borel_space X] {s : set X} {d : ℝ≥0} (h : < d) :
theorem measure_theory.measure_zero_of_dimH_lt {X : Type u_2} [borel_space X] {μ : measure_theory.measure X} {d : ℝ≥0} (h : μ μH[d]) {s : set X} (hd : < d) :
μ s = 0
theorem measure_theory.dimH_mono {X : Type u_2} [borel_space X] {s t : set X} (h : s t) :
@[simp]
theorem measure_theory.dimH_Union {ι : Type u_1} {X : Type u_2} [borel_space X] [encodable ι] (s : ι → set X) :
measure_theory.dimH (⋃ (i : ι), s i) = ⨆ (i : ι), measure_theory.dimH (s i)
@[simp]
theorem measure_theory.dimH_bUnion {ι : Type u_1} {X : Type u_2} [borel_space X] {s : set ι} (hs : s.countable) (t : ι → set X) :
measure_theory.dimH (⋃ (i : ι) (H : i s), t i) = ⨆ (i : ι) (H : i s), measure_theory.dimH (t i)
@[simp]
theorem measure_theory.dimH_sUnion {X : Type u_2} [borel_space X] {S : set (set X)} (hS : S.countable) :
= ⨆ (s : set X) (H : s S),
@[simp]
theorem measure_theory.dimH_union {X : Type u_2} [borel_space X] (s t : set X) :