HolderWith.dimH_range_le
theorem HolderWith.dimH_range_le :
∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] {C r : NNReal} {f : X → Y},
HolderWith C r f → 0 < r → dimH (Set.range f) ≤ dimH Set.univ / ↑r
The theorem `HolderWith.dimH_range_le` states that if `f` is a Hölder continuous function with a positive exponent `r`, then the Hausdorff dimension of the range of `f` is less than or equal to the Hausdorff dimension of the domain of `f` divided by `r`. This relationship applies for all types `X` and `Y` that are equipped with an `EMetricSpace` structure, i.e., a metric space structure based on extended non-negative real numbers. Here, `dimH` denotes the Hausdorff dimension, `Set.range f` denotes the range of the function `f`, and `Set.univ` represents the universal set containing all elements of the domain.
More concisely: If `f` is a Hölder continuous function from a metric space `(X, d_X)` to another metric space `(Y, d_Y)` with exponent `r > 0`, then the Hausdorff dimension of `Set.range f` is less than or equal to the Hausdorff dimension of `Set.univ (X)` divided by `r`.
|
ContDiff.dimH_range_le
theorem ContDiff.dimH_range_le :
∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : FiniteDimensional ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F},
ContDiff ℝ 1 f → dimH (Set.range f) ≤ ↑(FiniteDimensional.finrank ℝ E)
This theorem states that for any continuously differentiable function `f` (denoted as `C¹`-smooth function) defined on a finite-dimensional real normed space `E`, the Hausdorff dimension of the range of `f` is not greater than the dimension of its domain as a vector space over the real numbers `ℝ`. Here, the Hausdorff dimension is a measure of the "size" or "complexity" of a set, and the dimension of the domain is determined by the number of basis vectors in the vector space `E`.
More concisely: The Hausdorff dimension of the range of a continuously differentiable function `f` from a finite-dimensional real normed space `E` does not exceed the dimension of `E`.
|
ContDiff.dense_compl_range_of_finrank_lt_finrank
theorem ContDiff.dense_compl_range_of_finrank_lt_finrank :
∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : FiniteDimensional ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F]
[inst_5 : FiniteDimensional ℝ F] {f : E → F},
ContDiff ℝ 1 f → FiniteDimensional.finrank ℝ E < FiniteDimensional.finrank ℝ F → Dense (Set.range f)ᶜ
This theorem is a specific case of Sard's Theorem. It states that if `f` is a continuously differentiable (C¹ smooth) function from a real vector space `E` to a real vector space `F` of strictly larger dimension (the rank of `F` is greater than the rank of `E`), then the complement of the range of `f` is dense in `F`. In other words, every point in `F` is either in the image of `f` or arbitrarily close to the image of `f`. This theorem is a critical component in the study of differentiable mappings between different dimensional spaces.
More concisely: If `f` is a continuously differentiable function from a real vector space `E` to a real vector space `F` of strictly higher dimension, then the complement of `f`'s range is dense in `F`.
|
dimH_mono
theorem dimH_mono : ∀ {X : Type u_2} [inst : EMetricSpace X] {s t : Set X}, s ⊆ t → dimH s ≤ dimH t
The theorem `dimH_mono` states that for any type `X` that has an `EMetricSpace` instance, for any two sets `s` and `t` of type `X`, if `s` is a subset of `t` then the Hausdorff dimension of `s` is less than or equal to the Hausdorff dimension of `t`. In mathematical terms, if $s \subseteq t$, then $\text{dimH}(s) \leq \text{dimH}(t)$. This theorem is a statement about the monotonicity of the Hausdorff dimension in an extended metric space.
More concisely: For any extended metric space (X), if s is a subset of t, then the Hausdorff dimension of s is less than or equal to the Hausdorff dimension of t. (i.e., dimH(s) ≤ dimH(t)).
|
Finset.dimH_zero
theorem Finset.dimH_zero : ∀ {X : Type u_2} [inst : EMetricSpace X] (s : Finset X), dimH ↑s = 0
The theorem `Finset.dimH_zero` states that for any set `s` of finite elements (`Finset`) in an extended metric space `X`, the Hausdorff dimension (`dimH`) of `s` is zero. In other words, in an (e)metric space, the Hausdorff dimension of any finite set is always zero.
More concisely: The Hausdorff dimension of any finite set in an extended metric space is zero.
|
dimH_image_le_of_locally_holder_on
theorem dimH_image_le_of_locally_holder_on :
∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y]
[inst_2 : SecondCountableTopology X] {r : NNReal} {f : X → Y},
0 < r → ∀ {s : Set X}, (∀ x ∈ s, ∃ C, ∃ t ∈ nhdsWithin x s, HolderOnWith C r f t) → dimH (f '' s) ≤ dimH s / ↑r
This theorem states the following: Given a set `s` in a space `X` with a second countable topology, and a function `f: X → Y`, if the function 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 of `s` under `f` (denoted by `f '' s`) is at most the Hausdorff dimension of `s` divided by `r`. The continuity condition here refers to the requirement that for every `x in s`, there exists a coefficient `C` and a set `t` in the neighborhood of `x` within `s` such that the function `f` satisfies the Hölder condition with constant `C` and exponent `r` on the set `t`.
More concisely: If a function from a second countable space with a set of full Hausdorff dimension to another space is Hölder continuous with the same exponent in every neighborhood of each point in the set with positive dimension, then the Hausdorff dimension of the image of the set is strictly smaller than the dimension of the set by the Hölder exponent.
|
Set.Finite.dimH_zero
theorem Set.Finite.dimH_zero : ∀ {X : Type u_2} [inst : EMetricSpace X] {s : Set X}, s.Finite → dimH s = 0
This theorem, referred to as an alias of `dimH_finite`, states that for any set `s` of type `X`, where `X` is an eMetric space, if `s` is finite then the Hausdorff dimension of `s` is zero. The Hausdorff dimension, denoted as `dimH s`, is a measure of the "roughness" or "complexity" of a set, and in this case, it indicates that finite sets in the given eMetric space have a dimension of zero, implying they lack complexity in the sense of the Hausdorff measure.
More concisely: In an eMetric space, the Hausdorff dimension of a finite set is zero.
|
HolderWith.dimH_image_le
theorem HolderWith.dimH_image_le :
∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] {C r : NNReal} {f : X → Y},
HolderWith C r f → 0 < r → ∀ (s : Set X), dimH (f '' s) ≤ dimH s / ↑r
The theorem `HolderWith.dimH_image_le` states that if there is a function `f` from type `X` to type `Y`, both of which are in an extended metric space, and if this function is Hölder continuous with a positive real number exponent `r`, then the Hausdorff dimension of the image of a set `s` under `f` is at most the Hausdorff dimension of `s` divided by `r`. This result highlights the impact of Hölder continuous mappings on the Hausdorff dimension of sets in an extended metric space.
More concisely: If `f` is a Hölder continuous function from a set `X` in an extended metric space to another set `Y` with exponent `r > 0`, then the Hausdorff dimension of `f(s)` is bounded by the Hausdorff dimension of `s` divided by `r`.
|
ContDiffOn.dimH_image_le
theorem ContDiffOn.dimH_image_le :
∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : FiniteDimensional ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F}
{s t : Set E}, ContDiffOn ℝ 1 f s → Convex ℝ s → t ⊆ s → dimH (f '' t) ≤ dimH t
The theorem `ContDiffOn.dimH_image_le` states that for a given function `f` that is defined on a finite-dimensional real normed space `E`, if `f` is continuously differentiable (`C¹`-smooth) on a convex set `s`, then the Hausdorff dimension of the image of the set `s` under function `f` (denoted as `f '' s`) is less than or equal to the Hausdorff dimension of the set `s` itself. It is also mentioned that this result is valid for any subset `t` of `s`, provided that `t` is included in `s` (`t ⊆ s`). However, the theorem leaves open the question of whether the convexity of the set `s` is actually needed for the conclusion to hold.
More concisely: If `f` is a continuously differentiable function on a convex set `s` in a finite-dimensional real normed space, then the Hausdorff dimension of `f(s)` is less than or equal to that of `s`. This holds for any subset `t` of `s` that is included in it. The convexity of `s` may not be necessary.
|
iSup_limsup_dimH
theorem iSup_limsup_dimH :
∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : SecondCountableTopology X] (s : Set X),
⨆ x, Filter.limsup dimH (nhdsWithin x s).smallSets = dimH s
This theorem states that, in an extended metric space equipped with a second-countable topology, the Hausdorff dimension of a set `s` is equivalent to the supremum over all points `x` of the limit superior of the Hausdorff dimensions of `t`, where `t` is in the "small sets" of the "neighborhood within" `s` at `x`. The "neighborhood within" filter at `x` with respect to `s` represents the intersection of `s` and a neighborhood of `x`. "Small sets" refer to the sets in a filter that are "small enough" for specific mathematical considerations. The limit superior of a function along a filter is the infimum of all upper bounds that eventually hold for the function. The Hausdorff dimension is a measure of the 'roughness' or 'complexity' of a set, with higher dimensions indicating more complex sets.
More concisely: In an extended metric space with a second-countable topology, the Hausdorff dimension of a set is equal to the supreme limit superior of the Hausdorff dimensions of the intersections of the set and neighborhoods of each point, with respect to the "neighborhood within" filter.
|
dimH_le
theorem dimH_le :
∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {s : Set X}
{d : ENNReal}, (∀ (d' : NNReal), ↑↑(MeasureTheory.Measure.hausdorffMeasure ↑d') s = ⊤ → ↑d' ≤ d) → dimH s ≤ d
The theorem `dimH_le` states that for any type `X` that is an eMetric space, a Measurable space, and a Borel space, and for any set `s` of type `X` and any extended nonnegative real number `d`, if for all nonnegative real numbers `d'` the Hausdorff measure of `s` with respect to `d'` is infinity implies `d'` is less than or equal to `d`, then the Hausdorff dimension of `s` is less than or equal to `d`. In other words, it sets an upper bound on the Hausdorff dimension of a set in terms of the Hausdorff measures of the set.
More concisely: If a set in an eMetric, Measurable, and Borel space `X` has infinite Hausdorff measure for all `d' < d`, then its Hausdorff dimension is less than or equal to `d`.
|
exists_mem_nhdsWithin_lt_dimH_of_lt_dimH
theorem exists_mem_nhdsWithin_lt_dimH_of_lt_dimH :
∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : SecondCountableTopology X] {s : Set X} {r : ENNReal},
r < dimH s → ∃ x ∈ s, ∀ t ∈ nhdsWithin x s, r < dimH t
This theorem states that if the extended nonnegative real number `r` is less than the Hausdorff dimension of a set `s` in an (extended) metric space with a second countable topology, then there exists a point `x` that is a member of `s` such that every neighborhood `t` of `x` within `s` has a Hausdorff dimension greater than `r`. In other words, within a set in a certain type of space, if we have a particular measure of dimensionality (`r`), we can always find a point and its surrounding neighborhood within the set whose dimensionality exceeds `r`.
More concisely: In a second countable metric space, if a set `s` has Hausdorff dimension greater than a given real number `r`, then there exists a point `x` in `s` such that every neighborhood of `x` within `s` has strictly larger Hausdorff dimension.
|
Set.Countable.dimH_zero
theorem Set.Countable.dimH_zero : ∀ {X : Type u_2} [inst : EMetricSpace X] {s : Set X}, s.Countable → dimH s = 0 := by
sorry
This theorem is named `Set.Countable.dimH_zero` and it states that for any set `s` of type `X` in an extended metric space, if `s` is countable, then the Hausdorff dimension of `s` is zero. In other words, if you have a countable set in a space with a metric, the Hausdorff dimension of that set is always zero. The Hausdorff dimension is a measure of the 'complexity' or 'roughness' of a set, and this theorem tells us that countable sets are 'zero-dimensional' in this sense.
More concisely: If `s` is a countable subset of a metric space `X`, then the Hausdorff dimension of `s` is zero.
|
le_dimH_of_hausdorffMeasure_eq_top
theorem le_dimH_of_hausdorffMeasure_eq_top :
∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {s : Set X}
{d : NNReal}, ↑↑(MeasureTheory.Measure.hausdorffMeasure ↑d) s = ⊤ → ↑d ≤ dimH s
The theorem `le_dimH_of_hausdorffMeasure_eq_top` states that for any type `X` equipped with an `EMetricSpace`, `MeasurableSpace`, and `BorelSpace` structure, any set `s` of `X`, and nonnegative real number `d`, if the Hausdorff measure of `s` with the exponent equal to `d` is infinite (denoted by `⊤`), then the Hausdorff dimension of `s` is greater than or equal to `d`. The Hausdorff dimension here is defined as the supremum of all `d` for which the `d`-dimensional Hausdorff measure of the set is infinite. Hence, the theorem essentially says that if a set has infinite `d`-dimensional Hausdorff measure, it must have Hausdorff dimension at least `d`.
More concisely: If the Hausdorff measure of a set in an EMetricSpace with respect to a given exponent is infinite, then its Hausdorff dimension is greater than or equal to that exponent.
|
dimH_image_le_of_locally_lipschitzOn
theorem dimH_image_le_of_locally_lipschitzOn :
∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y]
[inst_2 : SecondCountableTopology X] {f : X → Y} {s : Set X},
(∀ x ∈ s, ∃ C, ∃ t ∈ nhdsWithin x s, LipschitzOnWith C f t) → dimH (f '' s) ≤ dimH s
The theorem `dimH_image_le_of_locally_lipschitzOn` states that given a set `s` in an extended metric space `X` with a second countable topology and a function `f` mapping from `X` to another extended metric space `Y`, if `f` is Lipschitz continuous within a neighborhood of every point `x` in `s` (i.e., the distance between `f(x)` and `f(y)` is at most some constant times the distance between `x` and `y`, for all `x` and `y` in the neighborhood), then the Hausdorff dimension of the image of `s` under `f` (denoted as `f '' s`) is less than or equal to the Hausdorff dimension of `s`. The Hausdorff dimension provides a measure of the "roughness" or "complexity" of a set, so this theorem essentially states that this "complexity" cannot increase under a locally Lipschitz continuous mapping.
More concisely: If a function between extended metric spaces is locally Lipschitz continuous on a set in a second countable topology, then the Hausdorff dimension of the image of the set is less than or equal to the Hausdorff dimension of the set.
|
ContDiffOn.dense_compl_image_of_dimH_lt_finrank
theorem ContDiffOn.dense_compl_image_of_dimH_lt_finrank :
∀ {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : FiniteDimensional ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F]
[inst_5 : FiniteDimensional ℝ F] {f : E → F} {s t : Set E},
ContDiffOn ℝ 1 f s → Convex ℝ s → t ⊆ s → dimH t < ↑(FiniteDimensional.finrank ℝ F) → Dense (f '' t)ᶜ
This theorem is a specific instance of Sard's Theorem. It states that for a differentiable map `f` from a real finite-dimensional vector space `E` to another real finite-dimensional vector space `F`, if `f` is C¹ smooth on a convex set `s` whose Hausdorff dimension is strictly less than the dimension of `F`, then the complement of the image of `f` on `s` is dense in `F`. In other words, for any point in `F`, there exists a sequence of points not in the image of `f` that converges to that point.
More concisely: If `f` is a C¹ smooth map between real finite-dimensional vector spaces, and `s` is a convex set of strictly smaller Hausdorff dimension than the destination space, then the complement of `f(s)` in the destination space is dense.
|
HolderOnWith.dimH_image_le
theorem HolderOnWith.dimH_image_le :
∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] {C r : NNReal} {f : X → Y}
{s : Set X}, HolderOnWith C r f s → 0 < r → dimH (f '' s) ≤ dimH s / ↑r
This theorem states that for any two eMetric spaces `X` and `Y`, any set `s` of elements of `X`, and any function `f` from `X` to `Y`, if `f` is Hölder continuous with exponent `r > 0` on the set `s`, then the Hausdorff dimension of the image of `s` under `f` is less than or equal to the Hausdorff dimension of `s` divided by `r`.
Here, Hölder continuity with exponent `r` means that the extended metric distance between `f(x)` and `f(y)` for any `x, y` in `s` is less than or equal to `C` times the extended metric distance between `x` and `y` raised to the power of `r`. The Hausdorff dimension of a set in an eMetric space is defined as the supremum of all `d` such that the `d`-dimensional Hausdorff measure of the set is infinite.
More concisely: The Hausdorff dimension of the image of a set under a Hölder continuous function with exponent r is less than or equal to the Hausdorff dimension of the set divided by r.
|
dimH_def
theorem dimH_def :
∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] (s : Set X),
dimH s = ⨆ d, ⨆ (_ : ↑↑(MeasureTheory.Measure.hausdorffMeasure ↑d) s = ⊤), ↑d
The theorem `dimH_def` provides the explicit formulation for the Hausdorff dimension of a set in an extended metric space. Specifically, for any set `s` in a type `X` that forms an extended metric space and also supports the concepts of measurability and Borel measurability, the Hausdorff dimension of `s` is the supremum (the least upper bound) of all real numbers `d` such that the Hausdorff measure of `s` with respect to `d` is infinite.
More concisely: The Hausdorff dimension of a measurable and Borel measurable set in an extended metric space is the supremum of real numbers d such that the Hausdorff measure of the set with respect to d is infinite.
|
bsupr_limsup_dimH
theorem bsupr_limsup_dimH :
∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : SecondCountableTopology X] (s : Set X),
⨆ x ∈ s, Filter.limsup dimH (nhdsWithin x s).smallSets = dimH s
In an extended metric space with a second countable topology, the theorem `bsupr_limsup_dimH` states that the Hausdorff dimension of a set `s` is equal to the supremum over all elements `x` in `s` of the limit superior of the Hausdorff dimension of subsets `t` converging towards `x` within the set `s`. The limit superior is taken along the filter of all small sets of the neighborhood of `x` within the set `s`. This theorem provides a way to compute the Hausdorff dimension of a set in terms of the Hausdorff dimensions of smaller subsets within its local neighborhoods.
More concisely: In an extended metric space with a second countable topology, the Hausdorff dimension of a set equals the supremum of the limit superiors of its Hausdorff dimensions in subsets converging to any point in the set.
|
LipschitzOnWith.dimH_image_le
theorem LipschitzOnWith.dimH_image_le :
∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] {K : NNReal} {f : X → Y}
{s : Set X}, LipschitzOnWith K f s → dimH (f '' s) ≤ dimH s
The theorem `LipschitzOnWith.dimH_image_le` states that for any function `f` from type `X` to type `Y`, where both `X` and `Y` are types in an extended metric space, and any set `s` of type `X`, if the function `f` is Lipschitz continuous on `s` with a nonnegative real number `K` as the Lipschitz constant, then the Hausdorff dimension of the image of `s` under `f` (denoted as `f '' s`) is less than or equal to the Hausdorff dimension of `s`. In other words, a Lipschitz continuous function does not increase the Hausdorff dimension when mapping a set to its image.
More concisely: If `f: X → Y` is a Lipschitz continuous function with Lipschitz constant `K` on set `s ⊆ X` in extended metric spaces `X` and `Y`, then the Hausdorff dimension of `f(s)` is less than or equal to the Hausdorff dimension of `s`.
|
LipschitzWith.dimH_range_le
theorem LipschitzWith.dimH_range_le :
∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] {K : NNReal} {f : X → Y},
LipschitzWith K f → dimH (Set.range f) ≤ dimH Set.univ
This theorem states that if a function `f` is Lipschitz continuous, then the Hausdorff dimension of its range is less than or equal to the Hausdorff dimension of its domain. Here, the Lipschitz continuity of `f` is specified with a nonnegative real constant `K`, the Hausdorff dimension of a set is measured in an eMetric space, and the range of a function and the domain are considered as sets. Essentially, this theorem captures that Lipschitz continuous maps do not increase the Hausdorff dimension.
More concisely: If `f` is a Lipschitz continuous function with constant `K` from a set of Hausdorff dimension `d` to another set, then the Hausdorff dimension of the range of `f` is less than or equal to `d`.
|
hausdorffMeasure_of_dimH_lt
theorem hausdorffMeasure_of_dimH_lt :
∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {s : Set X}
{d : NNReal}, dimH s < ↑d → ↑↑(MeasureTheory.Measure.hausdorffMeasure ↑d) s = 0
This theorem, `hausdorffMeasure_of_dimH_lt`, states that for a set `s` in a space `X`, which is equipped with an eMetric space structure, a measurable space structure, and a Borel space structure, if the Hausdorff dimension of `s` is strictly less than a nonnegative real number `d`, then the Hausdorff measure of `s` with associated dimension `d` is zero. In other words, if the Hausdorff dimension of a set is less than a certain value, the Hausdorff measure of the set at that value reduces to zero.
More concisely: If a measurable set in a metric space has Hausdorff dimension strictly less than a given number, then its Hausdorff measure with that dimension is zero.
|
dimH_iUnion
theorem dimH_iUnion :
∀ {X : Type u_2} [inst : EMetricSpace X] {ι : Sort u_4} [inst_1 : Countable ι] (s : ι → Set X),
dimH (⋃ i, s i) = ⨆ i, dimH (s i)
This theorem states that for any type `X` equipped with an eMetric space structure, and for any countable index set `ι`, the Hausdorff dimension of the union of sets generated by a function `s : ι → Set X` is equal to the supremum of the Hausdorff dimensions of the individual sets `s i`. In other words, the Hausdorff dimension of the union of a countable collection of sets is the largest Hausdorff dimension of any set in the collection.
More concisely: For any countable index set `ι` and function `s : ι → Set X` defining a collection of subsets of a metric space `(X, d)`, the Hausdorff dimension of their union is equal to the supremum of the Hausdorff dimensions of the individual sets.
|
dimH_range_le_of_locally_lipschitzOn
theorem dimH_range_le_of_locally_lipschitzOn :
∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y]
[inst_2 : SecondCountableTopology X] {f : X → Y},
(∀ (x : X), ∃ C, ∃ s ∈ nhds x, LipschitzOnWith C f s) → dimH (Set.range f) ≤ dimH Set.univ
This theorem states that if a function `f` from one type `X` to another type `Y` is Lipschitz continuous within a neighborhood of every point `x` in `X`, then the Hausdorff dimension of the range of `f` is less than or equal to the Hausdorff dimension of `X`. In more mathematical terms, given a function `f: X → Y` where `X` and `Y` are both Emetric spaces, if for every `x` in `X` there exists a real constant `C` and a set `s` in the neighborhood of `x` such that `f` is Lipschitz continuous with constant `C` on `s`, then the Hausdorff dimension of the image of `f` is less than or equal to the Hausdorff dimension of the entire set `X`. This theorem captures the intuitive idea that a continuous transformation cannot arbitrarily increase the "complexity" or "dimensionality" of a set.
More concisely: If every point in an Emetric space `X` has a neighborhood on which a continuous function `f: X → Y` is Lipschitz, then the Hausdorff dimension of `f(X)` is less than or equal to the Hausdorff dimension of `X`.
|
Set.Subsingleton.dimH_zero
theorem Set.Subsingleton.dimH_zero :
∀ {X : Type u_2} [inst : EMetricSpace X] {s : Set X}, s.Subsingleton → dimH s = 0
This theorem, referred to as an alias of `dimH_subsingleton`, states that for any set `s` of type `X`, where `X` is equipped with an eMetric space structure, if `s` is a subsingleton, then the Hausdorff dimension of `s` is zero. In other words, if a set contains at most one element in an eMetric space, its Hausdorff dimension, a measure of the "roughness" or "complexity" of the set, is zero.
More concisely: If a subsingleton set `s` in an eMetric space `X` has Hausdorff dimension, then that dimension is zero.
|
dimH_bUnion
theorem dimH_bUnion :
∀ {ι : Type u_1} {X : Type u_2} [inst : EMetricSpace X] {s : Set ι},
s.Countable → ∀ (t : ι → Set X), dimH (⋃ i ∈ s, t i) = ⨆ i ∈ s, dimH (t i)
The theorem `dimH_bUnion` states that for any type `ι`, type `X` with an eMetricSpace instance, a countable set `s` of type `ι`, and a function `t` from `ι` to `Set X`, the Hausdorff dimension of the union of all sets `t i` where `i` belongs to `s` is equal to the supremum of the Hausdorff dimensions of all sets `t i` where `i` belongs to `s`. In mathematical terms, we can write this as: for a countable index set `s`, the Hausdorff dimension of the union over `s` of sets `t i` is the supremum of the Hausdorff dimensions of the individual sets `t i`.
More concisely: The Hausdorff dimension of the countable union of sets in a metric space, each with finite Hausdorff dimension, is equal to the supreme of their individual Hausdorff dimensions.
|
Real.dimH_of_mem_nhds
theorem Real.dimH_of_mem_nhds :
∀ {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E] {x : E}
{s : Set E}, s ∈ nhds x → dimH s = ↑(FiniteDimensional.finrank ℝ E)
This theorem states that for any normed additive commutative group `E` that is a normed space over the real numbers `ℝ` and is finite-dimensional, given any point `x` in `E` and any set `s` in `E` that is a neighborhood of `x` (i.e., `s` belongs to the neighborhood filter of `x`), the Hausdorff dimension of `s` is equal to the rank of `E` as a module over `ℝ`. The rank of `E` is expressed as a natural number using `FiniteDimensional.finrank`. In essence, the theorem is a connection between topological dimension (Hausdorff dimension) and algebraic dimension (rank) in the context of finite-dimensional normed spaces over the reals.
More concisely: In a finite-dimensional, real normed space, the Hausdorff dimension of a neighborhood of any point equals the rank of the space as an $\mathbb{R}$-module.
|
LipschitzWith.dimH_image_le
theorem LipschitzWith.dimH_image_le :
∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] {K : NNReal} {f : X → Y},
LipschitzWith K f → ∀ (s : Set X), dimH (f '' s) ≤ dimH s
The theorem `LipschitzWith.dimH_image_le` states that if `f` is a Lipschitz continuous function, then the Hausdorff dimension of the image of a set `s` under `f` is less than or equal to the Hausdorff dimension of the set `s` itself. Here, the Hausdorff dimension of a set in a metric space is denoted by `dimH`. The set `s` is a collection of elements of some type `X`, and `f` is a function mapping from `X` to another type `Y`. Both `X` and `Y` are types in an extended metric space.
More concisely: If `f` is Lipschitz continuous, then `dimH(f(s)) ≤ dimH(s)` for any set `s` in a metric space.
|
dimH_range_le_of_locally_holder_on
theorem dimH_range_le_of_locally_holder_on :
∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y]
[inst_2 : SecondCountableTopology X] {r : NNReal} {f : X → Y},
0 < r → (∀ (x : X), ∃ C, ∃ s ∈ nhds x, HolderOnWith C r f s) → dimH (Set.range f) ≤ dimH Set.univ / ↑r
The theorem `dimH_range_le_of_locally_holder_on` states that if a function `f : X → Y` is Hölder continuous in a neighborhood of every point in `X` with the same positive exponent `r`, but possibly varying coefficients, then the Hausdorff dimension of the range of `f` is at most the Hausdorff dimension of `X` divided by `r`. Here, a function is considered Hölder continuous if the extended metric distance between `f(x)` and `f(y)` is less than or equal to the product of a non-negative real number `C` and the `r`th power of the extended metric distance between `x` and `y`. The Hausdorff dimension in this context is defined in terms of the Hausdorff measure, which measures the "size" of a set in a metric space.
More concisely: If a function is Hölder continuous on a metric space with exponent r and the same coefficient at each point, then the Hausdorff dimension of its range is at most the Hausdorff dimension of the domain divided by r.
|