[Merged by Bors] - feat: define Metric.Snowflaking

[urkud]

From https://github.com/urkud/SardMoreira

This is a copy of the original space with distance redefined to be d x y = (dist x y) ^ α.

---

[github-actions]

PR summary 05f342bfce

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Topology.MetricSpace.Snowflaking (new file)	1616

---

Declarations diff

+ Snowflaking
+ casesOn_toSnowflaking
+ continuous_ofSnowflaking
+ continuous_toSnowflaking
+ dist_ofSnowflaking_ofSnowflaking
+ dist_toSnowflaking_toSnowflaking
+ ediam_image_ofSnowflaking
+ ediam_image_toSnowflaking
+ ediam_preimage_ofSnowflaking
+ ediam_preimage_toSnowflaking
+ edist_def
+ edist_ofSnowflaking_ofSnowflaking
+ edist_toSnowflaking_toSnowflaking
+ homeomorph
+ image_ofSnowflaking_ball
+ image_ofSnowflaking_closedBall
+ image_ofSnowflaking_emetricBall
+ image_ofSnowflaking_emetricClosedBall
+ image_ofSnowflaking_eq_preimage
+ image_ofSnowflaking_image_toSnowflaking
+ image_toSnowflaking_ball
+ image_toSnowflaking_closedBall
+ image_toSnowflaking_emetricBall
+ image_toSnowflaking_emetricClosedBall
+ image_toSnowflaking_eq_preimage
+ image_toSnowflaking_image_ofSnowflaking
+ instance : Bornology (Snowflaking X α hα₀ hα₁) := .induced ofSnowflaking
+ instance : EDist (Snowflaking X α hα₀ hα₁)
+ instance : PseudoEMetricSpace (Snowflaking X α hα₀ hα₁)
+ instance : PseudoMetricSpace (Snowflaking X α hα₀ hα₁)
+ instance : TopologicalSpace (Snowflaking X α hα₀ hα₁) := .induced Snowflaking.ofSnowflaking ‹_›
+ instance : UniformSpace (Snowflaking X α hα₀ hα₁)
+ instance [Dist X] : Dist (Snowflaking X α hα₀ hα₁)
+ instance [EMetricSpace X] : EMetricSpace (Snowflaking X α hα₀ hα₁)
+ instance [MetricSpace X] : MetricSpace (Snowflaking X α hα₀ hα₁)
+ instance [SecondCountableTopology X] : SecondCountableTopology (Snowflaking X α hα₀ hα₁)
+ instance [T0Space X] : T0Space (Snowflaking X α hα₀ hα₁)
+ instance [T2Space X] : T2Space (Snowflaking X α hα₀ hα₁)
+ isBounded_image_ofSnowflaking_iff
+ isBounded_image_toSnowflaking_iff
+ isBounded_preimage_ofSnowflaking_iff
+ isBounded_preimage_toSnowflaking_iff
+ mk_eq_toSnowflaking
+ ofSnowflaking
+ ofSnowflaking_comp_toSnowflaking
+ ofSnowflaking_toSnowflaking
+ preimage_ofSnowflaking_ball
+ preimage_ofSnowflaking_closedBall
+ preimage_ofSnowflaking_emetricBall
+ preimage_ofSnowflaking_emetricClosedBall
+ preimage_toSnowflaking_ball
+ preimage_toSnowflaking_closedBall
+ preimage_toSnowflaking_emetricBall
+ preimage_toSnowflaking_emetricClosedBall
+ symm_ofSnowflaking
+ symm_toSnowflaking
+ toSnowflaking
+ toSnowflaking.sizeOf_spec
+ toSnowflaking_comp_ofSnowflaking
+ toSnowflaking_ofSnowflaking
+ uniformContinuous_ofSnowflaking
+ uniformContinuous_toSnowflaking
+ uniformEquiv
+ val_eq_ofSnowflaking

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.06)

Current number	Change	Type
18	1	disabled simpNF lints

Current commit 81ad12ffb6
Reference commit 05f342bfce

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[j-loreaux]

Before jumping into the bulk of this PR, which I will do tomorrow, let me bikeshed a bit. I think I would prefer Metric.Snowflake (or Metric.Snowflaking) instead of WithRPowDist. Snowflaking a metric is a common technique in geometric measure theory, and since it has a nice suggestive name, I propose we use it.

At the very least, we should mention snowflaking in the module documentation and docstring somewhere.

[urkud]

It's definitely a gap in my education :-(. I've just reinvented this wheel, because the balls were of a wrong shape. I'll definitely rename it tomorrow. Could you please add more motivation to the module docstring?

[j-loreaux]

Overall, aside from the naming issue, I think this is fine. I'll note a few things:

1. My claim about the bilipschitz embedding of snowflaked versions of doubling metric measure spaces is Proposition 2.6 in https://www.numdam.org/article/BSMF_1983__111__429_0.pdf by Assouad. Technically, 2.6 is only one of the implications, but the other is easier and is mentioned higher up in that section of the paper.
2. A standard reference in geometric measure theory that references snowflaking is Juha Heinonen's Lectures on Analysis on Metric Spaces. The beginning of Chapter 12 contains the definition.

[urkud]

Overall, aside from the naming issue, I think this is fine. I'll note a few things:

1. My claim about the bilipschitz embedding of snowflaked versions of doubling metric measure spaces is Proposition 2.6 in [numdam.org/article/BSMF_1983__111__429_0.pdf](https://www.numdam.org/article/BSMF_1983__111__429_0.pdf) by Assouad. Technically, 2.6 is only one of the implications, but the other is easier and is mentioned higher up in that section of the paper.

The paper talks about metric spaces of finite metric dimension. Is it the same?

[j-loreaux]

Overall, aside from the naming issue, I think this is fine. I'll note a few things:

1. My claim about the bilipschitz embedding of snowflaked versions of doubling metric measure spaces is Proposition 2.6 in [numdam.org/article/BSMF_1983__111__429_0.pdf](https://www.numdam.org/article/BSMF_1983__111__429_0.pdf) by Assouad. Technically, 2.6 is only one of the implications, but the other is easier and is mentioned higher up in that section of the paper.

The paper talks about metric spaces of finite metric dimension. Is it the same?

Yes, that's the one I meant. Sorry I forgot the hypothesis about finite metric dimension.

[j-loreaux]

Can you add the reference to either Assouad or Heinonen that I mention here? I'm fine with either or both. Otherwise, LGTM.

bors d+

[mathlib-bors]

✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[j-loreaux]

This needs to go in our bibliography:

@book {heinonen2001,
    AUTHOR = {Heinonen, Juha},
     TITLE = {Lectures on analysis on metric spaces},
    SERIES = {Universitext},
 PUBLISHER = {Springer-Verlag, New York},
      YEAR = {2001},
     PAGES = {x+140},
      ISBN = {0-387-95104-0},
   MRCLASS = {30C65 (28A75 28A78 46E35)},
  MRNUMBER = {1800917},
MRREVIEWER = {Christopher\ Bishop},
       DOI = {10.1007/978-1-4613-0131-8},
       URL = {https://doi.org/10.1007/978-1-4613-0131-8},
}

[urkud]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Post-Build Step