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} [EMetricSpace X] (s : Set X) : ENNReal

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

Equations

• dimH s = ⨆ (d : NNReal), ⨆ (_ : (MeasureTheory.Measure.hausdorffMeasure ↑d) s = ⊤), ↑d

Basic properties

theorem dimH_def {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] (s : Set X) : dimH s = ⨆ (d : NNReal), ⨆ (_ : (MeasureTheory.Measure.hausdorffMeasure ↑d) s = ⊤), ↑d

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

theorem hausdorffMeasure_of_lt_dimH {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {s : Set X} {d : NNReal} (h : ↑d < dimH s) : (MeasureTheory.Measure.hausdorffMeasure ↑d) s = ⊤

theorem dimH_le {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {s : Set X} {d : ENNReal} (H : ∀ (d' : NNReal), (MeasureTheory.Measure.hausdorffMeasure ↑d') s = ⊤ → ↑d' ≤ d) : dimH s ≤ d

theorem dimH_le_of_hausdorffMeasure_ne_top {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {s : Set X} {d : NNReal} (h : (MeasureTheory.Measure.hausdorffMeasure ↑d) s ≠ ⊤) : dimH s ≤ ↑d

theorem le_dimH_of_hausdorffMeasure_eq_top {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {s : Set X} {d : NNReal} (h : (MeasureTheory.Measure.hausdorffMeasure ↑d) s = ⊤) : ↑d ≤ dimH s

theorem hausdorffMeasure_of_dimH_lt {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {s : Set X} {d : NNReal} (h : dimH s < ↑d) : (MeasureTheory.Measure.hausdorffMeasure ↑d) s = 0

theorem measure_zero_of_dimH_lt {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {μ : MeasureTheory.Measure X} {d : NNReal} (h : μ.AbsolutelyContinuous (MeasureTheory.Measure.hausdorffMeasure ↑d)) {s : Set X} (hd : dimH s < ↑d) : μ s = 0

theorem le_dimH_of_hausdorffMeasure_ne_zero {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {s : Set X} {d : NNReal} (h : (MeasureTheory.Measure.hausdorffMeasure ↑d) s ≠ 0) : ↑d ≤ dimH s

theorem dimH_of_hausdorffMeasure_ne_zero_ne_top {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {d : NNReal} {s : Set X} (h : (MeasureTheory.Measure.hausdorffMeasure ↑d) s ≠ 0) (h' : (MeasureTheory.Measure.hausdorffMeasure ↑d) s ≠ ⊤) : dimH s = ↑d

theorem dimH_mono {X : Type u_2} [EMetricSpace X] {s t : Set X} (h : s ⊆ t) : dimH s ≤ dimH t

theorem dimH_subsingleton {X : Type u_2} [EMetricSpace X] {s : Set X} (h : s.Subsingleton) : dimH s = 0

theorem Set.Subsingleton.dimH_zero {X : Type u_2} [EMetricSpace X] {s : Set X} (h : s.Subsingleton) : dimH s = 0

Alias of dimH_subsingleton.

@[simp]

theorem dimH_empty {X : Type u_2} [EMetricSpace X] : dimH ∅ = 0

@[simp]

theorem dimH_singleton {X : Type u_2} [EMetricSpace X] (x : X) : dimH {x} = 0

@[simp]

theorem dimH_iUnion {X : Type u_2} [EMetricSpace X] {ι : Sort u_4} [Countable ι] (s : ι → Set X) : dimH (⋃ (i : ι), s i) = ⨆ (i : ι), dimH (s i)

@[simp]

theorem dimH_bUnion {ι : Type u_1} {X : Type u_2} [EMetricSpace X] {s : Set ι} (hs : s.Countable) (t : ι → Set X) : dimH (⋃ i ∈ s, t i) = ⨆ i ∈ s, dimH (t i)

@[simp]

theorem dimH_sUnion {X : Type u_2} [EMetricSpace X] {S : Set (Set X)} (hS : S.Countable) : dimH (⋃₀ S) = ⨆ s ∈ S, dimH s

@[simp]

theorem dimH_union {X : Type u_2} [EMetricSpace X] (s t : Set X) : dimH (s ∪ t) = max (dimH s) (dimH t)

theorem dimH_countable {X : Type u_2} [EMetricSpace X] {s : Set X} (hs : s.Countable) : dimH s = 0

theorem Set.Countable.dimH_zero {X : Type u_2} [EMetricSpace X] {s : Set X} (hs : s.Countable) : dimH s = 0

Alias of dimH_countable.

theorem dimH_finite {X : Type u_2} [EMetricSpace X] {s : Set X} (hs : s.Finite) : dimH s = 0

theorem Set.Finite.dimH_zero {X : Type u_2} [EMetricSpace X] {s : Set X} (hs : s.Finite) : dimH s = 0

Alias of dimH_finite.

@[simp]

theorem dimH_coe_finset {X : Type u_2} [EMetricSpace X] (s : Finset X) : dimH ↑s = 0

theorem Finset.dimH_zero {X : Type u_2} [EMetricSpace X] (s : Finset X) : 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} [EMetricSpace X] [SecondCountableTopology X] {s : Set X} {r : ENNReal} (h : r < dimH s) : ∃ x ∈ s, ∀ t ∈ nhdsWithin x s, 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} [EMetricSpace X] [SecondCountableTopology X] (s : Set X) : ⨆ x ∈ s, 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} [EMetricSpace X] [SecondCountableTopology X] (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} [EMetricSpace X] [EMetricSpace Y] {C r : NNReal} {f : X → Y} {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} [EMetricSpace X] [EMetricSpace Y] {C r : NNReal} {f : X → Y} (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} [EMetricSpace X] [EMetricSpace Y] {C r : NNReal} {f : X → Y} (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} [EMetricSpace X] [EMetricSpace Y] [SecondCountableTopology X] {r : NNReal} {f : X → Y} (hr : 0 < r) {s : Set X} (hf : ∀ x ∈ s, ∃ (C : NNReal), ∃ t ∈ nhdsWithin x s, 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} [EMetricSpace X] [EMetricSpace Y] [SecondCountableTopology X] {r : NNReal} {f : X → Y} (hr : 0 < r) (hf : ∀ (x : X), ∃ (C : NNReal), ∃ s ∈ nhds 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} [EMetricSpace X] [EMetricSpace Y] {K : NNReal} {f : X → Y} {s : Set X} (h : LipschitzOnWith K f s) : 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} [EMetricSpace X] [EMetricSpace Y] {K : NNReal} {f : X → Y} (h : LipschitzWith K f) (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} [EMetricSpace X] [EMetricSpace Y] {K : NNReal} {f : X → Y} (h : LipschitzWith K f) : 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} [EMetricSpace X] [EMetricSpace Y] [SecondCountableTopology X] {f : X → Y} {s : Set X} (hf : ∀ x ∈ s, ∃ (C : NNReal), ∃ t ∈ nhdsWithin x s, LipschitzOnWith C f 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} [EMetricSpace X] [EMetricSpace Y] [SecondCountableTopology X] {f : X → Y} (hf : ∀ (x : X), ∃ (C : NNReal), ∃ s ∈ nhds x, LipschitzOnWith C f s) : 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} [EMetricSpace X] [EMetricSpace Y] {K : NNReal} {f : X → Y} (hf : AntilipschitzWith K f) (s : Set Y) : dimH (f ⁻¹' s) ≤ dimH s

theorem AntilipschitzWith.le_dimH_image {X : Type u_2} {Y : Type u_3} [EMetricSpace X] [EMetricSpace Y] {K : NNReal} {f : X → Y} (hf : AntilipschitzWith K 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} [EMetricSpace X] [EMetricSpace Y] {f : X → Y} (hf : Isometry f) (s : Set X) : dimH (f '' s) = dimH s

@[simp]

theorem IsometryEquiv.dimH_image {X : Type u_2} {Y : Type u_3} [EMetricSpace X] [EMetricSpace Y] (e : X ≃ᵢ Y) (s : Set X) : dimH (⇑e '' s) = dimH s

@[simp]

theorem IsometryEquiv.dimH_preimage {X : Type u_2} {Y : Type u_3} [EMetricSpace X] [EMetricSpace Y] (e : X ≃ᵢ Y) (s : Set Y) : dimH (⇑e ⁻¹' s) = dimH s

theorem IsometryEquiv.dimH_univ {X : Type u_2} {Y : Type u_3} [EMetricSpace X] [EMetricSpace Y] (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} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (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} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (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} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (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} [Fintype ι] (x : ι → ℝ) {r : ℝ} (hr : 0 < r) : dimH (Metric.ball x r) = ↑(Fintype.card ι)

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) [Fintype ι] : 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} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {x : E} {s : Set E} (h : s ∈ nhds x) : dimH s = ↑(Module.finrank ℝ E)

theorem Real.dimH_of_nonempty_interior {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} (h : (interior s).Nonempty) : dimH s = ↑(Module.finrank ℝ E)

theorem Real.dimH_univ_eq_finrank (E : Type u_4) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] : dimH Set.univ = ↑(Module.finrank ℝ E)

theorem Real.dimH_univ : dimH Set.univ = 1

theorem Real.hausdorffMeasure_of_finrank_lt {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {d : ℝ} (hd : ↑(Module.finrank ℝ E) < d) : MeasureTheory.Measure.hausdorffMeasure d = 0

theorem dense_compl_of_dimH_lt_finrank {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} (hs : dimH s < ↑(Module.finrank ℝ E)) : Dense 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} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {s t : Set E} (hf : ContDiffOn ℝ 1 f s) (hc : Convex ℝ 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 ContDiff.dimH_range_le {E : Type u_4} {F : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} (h : ContDiff ℝ 1 f) : dimH (Set.range f) ≤ ↑(Module.finrank ℝ E)

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} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : E → F} {s t : Set E} (h : ContDiffOn ℝ 1 f s) (hc : Convex ℝ s) (ht : t ⊆ s) (htF : dimH t < ↑(Module.finrank ℝ F)) : 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} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : E → F} (h : ContDiff ℝ 1 f) (hEF : Module.finrank ℝ E < Module.finrank ℝ F) : Dense (Set.range 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.