Snowflaking of a metric space #
Given a (pseudo) (extended) metric space X and a number 0 < α ≤ 1,
one can consider the metric given by d x y = (dist x y) ^ α.
The metric space determined by this new metric is said to be the α-snowflaking (or α-snowflake)
of X. In this file we define Metric.Snowflaking X α hα₀ hα₁ to be a one-field structure wrapper
around X with metric given by this formula.
The use of the term snowflaking arises from the fact that if one chooses X := Set.Icc 0 1 and
α := log 3 / log 4, then Metric.Snowflaking X α … … is isometric to the von Koch snowflake,
where we equip that space with the natural metric induced by the α⁻¹-Hausdorff measure of paths.
Snowflake metrics are used regularly in the geometry of metric spaces where, among other things,
they characterize doubling metrics. In particular, a metric is doubling if and only
if every α-snowflaking (with 0 < α < 1) of it is bilipschitz equivalent to a subset of some
Euclidean space (the dimension of the Euclidean space depends on α). See [Hei01].
Another reason to introduce this definition is the following.
In the proof of his version of the Morse-Sard theorem,
Moreira [Mor01] studies maps of two variables that are Lipschitz continuous in one variable,
but satisfy a stronger assumption ‖f (a, y) - f (a, b)‖ = O(‖y - b‖ ^ (k + α))
along the second variable, as long as (a, b) is one of the "interesting" points.
If we want to apply Vitali covering theorem in this context, we need to cover the set by products
closedBall a (R ^ (k + α)) ×ˢ closedBall b R so that both components make a similar contribution
to ‖f (x, y) - f (a, b)‖. These sets aren't balls in the original metric
(or even subsets of balls that occupy at least a fixed fraction of the volume,
as we require in our version of Vitali theorem).
However, if we change the metric on the first component to the one introduced in this file, then these sets become balls, and we can apply Vitali theorem.
References #
- [Carlos Gustavo T. de A. Moreira, Hausdorff measures and the Morse-Sard theorem] [Mor01]
A copy of a type with metric given by dist x y = (dist x.val y.val) ^ α.
This is defined as a one-field structure.
- val : X
The value wrapped in
x : Snowflaking X α hα₀ hα₁.
Instances For
The natural equivalence between Snowflaking X α hr₀ hr₁ and X.
Equations
- Metric.Snowflaking.ofSnowflaking = { toFun := Metric.Snowflaking.val, invFun := Metric.Snowflaking.mk, left_inv := ⋯, right_inv := ⋯ }
Instances For
The natural equivalence between X and Snowflaking X α hr₀ hr₁.
Instances For
This definition makes cases x and induction x use toSnowflaking instead of mk.
Equations
- Metric.Snowflaking.casesOn_toSnowflaking toSnowflaking x = toSnowflaking x.val
Instances For
Topological space structure #
The topology on Snowflaking X α hα₀ hα₁ is induced from X.
The topological space structure on Snowflaking X α _ _ is induced from the original space.
The natural homeomorphism between Snowflaking X α hα₀ hα₁ and X.
Equations
- Metric.Snowflaking.homeomorph = { toEquiv := Metric.Snowflaking.ofSnowflaking, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
We copy some instances from the underlying space X to Snowflaking X α hα₀ hα₁.
In the future, we can add more of them, if needed,
or even copy all the topology-related classes, if we get a tactic to do it automatically.
Bornology #
The bornology on Snowflaking X α hα₀ hα₁ is induced from X.
Uniform space structure #
The uniform space structure on Snowflaking X α hα₀ hα₁ is induced from X.
The natural uniform space equivalence between Snowflaking X α hα hα₁
and the underlying space.
Equations
- Metric.Snowflaking.uniformEquiv = { toEquiv := Metric.Snowflaking.ofSnowflaking, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }
Instances For
Extended distance and a (pseudo) extended metric space structure #
Th extended distance on Snowflaking X α hα₀ hα₁
is given by edist x y = (edist x.ofSnowflaking y.ofSnowflaking) ^ α.
If the original space is a (pseudo) extended metric space, then so is Snowflaking X α hα₀ hα₁.
Equations
- Metric.Snowflaking.instEDist = { edist := fun (x y : Metric.Snowflaking X α hα₀ hα₁) => edist (Metric.Snowflaking.ofSnowflaking x) (Metric.Snowflaking.ofSnowflaking y) ^ α }
Equations
- One or more equations did not get rendered due to their size.
Equations
Distance and a (pseudo) metric space structure #
Th extended distance on Snowflaking X α hα₀ hα₁
is given by dist x y = (dist x.ofSnowflaking y.ofSnowflaking) ^ α.
If the original space is a (pseudo) metric space, then so is Snowflaking X α hα₀ hα₁.
Equations
- Metric.Snowflaking.instDist = { dist := fun (x y : Metric.Snowflaking X α hα₀ hα₁) => dist (Metric.Snowflaking.ofSnowflaking x) (Metric.Snowflaking.ofSnowflaking y) ^ α }