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

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 #

theorem dimH_def {X : Type u_2} [emetric_space X] [measurable_space X] [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} [emetric_space X] [measurable_space X] [borel_space X] {s : set X} {d : ℝ≥0} (h : d < dimH s) :
theorem dimH_le {X : Type u_2} [emetric_space X] [measurable_space X] [borel_space X] {s : set X} {d : ℝ≥0∞} (H : ∀ (d' : ℝ≥0), μH[d'] s = d' d) :
dimH s d
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 : ℝ≥0} (h : μH[d] s = ) :
theorem hausdorff_measure_of_dimH_lt {X : Type u_2} [emetric_space X] [measurable_space X] [borel_space X] {s : set X} {d : ℝ≥0} (h : dimH s < d) :
theorem measure_zero_of_dimH_lt {X : Type u_2} [emetric_space X] [measurable_space X] [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} [emetric_space X] [measurable_space X] [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} [emetric_space X] [measurable_space X] [borel_space X] {d : ℝ≥0} {s : set X} (h : μH[d] s 0) (h' : μH[d] s ) :
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) :
dimH (s t) = max (dimH s) (dimH t)
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 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 : ℝ≥0} {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 : ℝ≥0} {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 : ℝ≥0} {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 : ℝ≥0} {f : X → Y} (hr : 0 < r) {s : set X} (hf : ∀ (x : X), x s(∃ (C : ℝ≥0) (t : set X) (H : t 𝓝[s] x), 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 : ℝ≥0} {f : X → Y} (hr : 0 < r) (hf : ∀ (x : X), ∃ (C : ℝ≥0) (s : set X) (H : s 𝓝 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 : ℝ≥0} {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 : ℝ≥0} {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 : ℝ≥0} {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 : ℝ≥0) (t : set X) (H : t 𝓝[s] x), 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.

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 : ℝ≥0) (s : set X) (H : s 𝓝 x), lipschitz_on_with C f 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 : ℝ≥0} {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 : ℝ≥0} {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} [nondiscrete_normed_field 𝕜] [normed_group E] [normed_space 𝕜 E] [normed_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} [nondiscrete_normed_field 𝕜] [normed_group E] [normed_space 𝕜 E] [normed_group F] [normed_space 𝕜 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} [nondiscrete_normed_field 𝕜] [normed_group E] [normed_space 𝕜 E] [normed_group F] [normed_space 𝕜 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) :
theorem real.dimH_univ_pi (ι : Type u_1) [fintype ι] :
theorem real.dimH_of_mem_nhds {E : Type u_4} [normed_group E] [normed_space E] [finite_dimensional E] {x : E} {s : set E} (h : s 𝓝 x) :

Hausdorff dimension and -smooth maps #

-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] [normed_space E] [finite_dimensional E] [normed_group F] [normed_space F] {f : E → F} {s t : set E} (hf : times_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 .

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