Hausdorff dimension #

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

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

source

@[irreducible]

noncomputable def dimH {X : Type u_2} [emetric_space X] (s : set X) :

ennreal

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

Equations

dimH s = let _inst : measurable_space X := borel X in ⨆ (d : nnreal) (hd : ⇑(measure_theory.measure.hausdorff_measure ↑d) s = ⊤), ↑d

Basic properties #

source

theorem dimH_def {X : Type u_2} [emetric_space X] [measurable_space X] [borel_space X] (s : set X) :

dimH s = ⨆ (d : nnreal) (hd : ⇑(measure_theory.measure.hausdorff_measure ↑d) s = ⊤), ↑d

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

source

theorem hausdorff_measure_of_lt_dimH {X : Type u_2} [emetric_space X] [measurable_space X] [borel_space X] {s : set X} {d : nnreal} (h : ↑d < dimH s) :

⇑(measure_theory.measure.hausdorff_measure ↑d) s = ⊤

source

theorem dimH_le {X : Type u_2} [emetric_space X] [measurable_space X] [borel_space X] {s : set X} {d : ennreal} (H : ∀ (d' : nnreal), ⇑(measure_theory.measure.hausdorff_measure ↑d') s = ⊤ → ↑d' ≤ d) :

dimH s ≤ d

source

theorem dimH_le_of_hausdorff_measure_ne_top {X : Type u_2} [emetric_space X] [measurable_space X] [borel_space X] {s : set X} {d : nnreal} (h : ⇑(measure_theory.measure.hausdorff_measure ↑d) s ≠ ⊤) :

dimH s ≤ ↑d

source

theorem le_dimH_of_hausdorff_measure_eq_top {X : Type u_2} [emetric_space X] [measurable_space X] [borel_space X] {s : set X} {d : nnreal} (h : ⇑(measure_theory.measure.hausdorff_measure ↑d) s = ⊤) :

↑d ≤ dimH s

source

theorem hausdorff_measure_of_dimH_lt {X : Type u_2} [emetric_space X] [measurable_space X] [borel_space X] {s : set X} {d : nnreal} (h : dimH s < ↑d) :

⇑(measure_theory.measure.hausdorff_measure ↑d) s = 0

source

theorem measure_zero_of_dimH_lt {X : Type u_2} [emetric_space X] [measurable_space X] [borel_space X] {μ : measure_theory.measure X} {d : nnreal} (h : μ.absolutely_continuous (measure_theory.measure.hausdorff_measure ↑d)) {s : set X} (hd : dimH s < ↑d) :

⇑μ s = 0

source

theorem le_dimH_of_hausdorff_measure_ne_zero {X : Type u_2} [emetric_space X] [measurable_space X] [borel_space X] {s : set X} {d : nnreal} (h : ⇑(measure_theory.measure.hausdorff_measure ↑d) s ≠ 0) :

↑d ≤ dimH s

source

theorem dimH_of_hausdorff_measure_ne_zero_ne_top {X : Type u_2} [emetric_space X] [measurable_space X] [borel_space X] {d : nnreal} {s : set X} (h : ⇑(measure_theory.measure.hausdorff_measure ↑d) s ≠ 0) (h' : ⇑(measure_theory.measure.hausdorff_measure ↑d) s ≠ ⊤) :

dimH s = ↑d

source

theorem dimH_mono {X : Type u_2} [emetric_space X] {s t : set X} (h : s ⊆ t) :

dimH s ≤ dimH t

source

theorem dimH_subsingleton {X : Type u_2} [emetric_space X] {s : set X} (h : s.subsingleton) :

dimH s = 0

source

theorem set.subsingleton.dimH_zero {X : Type u_2} [emetric_space X] {s : set X} (h : s.subsingleton) :

dimH s = 0

Alias of dimH_subsingleton.

source

@[simp]

theorem dimH_empty {X : Type u_2} [emetric_space X] :

dimH ∅ = 0

source

@[simp]

theorem dimH_singleton {X : Type u_2} [emetric_space X] (x : X) :

dimH {x} = 0

source

@[simp]

theorem dimH_Union {ι : Type u_1} {X : Type u_2} [emetric_space X] [encodable ι] (s : ι → set X) :

dimH (⋃ (i : ι), s i) = ⨆ (i : ι), dimH (s i)

source

@[simp]

theorem dimH_bUnion {ι : Type u_1} {X : Type u_2} [emetric_space X] {s : set ι} (hs : s.countable) (t : ι → set X) :

dimH (⋃ (i : ι) (H : i ∈ s), t i) = ⨆ (i : ι) (H : i ∈ s), dimH (t i)

source

@[simp]

theorem dimH_sUnion {X : Type u_2} [emetric_space X] {S : set (set X)} (hS : S.countable) :

dimH (⋃₀ S) = ⨆ (s : set X) (H : s ∈ S), dimH s

source

@[simp]

theorem dimH_union {X : Type u_2} [emetric_space X] (s t : set X) :

dimH (s ∪ t) = linear_order.max (dimH s) (dimH t)

source

theorem dimH_countable {X : Type u_2} [emetric_space X] {s : set X} (hs : s.countable) :

dimH s = 0

source

theorem set.countable.dimH_zero {X : Type u_2} [emetric_space X] {s : set X} (hs : s.countable) :

dimH s = 0

Alias of dimH_countable.

source

theorem dimH_finite {X : Type u_2} [emetric_space X] {s : set X} (hs : s.finite) :

dimH s = 0

source

theorem set.finite.dimH_zero {X : Type u_2} [emetric_space X] {s : set X} (hs : s.finite) :

dimH s = 0

Alias of dimH_finite.

source

@[simp]

theorem dimH_coe_finset {X : Type u_2} [emetric_space X] (s : finset X) :

dimH ↑s = 0

source

theorem finset.dimH_zero {X : Type u_2} [emetric_space X] (s : finset X) :

dimH ↑s = 0

Alias of dimH_coe_finset.

Hausdorff dimension as the supremum of local Hausdorff dimensions #

source

theorem exists_mem_nhds_within_lt_dimH_of_lt_dimH {X : Type u_2} [emetric_space X] [topological_space.second_countable_topology X] {s : set X} {r : ennreal} (h : r < dimH s) :

∃ (x : X) (H : x ∈ s), ∀ (t : set X), t ∈ nhds_within 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.

source

theorem bsupr_limsup_dimH {X : Type u_2} [emetric_space X] [topological_space.second_countable_topology X] (s : set X) :

(⨆ (x : X) (H : x ∈ s), filter.limsup dimH (nhds_within x s).small_sets) = 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).small_sets.

source

theorem supr_limsup_dimH {X : Type u_2} [emetric_space X] [topological_space.second_countable_topology X] (s : set X) :

(⨆ (x : X), filter.limsup dimH (nhds_within x s).small_sets) = 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).small_sets.

Hausdorff dimension and Hölder continuity #

source

theorem holder_on_with.dimH_image_le {X : Type u_2} {Y : Type u_3} [emetric_space X] [emetric_space Y] {C r : nnreal} {f : X → Y} {s : set X} (h : holder_on_with 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.

source

theorem holder_with.dimH_image_le {X : Type u_2} {Y : Type u_3} [emetric_space X] [emetric_space Y] {C r : nnreal} {f : X → Y} (h : holder_with 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.

source

theorem holder_with.dimH_range_le {X : Type u_2} {Y : Type u_3} [emetric_space X] [emetric_space Y] {C r : nnreal} {f : X → Y} (h : holder_with 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.

source

theorem dimH_image_le_of_locally_holder_on {X : Type u_2} {Y : Type u_3} [emetric_space X] [emetric_space Y] [topological_space.second_countable_topology X] {r : nnreal} {f : X → Y} (hr : 0 < r) {s : set X} (hf : ∀ (x : X), x ∈ s → (∃ (C : nnreal) (t : set X) (H : t ∈ nhds_within x s), holder_on_with 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.

source

theorem dimH_range_le_of_locally_holder_on {X : Type u_2} {Y : Type u_3} [emetric_space X] [emetric_space Y] [topological_space.second_countable_topology X] {r : nnreal} {f : X → Y} (hr : 0 < r) (hf : ∀ (x : X), ∃ (C : nnreal) (s : set X) (H : s ∈ nhds x), holder_on_with 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 #

source

theorem lipschitz_on_with.dimH_image_le {X : Type u_2} {Y : Type u_3} [emetric_space X] [emetric_space Y] {K : nnreal} {f : X → Y} {s : set X} (h : lipschitz_on_with K f s) :

dimH (f '' s) ≤ dimH s

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

source

theorem lipschitz_with.dimH_image_le {X : Type u_2} {Y : Type u_3} [emetric_space X] [emetric_space Y] {K : nnreal} {f : X → Y} (h : lipschitz_with K f) (s : set X) :

dimH (f '' s) ≤ dimH s

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

source

theorem lipschitz_with.dimH_range_le {X : Type u_2} {Y : Type u_3} [emetric_space X] [emetric_space Y] {K : nnreal} {f : X → Y} (h : lipschitz_with 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.

source

theorem dimH_image_le_of_locally_lipschitz_on {X : Type u_2} {Y : Type u_3} [emetric_space X] [emetric_space Y] [topological_space.second_countable_topology X] {f : X → Y} {s : set X} (hf : ∀ (x : X), x ∈ s → (∃ (C : nnreal) (t : set X) (H : t ∈ nhds_within x s), lipschitz_on_with 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.

source

theorem dimH_range_le_of_locally_lipschitz_on {X : Type u_2} {Y : Type u_3} [emetric_space X] [emetric_space Y] [topological_space.second_countable_topology X] {f : X → Y} (hf : ∀ (x : X), ∃ (C : nnreal) (s : set X) (H : s ∈ nhds x), lipschitz_on_with 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.

source

theorem antilipschitz_with.dimH_preimage_le {X : Type u_2} {Y : Type u_3} [emetric_space X] [emetric_space Y] {K : nnreal} {f : X → Y} (hf : antilipschitz_with K f) (s : set Y) :

dimH (f ⁻¹' s) ≤ dimH s

source

theorem antilipschitz_with.le_dimH_image {X : Type u_2} {Y : Type u_3} [emetric_space X] [emetric_space Y] {K : nnreal} {f : X → Y} (hf : antilipschitz_with K f) (s : set X) :

dimH s ≤ dimH (f '' s)

Isometries preserve Hausdorff dimension #

source

theorem isometry.dimH_image {X : Type u_2} {Y : Type u_3} [emetric_space X] [emetric_space Y] {f : X → Y} (hf : isometry f) (s : set X) :

dimH (f '' s) = dimH s

source

@[simp]

theorem isometry_equiv.dimH_image {X : Type u_2} {Y : Type u_3} [emetric_space X] [emetric_space Y] (e : X ≃ᵢ Y) (s : set X) :

dimH (⇑e '' s) = dimH s

source

@[simp]

theorem isometry_equiv.dimH_preimage {X : Type u_2} {Y : Type u_3} [emetric_space X] [emetric_space Y] (e : X ≃ᵢ Y) (s : set Y) :

dimH (⇑e ⁻¹' s) = dimH s

source

theorem isometry_equiv.dimH_univ {X : Type u_2} {Y : Type u_3} [emetric_space X] [emetric_space Y] (e : X ≃ᵢ Y) :

dimH set.univ = dimH set.univ

source

@[simp]

theorem continuous_linear_equiv.dimH_image {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [nontrivially_normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [normed_add_comm_group F] [normed_space 𝕜 F] (e : E ≃L[𝕜] F) (s : set E) :

dimH (⇑e '' s) = dimH s

source

@[simp]

theorem continuous_linear_equiv.dimH_preimage {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [nontrivially_normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [normed_add_comm_group F] [normed_space 𝕜 F] (e : E ≃L[𝕜] F) (s : set F) :

dimH (⇑e ⁻¹' s) = dimH s

source

theorem continuous_linear_equiv.dimH_univ {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [nontrivially_normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] [normed_add_comm_group F] [normed_space 𝕜 F] (e : E ≃L[𝕜] F) :

dimH set.univ = dimH set.univ

Hausdorff dimension in a real vector space #

source

theorem real.dimH_ball_pi {ι : Type u_1} [fintype ι] (x : ι → ℝ) {r : ℝ} (hr : 0 < r) :

dimH (metric.ball x r) = ↑(fintype.card ι)

source

theorem real.dimH_ball_pi_fin {n : ℕ} (x : fin n → ℝ) {r : ℝ} (hr : 0 < r) :

dimH (metric.ball x r) = ↑n

source

theorem real.dimH_univ_pi (ι : Type u_1) [fintype ι] :

dimH set.univ = ↑(fintype.card ι)

source

theorem real.dimH_univ_pi_fin (n : ℕ) :

dimH set.univ = ↑n

source

theorem real.dimH_of_mem_nhds {E : Type u_4} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {x : E} {s : set E} (h : s ∈ nhds x) :

dimH s = ↑(fdim E)

source

theorem real.dimH_of_nonempty_interior {E : Type u_4} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {s : set E} (h : (interior s).nonempty) :

dimH s = ↑(fdim E)

source

theorem real.dimH_univ_eq_finrank (E : Type u_4) [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] :

dimH set.univ = ↑(fdim E)

source

theorem real.dimH_univ :

dimH set.univ = 1

source

theorem dense_compl_of_dimH_lt_finrank {E : Type u_4} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] {s : set E} (hs : dimH s < ↑(fdim 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.

source

theorem cont_diff_on.dimH_image_le {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] [normed_add_comm_group F] [normed_space ℝ F] {f : E → F} {s t : set E} (hf : cont_diff_on ℝ 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?

source

theorem cont_diff.dimH_range_le {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] [normed_add_comm_group F] [normed_space ℝ F] {f : E → F} (h : cont_diff ℝ 1 f) :

dimH (set.range f) ≤ ↑(fdim 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 ℝ.

source

theorem cont_diff_on.dense_compl_image_of_dimH_lt_finrank {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] [normed_add_comm_group F] [normed_space ℝ F] [finite_dimensional ℝ F] {f : E → F} {s t : set E} (h : cont_diff_on ℝ 1 f s) (hc : convex ℝ s) (ht : t ⊆ s) (htF : dimH t < ↑(fdim 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.

source

theorem cont_diff.dense_compl_range_of_finrank_lt_finrank {E : Type u_4} {F : Type u_5} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] [normed_add_comm_group F] [normed_space ℝ F] [finite_dimensional ℝ F] {f : E → F} (h : cont_diff ℝ 1 f) (hEF : fdim E < fdim 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.

Hausdorff dimension #

Main definitions #

Main results #

Basic properties of Hausdorff dimension #

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

Hausdorff measure in ℝⁿ #

Notations #

Implementation notes #

Tags #

Basic properties #

Hausdorff dimension as the supremum of local Hausdorff dimensions #

Hausdorff dimension and Hölder continuity #

Hausdorff dimension and Lipschitz continuity #

Isometries preserve Hausdorff dimension #

Hausdorff dimension in a real vector space #

Hausdorff dimension and C¹-smooth maps #

Hausdorff measure in `ℝⁿ` #

Hausdorff dimension and `C¹`-smooth maps #