# mathlib3documentation

measure_theory.measure.hausdorff

# Hausdorff measure and metric (outer) measures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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. In topology.metric_space.hausdorff_dimension we use this fact to define the Hausdorff dimension dimH of a set in an (extended) metric space.

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.

## Main definitions #

• measure_theory.outer_measure.is_metric: an outer measure μ is called metric if μ (s ∪ t) = μ s + μ t for any two metric separated sets s and t. A metric outer measure in a Borel extended metric space is guaranteed to satisfy the Caratheodory condition, see measure_theory.outer_measure.is_metric.borel_le_caratheodory.
• measure_theory.outer_measure.mk_metric' and its particular case measure_theory.outer_measure.mk_metric: a construction of an outer measure that is guaranteed to be metric. Both constructions are generalizations of the Hausdorff measure. The same measures interpreted as Borel measures are called measure_theory.measure.mk_metric' and measure_theory.measure.mk_metric.
• measure_theory.measure.hausdorff_measure a.k.a. μH[d]: the d-dimensional Hausdorff measure. There are many definitions of the Hausdorff measure that differ from each other by a multiplicative constant. We put μH[d] s = ⨆ r > 0, ⨅ (t : ℕ → set X) (hts : s ⊆ ⋃ n, t n) (ht : ∀ n, emetric.diam (t n) ≤ r), ∑' n, ⨆ (ht : ¬set.subsingleton (t n)), (emetric.diam (t n)) ^ d, see measure_theory.measure.hausdorff_measure_apply'. In the most interesting case 0 < d one can omit the ⨆ (ht : ¬set.subsingleton (t n)) part.

## Main statements #

### Basic properties #

• measure_theory.outer_measure.is_metric.borel_le_caratheodory: if μ is a metric outer measure on an extended metric space X (that is, it is additive on pairs of metric separated sets), then every Borel set is Caratheodory measurable (hence, μ defines an actual measure_theory.measure). See also measure_theory.measure.mk_metric.
• measure_theory.measure.hausdorff_measure_mono: μH[d] s is an antitone function of d.
• measure_theory.measure.hausdorff_measure_zero_or_top: if d₁ < d₂, then for any s, either μH[d₂] s = 0 or μH[d₁] s = ∞. Together with the previous lemma, this means that μH[d] s is equal to infinity on some ray (-∞, D) and is equal to zero on (D, +∞), where D is a possibly infinite number called the Hausdorff dimension of s; μH[D] s can be zero, infinity, or anything in between.
• measure_theory.measure.no_atoms_hausdorff: Hausdorff measure has no atoms.

### Hausdorff measure in ℝⁿ#

• measure_theory.hausdorff_measure_pi_real: for a nonempty ι, μH[card ι] on ι → ℝ equals Lebesgue measure.

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

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 I i j is_metric_separated (s i) (s j)) :
μ ( (i : ι) (H : i I), s i) = I.sum (λ (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.

noncomputable def measure_theory.outer_measure.mk_metric'.pre {X : Type u_2} (m : set X ennreal) (r : ennreal) :

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

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
noncomputable def measure_theory.outer_measure.mk_metric {X : Type u_2} (m : ennreal ennreal) :

Given a function m : ℝ≥0∞ → ℝ≥0∞ and r > 0, let μ r be the maximal outer measure such that μ s ≤ m (emetric.diam s) whenever emetric.diam s < r. Then mk_metric m = ⨆ r > 0, μ r.

Equations
theorem measure_theory.outer_measure.mk_metric'.le_pre {X : Type u_2} {m : set X ennreal} {r : ennreal}  :
(s : set X), μ s m s
theorem measure_theory.outer_measure.mk_metric'.pre_le {X : Type u_2} {m : set X ennreal} {r : ennreal} {s : set X} (hs : r) :
theorem measure_theory.outer_measure.mk_metric'.mono_pre {X : Type u_2} (m : set X ennreal) {r r' : ennreal} (h : r r') :
theorem measure_theory.outer_measure.mk_metric'.trim_pre {X : Type u_2} (m : set X ennreal) (hcl : (s : set X), m (closure s) = m s) (r : ennreal) :

measure_theory.outer_measure.mk_metric'.pre m r is a trimmed measure provided that m (closure s) = m s for any set s.

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₂ : ennreal ennreal} {c : ennreal} (hc : c ) (h0 : c 0) (hle : m₁ ≤ᶠ[ (set.Ici 0)] c m₂) :

If c ∉ {0, ∞} and m₁ d ≤ c * m₂ d for d < ε for some ε > 0 (we use ≤ᶠ[𝓝[≥] 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₂ : ennreal ennreal} (hle : m₁ ≤ᶠ[ (set.Ici 0)] m₂) :

If m₁ d ≤ m₂ d for d < ε for some ε > 0 (we use ≤ᶠ[𝓝[≥] 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 : ennreal ennreal) {f : X Y} (hf : isometry f) (H : ) :
theorem measure_theory.outer_measure.mk_metric_smul {X : Type u_2} (m : ennreal ennreal) {c : ennreal} (hc : c ) (hc' : c 0) :
theorem measure_theory.outer_measure.isometry_map_mk_metric {X : Type u_2} {Y : Type u_3} (m : ennreal ennreal) {f : X Y} (hf : isometry f) (H : ) :
theorem measure_theory.outer_measure.le_mk_metric {X : Type u_2} (m : ennreal ennreal) (r : ennreal) (h0 : 0 < r) (hr : (s : set X), μ s m (emetric.diam s)) :

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

noncomputable def measure_theory.measure.mk_metric' {X : Type u_2} [borel_space X] (m : set X ennreal) :

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
noncomputable def measure_theory.measure.mk_metric {X : Type u_2} [borel_space X] (m : ennreal ennreal) :

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₂ : ennreal ennreal} {c : ennreal} (hc : c ) (h0 : c 0) (hle : m₁ ≤ᶠ[ (set.Ici 0)] c m₂) :

If c ∉ {0, ∞} and m₁ d ≤ c * m₂ d for d < ε for some ε > 0 (we use ≤ᶠ[𝓝[≥] 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₂ : ennreal ennreal} (hle : m₁ ≤ᶠ[ (set.Ici 0)] m₂) :

If m₁ d ≤ m₂ d for d < ε for some ε > 0 (we use ≤ᶠ[𝓝[≥] 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 : ennreal ennreal) (s : set X) :
= (r : ennreal) (hr : 0 < r), (t : set X) (h : s (h' : (n : ), emetric.diam (t n) r), ∑' (n : ), (h : (t n).nonempty), m (emetric.diam (t n))

A formula for measure_theory.measure.mk_metric.

theorem measure_theory.measure.le_mk_metric {X : Type u_2} [borel_space X] (m : ennreal ennreal) (μ : measure_theory.measure X) (ε : ennreal) (h₀ : 0 < ε) (h : (s : set X), μ s m (emetric.diam s)) :
theorem measure_theory.measure.mk_metric_le_liminf_tsum {X : Type u_2} [borel_space X] {β : Type u_1} {ι : β Type u_3} [ (n : β), countable (ι n)] (s : set X) {l : filter β} (r : β ennreal) (hr : (nhds 0)) (t : Π (n : β), ι n set X) (ht : ∀ᶠ (n : β) in l, (i : ι n), emetric.diam (t n i) r n) (hst : ∀ᶠ (n : β) in l, s (i : ι n), t n i) (m : ennreal ennreal) :
filter.liminf (λ (n : β), ∑' (i : ι n), m (emetric.diam (t n i))) l

To bound the Hausdorff measure (or, more generally, for a measure defined using measure_theory.measure.mk_metric) of a set, one may use coverings with maximum diameter tending to 0, indexed by any sequence of countable types.

theorem measure_theory.measure.mk_metric_le_liminf_sum {X : Type u_2} [borel_space X] {β : Type u_1} {ι : β Type u_3} [hι : Π (n : β), fintype (ι n)] (s : set X) {l : filter β} (r : β ennreal) (hr : (nhds 0)) (t : Π (n : β), ι n set X) (ht : ∀ᶠ (n : β) in l, (i : ι n), emetric.diam (t n i) r n) (hst : ∀ᶠ (n : β) in l, s (i : ι n), t n i) (m : ennreal ennreal) :
filter.liminf (λ (n : β), finset.univ.sum (λ (i : ι n), m (emetric.diam (t n i)))) l

To bound the Hausdorff measure (or, more generally, for a measure defined using measure_theory.measure.mk_metric) of a set, one may use coverings with maximum diameter tending to 0, indexed by any sequence of finite types.

### Hausdorff measure and Hausdorff dimension #

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

Hausdorff measure on an (e)metric space.

Equations
Instances for measure_theory.measure.hausdorff_measure
theorem measure_theory.measure.le_hausdorff_measure {X : Type u_2} [borel_space X] (d : ) (μ : measure_theory.measure X) (ε : ennreal) (h₀ : 0 < ε) (h : (s : set X), μ s ) :
theorem measure_theory.measure.hausdorff_measure_apply {X : Type u_2} [borel_space X] (d : ) (s : set X) :
= (r : ennreal) (hr : 0 < r), (t : set X) (hts : s (n : ), t n) (ht : (n : ), emetric.diam (t n) r), ∑' (n : ), (h : (t n).nonempty), emetric.diam (t n) ^ d

A formula for μH[d] s.

theorem measure_theory.measure.hausdorff_measure_le_liminf_tsum {X : Type u_2} [borel_space X] {β : Type u_1} {ι : β Type u_3} [hι : (n : β), countable (ι n)] (d : ) (s : set X) {l : filter β} (r : β ennreal) (hr : (nhds 0)) (t : Π (n : β), ι n set X) (ht : ∀ᶠ (n : β) in l, (i : ι n), emetric.diam (t n i) r n) (hst : ∀ᶠ (n : β) in l, s (i : ι n), t n i) :
filter.liminf (λ (n : β), ∑' (i : ι n), emetric.diam (t n i) ^ d) l

To bound the Hausdorff measure of a set, one may use coverings with maximum diameter tending to 0, indexed by any sequence of countable types.

theorem measure_theory.measure.hausdorff_measure_le_liminf_sum {X : Type u_2} [borel_space X] {β : Type u_1} {ι : β Type u_3} [hι : Π (n : β), fintype (ι n)] (d : ) (s : set X) {l : filter β} (r : β ennreal) (hr : (nhds 0)) (t : Π (n : β), ι n set X) (ht : ∀ᶠ (n : β) in l, (i : ι n), emetric.diam (t n i) r n) (hst : ∀ᶠ (n : β) in l, s (i : ι n), t n i) :
filter.liminf (λ (n : β), finset.univ.sum (λ (i : ι n), emetric.diam (t n i) ^ d)) l

To bound the Hausdorff measure of a set, one may use coverings with maximum diameter tending to 0, indexed by any sequence of finite types.

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

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) :

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

theorem measure_theory.measure.no_atoms_hausdorff (X : Type u_2) [borel_space X] {d : } (hd : 0 < d) :

### Hausdorff measure, Hausdorff dimension, and Hölder or Lipschitz continuous maps #

theorem holder_on_with.hausdorff_measure_image_le {X : Type u_2} {Y : Type u_3} [borel_space X] [borel_space Y] {C r : nnreal} {f : X Y} {s : set X} (h : f s) (hr : 0 < r) {d : } (hd : 0 d) :
C ^ d *

If f : X → Y is Hölder continuous on s with a positive exponent r, then μH[d] (f '' s) ≤ C ^ d * μH[r * d] s.

theorem lipschitz_on_with.hausdorff_measure_image_le {X : Type u_2} {Y : Type u_3} [borel_space X] [borel_space Y] {K : nnreal} {f : X Y} {s : set X} (h : s) {d : } (hd : 0 d) :

If f : X → Y is K-Lipschitz on s, then μH[d] (f '' s) ≤ K ^ d * μH[d] s.

theorem lipschitz_with.hausdorff_measure_image_le {X : Type u_2} {Y : Type u_3} [borel_space X] [borel_space Y] {K : nnreal} {f : X Y} (h : f) {d : } (hd : 0 d) (s : set X) :

If f is a K-Lipschitz map, then it increases the Hausdorff d-measures of sets at most by the factor of K ^ d.

theorem measure_theory.measure.hausdorff_measure_smul₀ {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [ E] [borel_space E] {d : } (hd : 0 d) {r : 𝕜} (hr : r 0) (s : set E) :
=

### Antilipschitz maps do not decrease Hausdorff measures and dimension #

theorem antilipschitz_with.hausdorff_measure_preimage_le {X : Type u_2} {Y : Type u_3} [borel_space X] [borel_space Y] {f : X Y} {K : nnreal} {d : } (hf : f) (hd : 0 d) (s : set Y) :
theorem antilipschitz_with.le_hausdorff_measure_image {X : Type u_2} {Y : Type u_3} [borel_space X] [borel_space Y] {f : X Y} {K : nnreal} {d : } (hf : f) (hd : 0 d) (s : set X) :
K ^ d *

### Isometries preserve the Hausdorff measure and Hausdorff dimension #

theorem isometry.hausdorff_measure_image {X : Type u_2} {Y : Type u_3} [borel_space X] [borel_space Y] {f : X Y} {d : } (hf : isometry f) (hd : 0 d ) (s : set X) :
theorem isometry.hausdorff_measure_preimage {X : Type u_2} {Y : Type u_3} [borel_space X] [borel_space Y] {f : X Y} {d : } (hf : isometry f) (hd : 0 d ) (s : set Y) :
theorem isometry.map_hausdorff_measure {X : Type u_2} {Y : Type u_3} [borel_space X] [borel_space Y] {f : X Y} {d : } (hf : isometry f) (hd : 0 d ) :
@[simp]
theorem isometry_equiv.hausdorff_measure_image {X : Type u_2} {Y : Type u_3} [borel_space X] [borel_space Y] (e : X ≃ᵢ Y) (d : ) (s : set X) :
@[simp]
theorem isometry_equiv.hausdorff_measure_preimage {X : Type u_2} {Y : Type u_3} [borel_space X] [borel_space Y] (e : X ≃ᵢ Y) (d : ) (s : set Y) :
@[simp]
theorem isometry_equiv.map_hausdorff_measure {X : Type u_2} {Y : Type u_3} [borel_space X] [borel_space Y] (e : X ≃ᵢ Y) (d : ) :
theorem isometry_equiv.measure_preserving_hausdorff_measure {X : Type u_2} {Y : Type u_3} [borel_space X] [borel_space Y] (e : X ≃ᵢ Y) (d : ) :
theorem measure_theory.hausdorff_measure_smul {X : Type u_2} [borel_space X] {α : Type u_1} [ X] [ X] {d : } (c : α) (h : 0 d ) (s : set X) :
theorem measure_theory.hausdorff_measure_vadd {X : Type u_2} [borel_space X] {α : Type u_1} [ X] [ X] {d : } (c : α) (h : 0 d ) (s : set X) :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]

### Hausdorff measure and Lebesgue measure #

@[simp]

In the space ι → ℝ, the Hausdorff measure coincides exactly with the Lebesgue measure.

theorem measure_theory.hausdorff_measure_measure_preserving_pi_fin_two (α : fin 2 Type u_1) [Π (i : fin 2), measurable_space (α i)] [Π (i : fin 2), emetric_space (α i)] [ (i : fin 2), borel_space (α i)] [ (i : fin 2), ] (d : ) :
@[simp]

In the space ℝ, the Hausdorff measure coincides exactly with the Lebesgue measure.

@[simp]

In the space ℝ × ℝ, the Hausdorff measure coincides exactly with the Lebesgue measure.

### Geometric results in affine spaces #

theorem measure_theory.hausdorff_measure_smul_right_image {E : Type u_5} [ E] [borel_space E] (v : E) (s : set ) :
((λ (r : ), r v) '' s) =
theorem measure_theory.hausdorff_measure_homothety_image {𝕜 : Type u_4} {E : Type u_5} {P : Type u_6} [normed_field 𝕜] [ E] [metric_space P] [ P] [borel_space P] {d : } (hd : 0 d) (x : P) {c : 𝕜} (hc : c 0) (s : set P) :
=

Scaling by c around x scales the measure by ‖c‖₊ ^ d.

theorem measure_theory.hausdorff_measure_homothety_preimage {𝕜 : Type u_4} {E : Type u_5} {P : Type u_6} [normed_field 𝕜] [ E] [metric_space P] [ P] [borel_space P] {d : } (hd : 0 d) (x : P) {c : 𝕜} (hc : c 0) (s : set P) :

TODO: prove measure.map (affine_map.homothety x c) μH[d] = ‖c‖₊⁻¹ ^ d • μH[d], which needs a more general version of affine_map.homothety_continuous

theorem measure_theory.hausdorff_measure_line_map_image {E : Type u_5} {P : Type u_6} [ E] [metric_space P] [ P] [borel_space P] (x y : P) (s : set ) :

Mapping a set of reals along a line segment scales the measure by the length of a segment.

This is an auxiliary result used to prove hausdorff_measure_affine_segment.

@[simp]
theorem measure_theory.hausdorff_measure_affine_segment {E : Type u_5} {P : Type u_6} [ E] [metric_space P] [ P] [borel_space P] (x y : P) :

The measure of a segment is the distance between its endpoints.

@[simp]
theorem measure_theory.hausdorff_measure_segment {E : Type u_1} [ E] [borel_space E] (x y : E) :

The measure of a segment is the distance between its endpoints.