mathlib documentation

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

In this file we define dimH s to be the Hausdorff dimension of s, then prove some basic properties of 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 #

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

Implementation notes #

Tags #

Hausdorff measure, Hausdorff dimension, dimension

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

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

Equations

Basic properties #

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

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
theorem dimH_mono {X : Type u_2} [emetric_space X] {s t : set X} (h : s t) :
theorem dimH_subsingleton {X : Type u_2} [emetric_space X] {s : set X} (h : s.subsingleton) :
dimH s = 0
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.

@[simp]
theorem dimH_empty {X : Type u_2} [emetric_space X] :
@[simp]
theorem dimH_singleton {X : Type u_2} [emetric_space X] (x : X) :
dimH {x} = 0
@[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)
@[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)
@[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
@[simp]
theorem dimH_union {X : Type u_2} [emetric_space X] (s t : set X) :
theorem dimH_countable {X : Type u_2} [emetric_space X] {s : set X} (hs : s.countable) :
dimH s = 0
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.

theorem dimH_finite {X : Type u_2} [emetric_space X] {s : set X} (hs : s.finite) :
dimH s = 0
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.

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

Alias of dimH_coe_finset.

Hausdorff dimension as the supremum of local Hausdorff dimensions #

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.

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.

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 #

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.

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.

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

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

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

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

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.

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

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

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} [emetric_space X] [emetric_space Y] {K : nnreal} {f : X Y} (hf : antilipschitz_with K f) (s : set Y) :
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 #

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
@[simp]
theorem isometric.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
@[simp]
theorem isometric.dimH_preimage {X : Type u_2} {Y : Type u_3} [emetric_space X] [emetric_space Y] (e : X ≃ᵢ Y) (s : set Y) :
theorem isometric.dimH_univ {X : Type u_2} {Y : Type u_3} [emetric_space X] [emetric_space Y] (e : X ≃ᵢ Y) :
@[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
@[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) :

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

Hausdorff dimension and -smooth maps #

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

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

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

A particular case of Sard's Theorem. Let f : E → F be a map between finite dimensional real vector spaces. Suppose that f is 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.

A particular case of Sard's Theorem. If f is a 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.