Exact source: Mathlib/Topology/MetricSpace/HausdorffDimension.lean
Pinned GitHub source · Raw UTF-8 source
Back to Isometric unit spheres force equal finite dimensions
1/-2Copyright (c) 2021 Yury Kudryashov. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Yury Kudryashov5-/6module78public import Mathlib.Analysis.Calculus.ContDiff.RCLike9public import Mathlib.MeasureTheory.Measure.Hausdorff10import Mathlib.Analysis.Convex.Intrinsic1112/-!13# Hausdorff dimension1415The Hausdorff dimension of a set `X` in an (extended) metric space is the unique number16`dimH s : ℝ≥0∞` such that for any `d : ℝ≥0` we have1718- `μH[d] s = 0` if `dimH s < d`, and19- `μH[d] s = ∞` if `d < dimH s`.2021In this file we define `dimH s` to be the Hausdorff dimension of `s`, then prove some basic22properties of Hausdorff dimension.2324## Main definitions2526* `MeasureTheory.dimH`: the Hausdorff dimension of a set. For the Hausdorff dimension of the whole27 space we use `MeasureTheory.dimH (Set.univ : Set X)`.2829## Main results3031### Basic properties of Hausdorff dimension3233* `hausdorffMeasure_of_lt_dimH`, `dimH_le_of_hausdorffMeasure_ne_top`,34 `le_dimH_of_hausdorffMeasure_eq_top`, `hausdorffMeasure_of_dimH_lt`, `measure_zero_of_dimH_lt`,35 `le_dimH_of_hausdorffMeasure_ne_zero`, `dimH_of_hausdorffMeasure_ne_zero_ne_top`: various forms36 of the characteristic property of the Hausdorff dimension;37* `dimH_union`: the Hausdorff dimension of the union of two sets is the maximum of their Hausdorff38 dimensions.39* `dimH_iUnion`, `dimH_bUnion`, `dimH_sUnion`: the Hausdorff dimension of a countable union of sets40 is the supremum of their Hausdorff dimensions;41* `dimH_empty`, `dimH_singleton`, `Set.Subsingleton.dimH_zero`, `Set.Countable.dimH_zero` : `dimH s42 = 0` whenever `s` is countable;4344### (Pre)images under (anti)lipschitz and Hölder continuous maps4546* `HolderWith.dimH_image_le` etc: if `f : X → Y` is Hölder continuous with exponent `r > 0`, then47 for any `s`, `dimH (f '' s) ≤ dimH s / r`. We prove versions of this statement for `HolderWith`,48 `HolderOnWith`, and locally Hölder maps, as well as for `Set.image` and `Set.range`.49* `LipschitzWith.dimH_image_le` etc: Lipschitz continuous maps do not increase the Hausdorff50 dimension of sets.51* for a map that is known to be both Lipschitz and antilipschitz (e.g., for an `Isometry` or52 a `ContinuousLinearEquiv`) we also prove `dimH (f '' s) = dimH s`.5354### Hausdorff measure in `ℝⁿ`5556* `Real.dimH_of_nonempty_interior`: if `s` is a set in a finite-dimensional real vector space `E`57 with nonempty interior, then the Hausdorff dimension of `s` is equal to the dimension of `E`.58* `dense_compl_of_dimH_lt_finrank`: if `s` is a set in a finite-dimensional real vector space `E`59 with Hausdorff dimension strictly less than the dimension of `E`, the `s` has a dense complement.60* `ContDiff.dense_compl_range_of_finrank_lt_finrank`: the complement to the range of a `C¹`61 smooth map is dense provided that the dimension of the domain is strictly less than the dimension62 of the codomain.6364## Notation6566We use the following notation localized in `MeasureTheory`. It is defined in67`MeasureTheory.Measure.Hausdorff`.6869- `μH[d]` : `MeasureTheory.Measure.hausdorffMeasure d`7071## Implementation notes7273* The definition of `dimH` explicitly uses `borel X` as a measurable space structure. This way we74 can formulate lemmas about Hausdorff dimension without assuming that the environment has a75 `[MeasurableSpace X]` instance that is equal but possibly not defeq to `borel X`.7677 Lemma `dimH_def` unfolds this definition using whatever `[MeasurableSpace X]` instance we have in78 the environment (as long as it is equal to `borel X`).7980* The definition `dimH` is irreducible; use API lemmas or `dimH_def` instead.8182## Tags8384Hausdorff measure, Hausdorff dimension, dimension85-/8687@[expose] public section888990open scoped MeasureTheory ENNReal NNReal Topology9192open MeasureTheory MeasureTheory.Measure Set TopologicalSpace Module Filter9394variable {ι X Y : Type*} [EMetricSpace X] [EMetricSpace Y]9596/-- Hausdorff dimension of a set in an (e)metric space. -/97@[irreducible] noncomputable def dimH (s : Set X) : ℝ≥0∞ := by98 borelize X; exact ⨆ (d : ℝ≥0) (_ : @hausdorffMeasure X _ _ ⟨rfl⟩ d s = ∞), d99100/-!101### Basic properties102-/103104105section Measurable106107variable [MeasurableSpace X] [BorelSpace X]108109/-- Unfold the definition of `dimH` using `[MeasurableSpace X] [BorelSpace X]` from the110environment. -/111theorem dimH_def (s : Set X) : dimH s = ⨆ (d : ℝ≥0) (_ : μH[d] s = ∞), (d : ℝ≥0∞) := by112 borelize X; rw [dimH]113114theorem hausdorffMeasure_of_lt_dimH {s : Set X} {d : ℝ≥0} (h : ↑d < dimH s) : μH[d] s = ∞ := by115 simp only [dimH_def, lt_iSup_iff] at h116 rcases h with ⟨d', hsd', hdd'⟩117 rw [ENNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at hdd'118 exact top_unique (hsd' ▸ hausdorffMeasure_mono hdd'.le _)119120theorem dimH_le {s : Set X} {d : ℝ≥0∞} (H : ∀ d' : ℝ≥0, μH[d'] s = ∞ → ↑d' ≤ d) : dimH s ≤ d :=121 (dimH_def s).trans_le <| iSup₂_le H122123theorem dimH_le_of_hausdorffMeasure_ne_top {s : Set X} {d : ℝ≥0} (h : μH[d] s ≠ ∞) : dimH s ≤ d :=124 le_of_not_gt <| mt hausdorffMeasure_of_lt_dimH h125126theorem le_dimH_of_hausdorffMeasure_eq_top {s : Set X} {d : ℝ≥0} (h : μH[d] s = ∞) :127 ↑d ≤ dimH s := by128 rw [dimH_def]; exact le_iSup₂ (α := ℝ≥0∞) d h129130theorem hausdorffMeasure_of_dimH_lt {s : Set X} {d : ℝ≥0} (h : dimH s < d) : μH[d] s = 0 := by131 rw [dimH_def] at h132 rcases ENNReal.lt_iff_exists_nnreal_btwn.1 h with ⟨d', hsd', hd'd⟩133 rw [ENNReal.coe_lt_coe, ← NNReal.coe_lt_coe] at hd'd134 exact (hausdorffMeasure_zero_or_top hd'd s).resolve_right fun h₂ => hsd'.not_ge <|135 le_iSup₂ (α := ℝ≥0∞) d' h₂136137theorem measure_zero_of_dimH_lt {μ : Measure X} {d : ℝ≥0} (h : μ ≪ μH[d]) {s : Set X}138 (hd : dimH s < d) : μ s = 0 :=139 h <| hausdorffMeasure_of_dimH_lt hd140141theorem le_dimH_of_hausdorffMeasure_ne_zero {s : Set X} {d : ℝ≥0} (h : μH[d] s ≠ 0) : ↑d ≤ dimH s :=142 le_of_not_gt <| mt hausdorffMeasure_of_dimH_lt h143144theorem dimH_of_hausdorffMeasure_ne_zero_ne_top {d : ℝ≥0} {s : Set X} (h : μH[d] s ≠ 0)145 (h' : μH[d] s ≠ ∞) : dimH s = d :=146 le_antisymm (dimH_le_of_hausdorffMeasure_ne_top h') (le_dimH_of_hausdorffMeasure_ne_zero h)147148/-- The Hausdorff dimension of a set `s` is the infimum of all `d : ℝ≥0` such that the149`d`-dimensional Hausdorff measure of `s` is zero. This infimum is taken in `ℝ≥0∞`.150This gives an equivalent definition of the Hausdorff dimension. -/151theorem dimH_eq_iInf (s : Set X) : dimH s = ⨅ (d : ℝ≥0) (_ : μH[d] s = 0), (d : ℝ≥0∞) := by152 apply le_antisymm153 · rw [dimH_def]154 simp only [le_iInf_iff, iSup_le_iff, ENNReal.coe_le_coe]155 intro i hi j hj156 by_contra! hij157 simpa [hi, hj] using hausdorffMeasure_mono hij.le s158 · by_contra! h159 rcases ENNReal.lt_iff_exists_nnreal_btwn.1 h with ⟨d', hdim_lt, hlt⟩160 have h0 : μH[d'] s = 0 := hausdorffMeasure_of_dimH_lt hdim_lt161 exact hlt.not_ge (iInf₂_le d' h0)162163end Measurable164165@[gcongr, mono]166theorem dimH_mono {s t : Set X} (h : s ⊆ t) : dimH s ≤ dimH t := by167 borelize X168 exact dimH_le fun d hd => le_dimH_of_hausdorffMeasure_eq_top <| top_unique <| hd ▸ measure_mono h169170theorem dimH_subsingleton {s : Set X} (h : s.Subsingleton) : dimH s = 0 := by171 borelize X172 rw [← nonpos_iff_eq_zero]173 apply dimH_le_of_hausdorffMeasure_ne_top174 exact ((hausdorffMeasure_le_one_of_subsingleton h le_rfl).trans_lt ENNReal.one_lt_top).ne175176alias Set.Subsingleton.dimH_zero := dimH_subsingleton177178@[simp]179theorem dimH_empty : dimH (∅ : Set X) = 0 :=180 subsingleton_empty.dimH_zero181182@[simp]183theorem dimH_singleton (x : X) : dimH ({x} : Set X) = 0 :=184 subsingleton_singleton.dimH_zero185186@[simp]187theorem dimH_iUnion {ι : Sort*} [Countable ι] (s : ι → Set X) :188 dimH (⋃ i, s i) = ⨆ i, dimH (s i) := by189 borelize X190 refine le_antisymm (dimH_le fun d hd => ?_) (iSup_le fun i => dimH_mono <| subset_iUnion _ _)191 contrapose! hd192 have : ∀ i, μH[d] (s i) = 0 := fun i =>193 hausdorffMeasure_of_dimH_lt ((le_iSup (fun i => dimH (s i)) i).trans_lt hd)194 rw [measure_iUnion_null this]195 exact ENNReal.zero_ne_top196197@[simp]198theorem dimH_bUnion {s : Set ι} (hs : s.Countable) (t : ι → Set X) :199 dimH (⋃ i ∈ s, t i) = ⨆ i ∈ s, dimH (t i) := by200 haveI := hs.toEncodable201 rw [biUnion_eq_iUnion, dimH_iUnion, ← iSup_subtype'']202203@[simp]204theorem dimH_sUnion {S : Set (Set X)} (hS : S.Countable) : dimH (⋃₀ S) = ⨆ s ∈ S, dimH s := by205 rw [sUnion_eq_biUnion, dimH_bUnion hS]206207@[simp]208theorem dimH_union (s t : Set X) : dimH (s ∪ t) = max (dimH s) (dimH t) := by209 rw [union_eq_iUnion, dimH_iUnion, iSup_bool_eq, cond, cond]210211theorem dimH_countable {s : Set X} (hs : s.Countable) : dimH s = 0 :=212 biUnion_of_singleton s ▸ by simp only [dimH_bUnion hs, dimH_singleton, ENNReal.iSup_zero]213214alias Set.Countable.dimH_zero := dimH_countable215216theorem dimH_finite {s : Set X} (hs : s.Finite) : dimH s = 0 :=217 hs.countable.dimH_zero218219alias Set.Finite.dimH_zero := dimH_finite220221@[simp]222theorem dimH_coe_finset (s : Finset X) : dimH (s : Set X) = 0 :=223 s.finite_toSet.dimH_zero224225alias Finset.dimH_zero := dimH_coe_finset226227/-!228### Hausdorff dimension as the supremum of local Hausdorff dimensions229-/230231232section233234variable [SecondCountableTopology X]235236/-- If `r` is less than the Hausdorff dimension of a set `s` in an (extended) metric space with237second countable topology, then there exists a point `x ∈ s` such that every neighborhood238`t` of `x` within `s` has Hausdorff dimension greater than `r`. -/239theorem exists_mem_nhdsWithin_lt_dimH_of_lt_dimH {s : Set X} {r : ℝ≥0∞} (h : r < dimH s) :240 ∃ x ∈ s, ∀ t ∈ 𝓝[s] x, r < dimH t := by241 contrapose! h; choose! t htx htr using h242 rcases countable_cover_nhdsWithin htx with ⟨S, hSs, hSc, hSU⟩243 calc244 dimH s ≤ dimH (⋃ x ∈ S, t x) := dimH_mono hSU245 _ = ⨆ x ∈ S, dimH (t x) := dimH_bUnion hSc _246 _ ≤ r := iSup₂_le fun x hx => htr x <| hSs hx247248/-- In an (extended) metric space with second countable topology, the Hausdorff dimension249of a set `s` is the supremum over `x ∈ s` of the limit superiors of `dimH t` along250`(𝓝[s] x).smallSets`. -/251theorem bsupr_limsup_dimH (s : Set X) : ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets = dimH s := by252 refine le_antisymm (iSup₂_le fun x _ => ?_) ?_253 · refine limsup_le_of_le isCobounded_le_of_bot ?_254 exact eventually_smallSets.2 ⟨s, self_mem_nhdsWithin, fun t => dimH_mono⟩255 · refine le_of_forall_lt_imp_le_of_dense fun r hr => ?_256 rcases exists_mem_nhdsWithin_lt_dimH_of_lt_dimH hr with ⟨x, hxs, hxr⟩257 refine le_iSup₂_of_le x hxs ?_; rw [limsup_eq]; refine le_sInf fun b hb => ?_258 rcases eventually_smallSets.1 hb with ⟨t, htx, ht⟩259 exact (hxr t htx).le.trans (ht t Subset.rfl)260261/-- In an (extended) metric space with second countable topology, the Hausdorff dimension262of a set `s` is the supremum over all `x` of the limit superiors of `dimH t` along263`(𝓝[s] x).smallSets`. -/264theorem iSup_limsup_dimH (s : Set X) : ⨆ x, limsup dimH (𝓝[s] x).smallSets = dimH s := by265 refine le_antisymm (iSup_le fun x => ?_) ?_266 · refine limsup_le_of_le isCobounded_le_of_bot ?_267 exact eventually_smallSets.2 ⟨s, self_mem_nhdsWithin, fun t => dimH_mono⟩268 · rw [← bsupr_limsup_dimH]; exact iSup₂_le_iSup _ _269270end271272/-!273### Hausdorff dimension and Hölder continuity274-/275276277variable {C K r : ℝ≥0} {f : X → Y} {s : Set X}278279/-- If `f` is a Hölder continuous map with exponent `r > 0`, then `dimH (f '' s) ≤ dimH s / r`. -/280theorem HolderOnWith.dimH_image_le (h : HolderOnWith C r f s) (hr : 0 < r) :281 dimH (f '' s) ≤ dimH s / r := by282 borelize X Y283 refine dimH_le fun d hd => ?_284 have := h.hausdorffMeasure_image_le hr d.coe_nonneg285 rw [hd, ← ENNReal.coe_rpow_of_nonneg _ d.coe_nonneg, top_le_iff] at this286 have Hrd : μH[(r * d : ℝ≥0)] s = ⊤ := by287 contrapose this288 finiteness289 rw [ENNReal.le_div_iff_mul_le, mul_comm, ← ENNReal.coe_mul]290 exacts [le_dimH_of_hausdorffMeasure_eq_top Hrd, Or.inl (mt ENNReal.coe_eq_zero.1 hr.ne'),291 Or.inl ENNReal.coe_ne_top]292293namespace HolderWith294295/-- If `f : X → Y` is Hölder continuous with a positive exponent `r`, then the Hausdorff dimension296of the image of a set `s` is at most `dimH s / r`. -/297theorem dimH_image_le (h : HolderWith C r f) (hr : 0 < r) (s : Set X) :298 dimH (f '' s) ≤ dimH s / r :=299 (h.holderOnWith s).dimH_image_le hr300301/-- If `f` is a Hölder continuous map with exponent `r > 0`, then the Hausdorff dimension of its302range is at most the Hausdorff dimension of its domain divided by `r`. -/303theorem dimH_range_le (h : HolderWith C r f) (hr : 0 < r) :304 dimH (range f) ≤ dimH (univ : Set X) / r :=305 @image_univ _ _ f ▸ h.dimH_image_le hr univ306307end HolderWith308309/-- If `s` is a set in a space `X` with second countable topology and `f : X → Y` is Hölder310continuous in a neighborhood within `s` of every point `x ∈ s` with the same positive exponent `r`311but possibly different coefficients, then the Hausdorff dimension of the image `f '' s` is at most312the Hausdorff dimension of `s` divided by `r`. -/313theorem dimH_image_le_of_locally_holder_on [SecondCountableTopology X] {r : ℝ≥0} {f : X → Y}314 (hr : 0 < r) {s : Set X} (hf : ∀ x ∈ s, ∃ C : ℝ≥0, ∃ t ∈ 𝓝[s] x, HolderOnWith C r f t) :315 dimH (f '' s) ≤ dimH s / r := by316 choose! C t htn hC using hf317 rcases countable_cover_nhdsWithin htn with ⟨u, hus, huc, huU⟩318 replace huU := inter_eq_self_of_subset_left huU; rw [inter_iUnion₂] at huU319 rw [← huU, image_iUnion₂, dimH_bUnion huc, dimH_bUnion huc]; simp only [ENNReal.iSup_div]320 exact iSup₂_mono fun x hx => ((hC x (hus hx)).mono inter_subset_right).dimH_image_le hr321322/-- If `f : X → Y` is Hölder continuous in a neighborhood of every point `x : X` with the same323positive exponent `r` but possibly different coefficients, then the Hausdorff dimension of the range324of `f` is at most the Hausdorff dimension of `X` divided by `r`. -/325theorem dimH_range_le_of_locally_holder_on [SecondCountableTopology X] {r : ℝ≥0} {f : X → Y}326 (hr : 0 < r) (hf : ∀ x : X, ∃ C : ℝ≥0, ∃ s ∈ 𝓝 x, HolderOnWith C r f s) :327 dimH (range f) ≤ dimH (univ : Set X) / r := by328 rw [← image_univ]329 refine dimH_image_le_of_locally_holder_on hr fun x _ => ?_330 simpa only [exists_prop, nhdsWithin_univ] using hf x331332/-!333### Hausdorff dimension and Lipschitz continuity334-/335336337/-- If `f : X → Y` is Lipschitz continuous on `s`, then `dimH (f '' s) ≤ dimH s`. -/338theorem LipschitzOnWith.dimH_image_le (h : LipschitzOnWith K f s) : dimH (f '' s) ≤ dimH s := by339 simpa using h.holderOnWith.dimH_image_le zero_lt_one340341namespace LipschitzWith342343/-- If `f` is a Lipschitz continuous map, then `dimH (f '' s) ≤ dimH s`. -/344theorem dimH_image_le (h : LipschitzWith K f) (s : Set X) : dimH (f '' s) ≤ dimH s :=345 h.lipschitzOnWith.dimH_image_le346347/-- If `f` is a Lipschitz continuous map, then the Hausdorff dimension of its range is at most the348Hausdorff dimension of its domain. -/349theorem dimH_range_le (h : LipschitzWith K f) : dimH (range f) ≤ dimH (univ : Set X) :=350 @image_univ _ _ f ▸ h.dimH_image_le univ351352end LipschitzWith353354/-- If `s` is a set in an extended metric space `X` with second countable topology and `f : X → Y`355is Lipschitz in a neighborhood within `s` of every point `x ∈ s`, then the Hausdorff dimension of356the image `f '' s` is at most the Hausdorff dimension of `s`. -/357theorem dimH_image_le_of_locally_lipschitzOn [SecondCountableTopology X] {f : X → Y} {s : Set X}358 (hf : ∀ x ∈ s, ∃ C : ℝ≥0, ∃ t ∈ 𝓝[s] x, LipschitzOnWith C f t) : dimH (f '' s) ≤ dimH s := by359 have : ∀ x ∈ s, ∃ C : ℝ≥0, ∃ t ∈ 𝓝[s] x, HolderOnWith C 1 f t := by360 simpa only [holderOnWith_one] using hf361 simpa only [ENNReal.coe_one, div_one] using dimH_image_le_of_locally_holder_on zero_lt_one this362363/-- If `f : X → Y` is Lipschitz in a neighborhood of each point `x : X`, then the Hausdorff364dimension of `range f` is at most the Hausdorff dimension of `X`. -/365theorem dimH_range_le_of_locally_lipschitzOn [SecondCountableTopology X] {f : X → Y}366 (hf : ∀ x : X, ∃ C : ℝ≥0, ∃ s ∈ 𝓝 x, LipschitzOnWith C f s) :367 dimH (range f) ≤ dimH (univ : Set X) := by368 rw [← image_univ]369 refine dimH_image_le_of_locally_lipschitzOn fun x _ => ?_370 simpa only [exists_prop, nhdsWithin_univ] using hf x371372namespace AntilipschitzWith373374theorem dimH_preimage_le (hf : AntilipschitzWith K f) (s : Set Y) : dimH (f ⁻¹' s) ≤ dimH s := by375 borelize X Y376 refine dimH_le fun d hd => le_dimH_of_hausdorffMeasure_eq_top ?_377 have := hf.hausdorffMeasure_preimage_le d.coe_nonneg s378 rw [hd, top_le_iff] at this379 contrapose! this380 exact ENNReal.mul_ne_top (by simp) this381382theorem le_dimH_image (hf : AntilipschitzWith K f) (s : Set X) : dimH s ≤ dimH (f '' s) :=383 calc384 dimH s ≤ dimH (f ⁻¹' f '' s) := dimH_mono (subset_preimage_image _ _)385 _ ≤ dimH (f '' s) := hf.dimH_preimage_le _386387end AntilipschitzWith388389/-!390### Isometries preserve Hausdorff dimension391-/392393394theorem Isometry.dimH_image (hf : Isometry f) (s : Set X) : dimH (f '' s) = dimH s :=395 le_antisymm (hf.lipschitz.dimH_image_le _) (hf.antilipschitz.le_dimH_image _)396397namespace IsometryEquiv398399@[simp]400theorem dimH_image (e : X ≃ᵢ Y) (s : Set X) : dimH (e '' s) = dimH s :=401 e.isometry.dimH_image s402403@[simp]404theorem dimH_preimage (e : X ≃ᵢ Y) (s : Set Y) : dimH (e ⁻¹' s) = dimH s := by405 rw [← e.image_symm, e.symm.dimH_image]406407theorem dimH_univ (e : X ≃ᵢ Y) : dimH (univ : Set X) = dimH (univ : Set Y) := by408 rw [← e.dimH_preimage univ, preimage_univ]409410end IsometryEquiv411412namespace ContinuousLinearEquiv413414variable {𝕜 E F : Type*} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]415 [NormedAddCommGroup F] [NormedSpace 𝕜 F]416417@[simp]418theorem dimH_image (e : E ≃L[𝕜] F) (s : Set E) : dimH (e '' s) = dimH s :=419 le_antisymm (e.lipschitz.dimH_image_le s) <| by420 simpa only [e.symm_image_image] using e.symm.lipschitz.dimH_image_le (e '' s)421422@[simp]423theorem dimH_preimage (e : E ≃L[𝕜] F) (s : Set F) : dimH (e ⁻¹' s) = dimH s := by424 rw [← e.image_symm_eq_preimage, e.symm.dimH_image]425426theorem dimH_univ (e : E ≃L[𝕜] F) : dimH (univ : Set E) = dimH (univ : Set F) := by427 rw [← e.dimH_preimage, preimage_univ]428429end ContinuousLinearEquiv430431/-!432### Hausdorff dimension in a real vector space433-/434435436namespace Real437438variable {E : Type*} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]439440theorem dimH_ball_pi (x : ι → ℝ) {r : ℝ} (hr : 0 < r) :441 dimH (Metric.ball x r) = Fintype.card ι := by442 cases isEmpty_or_nonempty ι443 · rwa [dimH_subsingleton, eq_comm, Nat.cast_eq_zero, Fintype.card_eq_zero_iff]444 exact fun x _ y _ => Subsingleton.elim x y445 · rw [← ENNReal.coe_natCast]446 have : μH[Fintype.card ι] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι) := by447 rw [hausdorffMeasure_pi_real, Real.volume_pi_ball _ hr]448 refine dimH_of_hausdorffMeasure_ne_zero_ne_top ?_ ?_ <;> rw [NNReal.coe_natCast, this]449 · simp [pow_pos (mul_pos (zero_lt_two' ℝ) hr)]450 · exact ENNReal.ofReal_ne_top451452theorem dimH_ball_pi_fin {n : ℕ} (x : Fin n → ℝ) {r : ℝ} (hr : 0 < r) :453 dimH (Metric.ball x r) = n := by rw [dimH_ball_pi x hr, Fintype.card_fin]454455theorem dimH_univ_pi (ι : Type*) [Fintype ι] : dimH (univ : Set (ι → ℝ)) = Fintype.card ι := by456 simp only [← Metric.iUnion_ball_nat_succ (0 : ι → ℝ), dimH_iUnion,457 dimH_ball_pi _ (Nat.cast_add_one_pos _), iSup_const]458459theorem dimH_univ_pi_fin (n : ℕ) : dimH (univ : Set (Fin n → ℝ)) = n := by460 rw [dimH_univ_pi, Fintype.card_fin]461462theorem dimH_of_mem_nhds {x : E} {s : Set E} (h : s ∈ 𝓝 x) : dimH s = finrank ℝ E := by463 have e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ :=464 ContinuousLinearEquiv.ofFinrankEq (Module.finrank_fin_fun ℝ).symm465 rw [← e.dimH_image]466 refine le_antisymm ?_ ?_467 · exact (dimH_mono (subset_univ _)).trans_eq (dimH_univ_pi_fin _)468 · have : e '' s ∈ 𝓝 (e x) := by rw [← e.map_nhds_eq]; exact image_mem_map h469 rcases Metric.nhds_basis_ball.mem_iff.1 this with ⟨r, hr0, hr⟩470 simpa only [dimH_ball_pi_fin (e x) hr0] using dimH_mono hr471472theorem dimH_of_nonempty_interior {s : Set E} (h : (interior s).Nonempty) : dimH s = finrank ℝ E :=473 let ⟨_, hx⟩ := h474 dimH_of_mem_nhds (mem_interior_iff_mem_nhds.1 hx)475476/-- The Hausdorff dimension of a nonempty convex set equals the dimension of its affine span. -/477theorem Convex.dimH_eq_finrank_vectorSpan {s : Set E} (hcvx : Convex ℝ s) (hne : s.Nonempty) :478 dimH s = finrank ℝ (vectorSpan ℝ s) := by479 have := hne.to_subtype480 let φ := AffineIsometryEquiv.constVSub ℝ481 (⟨hne.some, subset_affineSpan ℝ s hne.some_mem⟩ : affineSpan ℝ s)482 have hs_eq : s = (↑) '' ((↑) ⁻¹' s : Set (affineSpan ℝ s)) :=483 (image_preimage_eq_of_subset <| (subset_affineSpan ℝ s).trans Subtype.range_coe.superset).symm484 rw [hs_eq, isometry_subtype_coe.dimH_image, ← φ.isometry.dimH_image,485 Real.dimH_of_nonempty_interior, direction_affineSpan ℝ s, ← hs_eq]486 simp_rw [← AffineIsometryEquiv.coe_toHomeomorph, ← φ.toHomeomorph.image_interior, image_nonempty]487 simpa [intrinsicInterior] using (intrinsicInterior_nonempty hcvx).mpr hne488489variable (E)490491theorem dimH_univ_eq_finrank : dimH (univ : Set E) = finrank ℝ E :=492 dimH_of_mem_nhds (@univ_mem _ (𝓝 0))493494theorem dimH_univ : dimH (univ : Set ℝ) = 1 := by495 rw [dimH_univ_eq_finrank ℝ, Module.finrank_self, Nat.cast_one]496497variable {E}498499/-- The Hausdorff dimension of any set in a finite-dimensional real normed space is finite. -/500theorem dimH_lt_top (s : Set E) : dimH s < ⊤ := by calc501 dimH s ≤ dimH (univ : Set E) := dimH_mono (subset_univ s)502 _ = finrank ℝ E := dimH_univ_eq_finrank E503 _ < ⊤ := by simp504505theorem dimH_ne_top (s : Set E) : dimH s ≠ ⊤ := (dimH_lt_top s).ne506507lemma hausdorffMeasure_of_finrank_lt [MeasurableSpace E] [BorelSpace E] {d : ℝ}508 (hd : finrank ℝ E < d) : (μH[d] : Measure E) = 0 := by509 lift d to ℝ≥0 using (Nat.cast_nonneg _).trans hd.le510 rw [← measure_univ_eq_zero]511 apply hausdorffMeasure_of_dimH_lt512 rw [dimH_univ_eq_finrank]513 exact mod_cast hd514515/-- The Hausdorff dimension of a non-degenerate segment in a real normed space is 1. -/516theorem dimH_segment {x y : E} (h : x ≠ y) :517 dimH (segment ℝ x y) = 1 := by518 rw [Convex.dimH_eq_finrank_vectorSpan (convex_segment x y) ⟨x, left_mem_segment ℝ x y⟩,519 vectorSpan_segment]520 simp [finrank_span_singleton (sub_ne_zero.mpr h.symm)]521522end Real523524variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]525 [NormedAddCommGroup F] [NormedSpace ℝ F]526527theorem dense_compl_of_dimH_lt_finrank {s : Set E} (hs : dimH s < finrank ℝ E) : Dense sᶜ := by528 refine fun x => mem_closure_iff_nhds.2 fun t ht => nonempty_iff_ne_empty.2 fun he => hs.not_ge ?_529 rw [← sdiff_eq, sdiff_eq_empty] at he530 rw [← Real.dimH_of_mem_nhds ht]531 exact dimH_mono he532533/-!534### Hausdorff dimension and `C¹`-smooth maps535536`C¹`-smooth maps are locally Lipschitz continuous, hence they do not increase the Hausdorff537dimension of sets.538-/539540541/-- Let `f` be a function defined on a finite-dimensional real normed space. If `f` is `C¹`-smooth542on a convex set `s`, then the Hausdorff dimension of `f '' s` is less than or equal to the Hausdorff543dimension of `s`.544545TODO: do we actually need `Convex ℝ s`? -/546theorem ContDiffOn.dimH_image_le {f : E → F} {s t : Set E} (hf : ContDiffOn ℝ 1 f s)547 (hc : Convex ℝ s) (ht : t ⊆ s) : dimH (f '' t) ≤ dimH t :=548 dimH_image_le_of_locally_lipschitzOn fun x hx =>549 let ⟨C, u, hu, hf⟩ := (hf x (ht hx)).exists_lipschitzOnWith hc550 ⟨C, u, nhdsWithin_mono _ ht hu, hf⟩551552/-- The Hausdorff dimension of the range of a `C¹`-smooth function defined on a finite-dimensional553real normed space is at most the dimension of its domain as a vector space over `ℝ`. -/554theorem ContDiff.dimH_range_le {f : E → F} (h : ContDiff ℝ 1 f) : dimH (range f) ≤ finrank ℝ E :=555 calc556 dimH (range f) = dimH (f '' univ) := by rw [image_univ]557 _ ≤ dimH (univ : Set E) := h.contDiffOn.dimH_image_le convex_univ Subset.rfl558 _ = finrank ℝ E := Real.dimH_univ_eq_finrank E559560/-- A particular case of Sard's Theorem. Let `f : E → F` be a map between finite-dimensional real561vector spaces. Suppose that `f` is `C¹` smooth on a convex set `s` of Hausdorff dimension strictly562less than the dimension of `F`. Then the complement of the image `f '' s` is dense in `F`. -/563theorem ContDiffOn.dense_compl_image_of_dimH_lt_finrank [FiniteDimensional ℝ F] {f : E → F}564 {s t : Set E} (h : ContDiffOn ℝ 1 f s) (hc : Convex ℝ s) (ht : t ⊆ s)565 (htF : dimH t < finrank ℝ F) : Dense (f '' t)ᶜ :=566 dense_compl_of_dimH_lt_finrank <| (h.dimH_image_le hc ht).trans_lt htF567568/-- A particular case of Sard's Theorem. If `f` is a `C¹` smooth map from a real vector space to a569real vector space `F` of strictly larger dimension, then the complement of the range of `f` is dense570in `F`. -/571theorem ContDiff.dense_compl_range_of_finrank_lt_finrank [FiniteDimensional ℝ F] {f : E → F}572 (h : ContDiff ℝ 1 f) (hEF : finrank ℝ E < finrank ℝ F) : Dense (range f)ᶜ :=573 dense_compl_of_dimH_lt_finrank <| h.dimH_range_le.trans_lt <| Nat.cast_lt.2 hEF574575/--576The Hausdorff dimension of the orthogonal projection of a set `s` onto a subspace `K`577is less than or equal to the Hausdorff dimension of `s`.578-/579theorem dimH_orthogonalProjectionOnto_le {𝕜 E : Type*} [RCLike 𝕜]580 [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]581 (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (s : Set E) :582 dimH (K.orthogonalProjectionOnto '' s) ≤ dimH s :=583 K.lipschitzWith_orthogonalProjectionOnto.dimH_image_le s584585@[deprecated (since := "2026-05-05")] alias dimH_orthogonalProjection_le :=586 dimH_orthogonalProjectionOnto_le