# mathlibdocumentation

topology.metric_space.hausdorff_dimension

# Hausdorff dimension #

The Hausdorff dimension of a set X in an (extended) metric space is the unique number dimH s : ℝ≥0∞ such that for any d : ℝ≥0 we have

• μH[d] s = 0 if dimH s < d, and
• μH[d] s = ∞ if d < dimH s.

In this file we define dimH s to be the Hausdorff dimension of s, then prove some basic properties of Hausdorff dimension.

## Main definitions #

• measure_theory.dimH: the Hausdorff dimension of a set. For the Hausdorff dimension of the whole space we use measure_theory.dimH (set.univ : set X).

## Main results #

### Basic properties of Hausdorff dimension #

• hausdorff_measure_of_lt_dimH, dimH_le_of_hausdorff_measure_ne_top, le_dimH_of_hausdorff_measure_eq_top, hausdorff_measure_of_dimH_lt, measure_zero_of_dimH_lt, le_dimH_of_hausdorff_measure_ne_zero, dimH_of_hausdorff_measure_ne_zero_ne_top: various forms of the characteristic property of the Hausdorff dimension;
• dimH_union: the Hausdorff dimension of the union of two sets is the maximum of their Hausdorff dimensions.
• dimH_Union, dimH_bUnion, dimH_sUnion: the Hausdorff dimension of a countable union of sets is the supremum of their Hausdorff dimensions;
• dimH_empty, dimH_singleton, set.subsingleton.dimH_zero, set.countable.dimH_zero : dimH s = 0 whenever s is countable;

### (Pre)images under (anti)lipschitz and Hölder continuous maps #

• holder_with.dimH_image_le etc: if f : X → Y is Hölder continuous with exponent r > 0, then for any s, dimH (f '' s) ≤ dimH s / r. We prove versions of this statement for holder_with, holder_on_with, and locally Hölder maps, as well as for set.image and set.range.
• lipschitz_with.dimH_image_le etc: Lipschitz continuous maps do not increase the Hausdorff dimension of sets.
• for a map that is known to be both Lipschitz and antilipschitz (e.g., for an isometry or a continuous_linear_equiv) we also prove dimH (f '' s) = dimH s.

### Hausdorff measure in ℝⁿ#

• real.dimH_of_nonempty_interior: if s is a set in a finite dimensional real vector space E with nonempty interior, then the Hausdorff dimension of s is equal to the dimension of E.
• dense_compl_of_dimH_lt_finrank: if s is a set in a finite dimensional real vector space E with Hausdorff dimension strictly less than the dimension of E, the s has a dense complement.
• times_cont_diff.dense_compl_range_of_finrank_lt_finrank: the complement to the range of a C¹ smooth map is dense provided that the dimension of the domain is strictly less than the dimension of the codomain.

## Notations #

We use the following notation localized in measure_theory. It is defined in measure_theory.measure.hausdorff.

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

## Implementation notes #

• The definition of dimH explicitly uses borel X as a measurable space structure. This way we can formulate lemmas about Hausdorff dimension without assuming that the environment has a [measurable_space X] instance that is equal but possibly not defeq to borel X.

Lemma dimH_def unfolds this definition using whatever [measurable_space X] instance we have in the environment (as long as it is equal to borel X).

• The definition dimH is irreducible; use API lemmas or dimH_def instead.

## Tags #

Hausdorff measure, Hausdorff dimension, dimension

def dimH {X : Type u_2} (s : set X) :

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

Equations

### Basic properties #

theorem dimH_def {X : Type u_2} [borel_space X] (s : set X) :
dimH s = ⨆ (d : ℝ≥0) (hd : μH[d] s = ), d

Unfold the definition of dimH using [measurable_space X] [borel_space X] from the environment.

theorem hausdorff_measure_of_lt_dimH {X : Type u_2} [borel_space X] {s : set X} {d : ℝ≥0} (h : d < dimH s) :
theorem dimH_le {X : Type u_2} [borel_space X] {s : set X} {d : ℝ≥0∞} (H : ∀ (d' : ℝ≥0), μH[d'] s = d' d) :
dimH s d
theorem dimH_le_of_hausdorff_measure_ne_top {X : Type u_2} [borel_space X] {s : set X} {d : ℝ≥0} (h : μH[d] s ) :
theorem le_dimH_of_hausdorff_measure_eq_top {X : Type u_2} [borel_space X] {s : set X} {d : ℝ≥0} (h : μH[d] s = ) :
theorem hausdorff_measure_of_dimH_lt {X : Type u_2} [borel_space X] {s : set X} {d : ℝ≥0} (h : dimH s < d) :
theorem 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 : dimH s < d) :
μ s = 0
theorem le_dimH_of_hausdorff_measure_ne_zero {X : Type u_2} [borel_space X] {s : set X} {d : ℝ≥0} (h : μH[d] s 0) :
theorem dimH_of_hausdorff_measure_ne_zero_ne_top {X : Type u_2} [borel_space X] {d : ℝ≥0} {s : set X} (h : μH[d] s 0) (h' : μH[d] s ) :
theorem dimH_mono {X : Type u_2} {s t : set X} (h : s t) :
theorem dimH_subsingleton {X : Type u_2} {s : set X} (h : s.subsingleton) :
dimH s = 0
theorem set.subsingleton.dimH_zero {X : Type u_2} {s : set X} (h : s.subsingleton) :
dimH s = 0

Alias of dimH_subsingleton.

@[simp]
theorem dimH_empty {X : Type u_2}  :
= 0
@[simp]
theorem dimH_singleton {X : Type u_2} (x : X) :
dimH {x} = 0
@[simp]
theorem dimH_Union {ι : Type u_1} {X : Type u_2} [encodable ι] (s : ι → set X) :
dimH (⋃ (i : ι), s i) = ⨆ (i : ι), dimH (s i)
@[simp]
theorem dimH_bUnion {ι : Type u_1} {X : Type u_2} {s : set ι} (hs : s.countable) (t : ι → set X) :
dimH (⋃ (i : ι) (H : i s), t i) = ⨆ (i : ι) (H : i s), dimH (t i)
@[simp]
theorem dimH_sUnion {X : Type u_2} {S : set (set X)} (hS : S.countable) :
dimH (⋃₀S) = ⨆ (s : set X) (H : s S), dimH s
@[simp]
theorem dimH_union {X : Type u_2} (s t : set X) :
dimH (s t) = max (dimH s) (dimH t)
theorem dimH_countable {X : Type u_2} {s : set X} (hs : s.countable) :
dimH s = 0
theorem set.countable.dimH_zero {X : Type u_2} {s : set X} (hs : s.countable) :
dimH s = 0

Alias of dimH_countable.

theorem dimH_finite {X : Type u_2} {s : set X} (hs : s.finite) :
dimH s = 0
theorem set.finite.dimH_zero {X : Type u_2} {s : set X} (hs : s.finite) :
dimH s = 0

Alias of dimH_finite.

@[simp]
theorem dimH_coe_finset {X : Type u_2} (s : finset X) :
= 0
theorem finset.dimH_zero {X : Type u_2} (s : finset X) :
= 0

Alias of dimH_coe_finset.

### Hausdorff dimension and Hölder continuity #

theorem holder_on_with.dimH_image_le {X : Type u_2} {Y : Type u_3} {C r : ℝ≥0} {f : X → Y} {s : set X} (h : f s) (hr : 0 < r) :
dimH (f '' s) dimH s / r

If f is a Hölder continuous map with exponent r > 0, then dimH (f '' s) ≤ dimH s / r.

theorem holder_with.dimH_image_le {X : Type u_2} {Y : Type u_3} {C r : ℝ≥0} {f : X → Y} (h : r f) (hr : 0 < r) (s : set X) :
dimH (f '' s) dimH s / r

If f : X → Y is Hölder continuous with a positive exponent r, then the Hausdorff dimension of the image of a set s is at most dimH s / r.

theorem holder_with.dimH_range_le {X : Type u_2} {Y : Type u_3} {C r : ℝ≥0} {f : X → Y} (h : r f) (hr : 0 < r) :

If f is a Hölder continuous map with exponent r > 0, then the Hausdorff dimension of its range is at most the Hausdorff dimension of its domain divided by r.

theorem dimH_image_le_of_locally_holder_on {X : Type u_2} {Y : Type u_3} {r : ℝ≥0} {f : X → Y} (hr : 0 < r) {s : set X} (hf : ∀ (x : X), x s(∃ (C : ℝ≥0) (t : set X) (H : t 𝓝[s] x), f t)) :
dimH (f '' s) dimH s / r

If s is a set in a space X with second countable topology and f : X → Y is Hölder continuous in a neighborhood within s of every point x ∈ s with the same positive exponent r but possibly different coefficients, then the Hausdorff dimension of the image f '' s is at most the Hausdorff dimension of s divided by r.

theorem dimH_range_le_of_locally_holder_on {X : Type u_2} {Y : Type u_3} {r : ℝ≥0} {f : X → Y} (hr : 0 < r) (hf : ∀ (x : X), ∃ (C : ℝ≥0) (s : set X) (H : s 𝓝 x), f s) :

If f : X → Y is Hölder continuous in a neighborhood of every point x : X with the same positive exponent r but possibly different coefficients, then the Hausdorff dimension of the range of f is at most the Hausdorff dimension of X divided by r.

### Hausdorff dimension and Lipschitz continuity #

theorem lipschitz_on_with.dimH_image_le {X : Type u_2} {Y : Type u_3} {K : ℝ≥0} {f : X → Y} {s : set X} (h : s) :
dimH (f '' s) dimH s

If f : X → Y is Lipschitz continuous on s, then dimH (f '' s) ≤ dimH s.

theorem lipschitz_with.dimH_image_le {X : Type u_2} {Y : Type u_3} {K : ℝ≥0} {f : X → Y} (h : f) (s : set X) :
dimH (f '' s) dimH s

If f is a Lipschitz continuous map, then dimH (f '' s) ≤ dimH s.

theorem lipschitz_with.dimH_range_le {X : Type u_2} {Y : Type u_3} {K : ℝ≥0} {f : X → Y} (h : f) :

If f is a Lipschitz continuous map, then the Hausdorff dimension of its range is at most the Hausdorff dimension of its domain.

theorem dimH_image_le_of_locally_lipschitz_on {X : Type u_2} {Y : Type u_3} {f : X → Y} {s : set X} (hf : ∀ (x : X), x s(∃ (C : ℝ≥0) (t : set X) (H : t 𝓝[s] x), t)) :
dimH (f '' s) dimH s

If s is a set in an extended metric space X with second countable topology and f : X → Y is Lipschitz in a neighborhood within s of every point x ∈ s, then the Hausdorff dimension of the image f '' s is at most the Hausdorff dimension of s.

theorem dimH_range_le_of_locally_lipschitz_on {X : Type u_2} {Y : Type u_3} {f : X → Y} (hf : ∀ (x : X), ∃ (C : ℝ≥0) (s : set X) (H : s 𝓝 x), s) :

If f : X → Y is Lipschitz in a neighborhood of each point x : X, then the Hausdorff dimension of range f is at most the Hausdorff dimension of X.

theorem antilipschitz_with.dimH_preimage_le {X : Type u_2} {Y : Type u_3} {K : ℝ≥0} {f : X → Y} (hf : f) (s : set Y) :
theorem antilipschitz_with.le_dimH_image {X : Type u_2} {Y : Type u_3} {K : ℝ≥0} {f : X → Y} (hf : f) (s : set X) :
dimH s dimH (f '' s)

### Isometries preserve Hausdorff dimension #

theorem isometry.dimH_image {X : Type u_2} {Y : Type u_3} {f : X → Y} (hf : isometry f) (s : set X) :
dimH (f '' s) = dimH s
@[simp]
theorem isometric.dimH_image {X : Type u_2} {Y : Type u_3} (e : X ≃ᵢ Y) (s : set X) :
dimH (e '' s) = dimH s
@[simp]
theorem isometric.dimH_preimage {X : Type u_2} {Y : Type u_3} (e : X ≃ᵢ Y) (s : set Y) :
theorem isometric.dimH_univ {X : Type u_2} {Y : Type u_3} (e : X ≃ᵢ Y) :
@[simp]
theorem continuous_linear_equiv.dimH_image {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [normed_group E] [ E] [normed_group F] [ F] (e : E ≃L[𝕜] F) (s : set E) :
dimH (e '' s) = dimH s
@[simp]
theorem continuous_linear_equiv.dimH_preimage {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [normed_group E] [ E] [normed_group F] [ F] (e : E ≃L[𝕜] F) (s : set F) :
theorem continuous_linear_equiv.dimH_univ {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [normed_group E] [ E] [normed_group F] [ F] (e : E ≃L[𝕜] F) :

### Hausdorff dimension in a real vector space #

theorem real.dimH_ball_pi {ι : Type u_1} [fintype ι] (x : ι → ) {r : } (hr : 0 < r) :
theorem real.dimH_ball_pi_fin {n : } (x : fin n) {r : } (hr : 0 < r) :
dimH r) = n
theorem real.dimH_univ_pi (ι : Type u_1) [fintype ι] :
theorem real.dimH_univ_pi_fin (n : ) :
theorem real.dimH_of_mem_nhds {E : Type u_4} [normed_group E] [ E] {x : E} {s : set E} (h : s 𝓝 x) :
theorem real.dimH_of_nonempty_interior {E : Type u_4} [normed_group E] [ E] {s : set E} (h : (interior s).nonempty) :
theorem real.dimH_univ_eq_finrank (E : Type u_4) [normed_group E] [ E]  :
theorem real.dimH_univ  :
theorem dense_compl_of_dimH_lt_finrank {E : Type u_4} [normed_group E] [ E] {s : set E} (hs : dimH s < ) :

### Hausdorff dimension and C¹-smooth maps #

C¹-smooth maps are locally Lipschitz continuous, hence they do not increase the Hausdorff dimension of sets.

theorem times_cont_diff_on.dimH_image_le {E : Type u_4} {F : Type u_5} [normed_group E] [ E] [normed_group F] [ F] {f : E → F} {s t : set E} (hf : s) (hc : s) (ht : t s) :
dimH (f '' t) dimH t

Let f be a function defined on a finite dimensional real normed space. If f is C¹-smooth on a convex set s, then the Hausdorff dimension of f '' s is less than or equal to the Hausdorff dimension of s.

TODO: do we actually need convex ℝ s?

theorem times_cont_diff.dimH_range_le {E : Type u_4} {F : Type u_5} [normed_group E] [ E] [normed_group F] [ F] {f : E → F} (h : f) :

The Hausdorff dimension of the range of a C¹-smooth function defined on a finite dimensional real normed space is at most the dimension of its domain as a vector space over ℝ.

theorem times_cont_diff_on.dense_compl_image_of_dimH_lt_finrank {E : Type u_4} {F : Type u_5} [normed_group E] [ E] [normed_group F] [ F] {f : E → F} {s t : set E} (h : s) (hc : s) (ht : t s) (htF : dimH t < ) :
dense (f '' t)

A particular case of Sard's Theorem. Let f : E → F be a map between finite dimensional real vector spaces. Suppose that f is C¹ smooth on a convex set s of Hausdorff dimension strictly less than the dimension of F. Then the complement of the image f '' s is dense in F.

theorem times_cont_diff.dense_compl_range_of_finrank_lt_finrank {E : Type u_4} {F : Type u_5} [normed_group E] [ E] [normed_group F] [ F] {f : E → F} (h : f)  :

A particular case of Sard's Theorem. If f is a C¹ smooth map from a real vector space to a real vector space F of strictly larger dimension, then the complement of the range of f is dense in F.