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

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

## Main results #

### Basic properties of Hausdorff dimension #

• hausdorffMeasure_of_lt_dimH, dimH_le_of_hausdorffMeasure_ne_top, le_dimH_of_hausdorffMeasure_eq_top, hausdorffMeasure_of_dimH_lt, measure_zero_of_dimH_lt, le_dimH_of_hausdorffMeasure_ne_zero, dimH_of_hausdorffMeasure_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_iUnion, 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 #

• HolderWith.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 HolderWith, HolderOnWith, and locally Hölder maps, as well as for Set.image and Set.range.
• LipschitzWith.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 ContinuousLinearEquiv) 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.
• ContDiff.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 MeasureTheory. It is defined in MeasureTheory.Measure.Hausdorff.

• μH[d] : MeasureTheory.Measure.hausdorffMeasure 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 [MeasurableSpace X] instance that is equal but possibly not defeq to borel X.

Lemma dimH_def unfolds this definition using whatever [MeasurableSpace 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

@[irreducible]
noncomputable def dimH {X : Type u_2} [] (s : Set X) :

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

Equations
Instances For

### Basic properties #

theorem dimH_def {X : Type u_2} [] [] [] (s : Set X) :
dimH s = ⨆ (d : NNReal), ⨆ (_ : ), d

Unfold the definition of dimH using [MeasurableSpace X] [BorelSpace X] from the environment.

theorem hausdorffMeasure_of_lt_dimH {X : Type u_2} [] [] [] {s : Set X} {d : NNReal} (h : d < dimH s) :
theorem dimH_le {X : Type u_2} [] [] [] {s : Set X} {d : ENNReal} (H : ∀ (d' : NNReal), d' d) :
dimH s d
theorem dimH_le_of_hausdorffMeasure_ne_top {X : Type u_2} [] [] [] {s : Set X} {d : NNReal} (h : ) :
dimH s d
theorem le_dimH_of_hausdorffMeasure_eq_top {X : Type u_2} [] [] [] {s : Set X} {d : NNReal} (h : ) :
d dimH s
theorem hausdorffMeasure_of_dimH_lt {X : Type u_2} [] [] [] {s : Set X} {d : NNReal} (h : dimH s < d) :
theorem measure_zero_of_dimH_lt {X : Type u_2} [] [] [] {μ : } {d : NNReal} (h : μ.AbsolutelyContinuous ) {s : Set X} (hd : dimH s < d) :
μ s = 0
theorem le_dimH_of_hausdorffMeasure_ne_zero {X : Type u_2} [] [] [] {s : Set X} {d : NNReal} (h : ) :
d dimH s
theorem dimH_of_hausdorffMeasure_ne_zero_ne_top {X : Type u_2} [] [] [] {d : NNReal} {s : Set X} (h : ) (h' : ) :
dimH s = d
theorem dimH_mono {X : Type u_2} [] {s : Set X} {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_iUnion {X : Type u_2} [] {ι : Sort u_4} [] (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 (⋃ is, t i) = is, dimH (t i)
@[simp]
theorem dimH_sUnion {X : Type u_2} [] {S : Set (Set X)} (hS : S.Countable) :
dimH (⋃₀ S) = sS, dimH s
@[simp]
theorem dimH_union {X : Type u_2} [] (s : Set X) (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 : ) :
dimH s = 0
theorem Finset.dimH_zero {X : Type u_2} [] (s : ) :
dimH s = 0

Alias of dimH_coe_finset.

### Hausdorff dimension as the supremum of local Hausdorff dimensions #

theorem exists_mem_nhdsWithin_lt_dimH_of_lt_dimH {X : Type u_2} [] {s : Set X} {r : ENNReal} (h : r < dimH s) :
xs, t, r < dimH t

If r is less than the Hausdorff dimension of a set s in an (extended) metric space with second countable topology, then there exists a point x ∈ s such that every neighborhood t of x within s has Hausdorff dimension greater than r.

theorem bsupr_limsup_dimH {X : Type u_2} [] (s : Set X) :
xs, Filter.limsup dimH (nhdsWithin x s).smallSets = dimH s

In an (extended) metric space with second countable topology, the Hausdorff dimension of a set s is the supremum over x ∈ s of the limit superiors of dimH t along (𝓝[s] x).smallSets.

theorem iSup_limsup_dimH {X : Type u_2} [] (s : Set X) :
⨆ (x : X), Filter.limsup dimH (nhdsWithin x s).smallSets = dimH s

In an (extended) metric space with second countable topology, the Hausdorff dimension of a set s is the supremum over all x of the limit superiors of dimH t along (𝓝[s] x).smallSets.

### Hausdorff dimension and Hölder continuity #

theorem HolderOnWith.dimH_image_le {X : Type u_2} {Y : Type u_3} [] [] {C : NNReal} {r : NNReal} {f : XY} {s : Set X} (h : HolderOnWith C r 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 HolderWith.dimH_image_le {X : Type u_2} {Y : Type u_3} [] [] {C : NNReal} {r : NNReal} {f : XY} (h : HolderWith C 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 HolderWith.dimH_range_le {X : Type u_2} {Y : Type u_3} [] [] {C : NNReal} {r : NNReal} {f : XY} (h : HolderWith C r f) (hr : 0 < r) :
dimH (Set.range f) dimH Set.univ / 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 : NNReal} {f : XY} (hr : 0 < r) {s : Set X} (hf : xs, ∃ (C : NNReal), t, HolderOnWith C r 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 : NNReal} {f : XY} (hr : 0 < r) (hf : ∀ (x : X), ∃ (C : NNReal), snhds x, HolderOnWith C r f s) :
dimH (Set.range f) dimH Set.univ / r

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 LipschitzOnWith.dimH_image_le {X : Type u_2} {Y : Type u_3} [] [] {K : NNReal} {f : XY} {s : Set X} (h : ) :
dimH (f '' s) dimH s

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

theorem LipschitzWith.dimH_image_le {X : Type u_2} {Y : Type u_3} [] [] {K : NNReal} {f : XY} (h : ) (s : Set X) :
dimH (f '' s) dimH s

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

theorem LipschitzWith.dimH_range_le {X : Type u_2} {Y : Type u_3} [] [] {K : NNReal} {f : XY} (h : ) :
dimH (Set.range f) dimH Set.univ

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_lipschitzOn {X : Type u_2} {Y : Type u_3} [] [] {f : XY} {s : Set X} (hf : xs, ∃ (C : NNReal), 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_lipschitzOn {X : Type u_2} {Y : Type u_3} [] [] {f : XY} (hf : ∀ (x : X), ∃ (C : NNReal), snhds x, ) :
dimH (Set.range f) dimH Set.univ

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 AntilipschitzWith.dimH_preimage_le {X : Type u_2} {Y : Type u_3} [] [] {K : NNReal} {f : XY} (hf : ) (s : Set Y) :
theorem AntilipschitzWith.le_dimH_image {X : Type u_2} {Y : Type u_3} [] [] {K : NNReal} {f : XY} (hf : ) (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 : XY} (hf : ) (s : Set X) :
dimH (f '' s) = dimH s
@[simp]
theorem IsometryEquiv.dimH_image {X : Type u_2} {Y : Type u_3} [] [] (e : X ≃ᵢ Y) (s : Set X) :
dimH (e '' s) = dimH s
@[simp]
theorem IsometryEquiv.dimH_preimage {X : Type u_2} {Y : Type u_3} [] [] (e : X ≃ᵢ Y) (s : Set Y) :
dimH (e ⁻¹' s) = dimH s
theorem IsometryEquiv.dimH_univ {X : Type u_2} {Y : Type u_3} [] [] (e : X ≃ᵢ Y) :
dimH Set.univ = dimH Set.univ
@[simp]
theorem ContinuousLinearEquiv.dimH_image {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [] [] (e : E ≃L[𝕜] F) (s : Set E) :
dimH (e '' s) = dimH s
@[simp]
theorem ContinuousLinearEquiv.dimH_preimage {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [] [] (e : E ≃L[𝕜] F) (s : Set F) :
dimH (e ⁻¹' s) = dimH s
theorem ContinuousLinearEquiv.dimH_univ {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [] [] (e : E ≃L[𝕜] F) :
dimH Set.univ = dimH Set.univ

### Hausdorff dimension in a real vector space #

theorem Real.dimH_ball_pi {ι : Type u_1} [] (x : ι) {r : } (hr : 0 < r) :
theorem Real.dimH_ball_pi_fin {n : } (x : Fin n) {r : } (hr : 0 < r) :
dimH (Metric.ball x r) = n
theorem Real.dimH_univ_pi (ι : Type u_5) [] :
dimH Set.univ = (Fintype.card ι)
theorem Real.dimH_univ_pi_fin (n : ) :
dimH Set.univ = n
theorem Real.dimH_of_mem_nhds {E : Type u_4} [] [] {x : E} {s : Set E} (h : s nhds x) :
dimH s =
theorem Real.dimH_of_nonempty_interior {E : Type u_4} [] [] {s : Set E} (h : (interior s).Nonempty) :
dimH s =
theorem Real.dimH_univ_eq_finrank (E : Type u_4) [] [] :
dimH Set.univ =
theorem Real.dimH_univ :
dimH Set.univ = 1
theorem Real.hausdorffMeasure_of_finrank_lt {E : Type u_4} [] [] [] [] {d : } (hd : < d) :
theorem dense_compl_of_dimH_lt_finrank {E : Type u_4} [] [] {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 ContDiffOn.dimH_image_le {E : Type u_4} {F : Type u_5} [] [] [] {f : EF} {s : Set E} {t : Set E} (hf : ContDiffOn 1 f s) (hc : ) (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 ContDiff.dimH_range_le {E : Type u_4} {F : Type u_5} [] [] [] {f : EF} (h : ) :

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 ContDiffOn.dense_compl_image_of_dimH_lt_finrank {E : Type u_4} {F : Type u_5} [] [] [] [] {f : EF} {s : Set E} {t : Set E} (h : ContDiffOn 1 f s) (hc : ) (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 ContDiff.dense_compl_range_of_finrank_lt_finrank {E : Type u_4} {F : Type u_5} [] [] [] [] {f : EF} (h : ) (hEF : ) :

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.