Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(topology/metric_space/dilation): Dilations on metric spaces#14315

Closed
winston-h-zhang wants to merge 30 commits intomasterfrom
hzhang-dilations
Closed

[Merged by Bors] - feat(topology/metric_space/dilation): Dilations on metric spaces#14315
winston-h-zhang wants to merge 30 commits intomasterfrom
hzhang-dilations

Conversation

@winston-h-zhang
Copy link
Copy Markdown
Collaborator

@winston-h-zhang winston-h-zhang commented May 22, 2022 •
edited by alreadydone
Loading

We define dilation α β as the type of maps that satisfy edist (f x) (f y) = r * edist x y for all x y. Here r : ℝ≥0, so we do not exclude the degenerate case of dilations which collapse into constant maps.

After this I will extend to {linear, affine}_dilation_{equiv}s and {linear, affine}_isometry_{equiv}s.

Open in Gitpod

@winston-h-zhang winston-h-zhang self-assigned this May 22, 2022
@winston-h-zhang winston-h-zhang added the awaiting-review The author would like community review of the PR label May 22, 2022
@winston-h-zhang winston-h-zhang requested a review from jsm28 May 22, 2022 22:19
jsm28
jsm28 reviewed May 23, 2022
View reviewed changes
jsm28
jsm28 reviewed May 23, 2022
View reviewed changes
@winston-h-zhang
Copy link
Copy Markdown
Collaborator Author

winston-h-zhang commented May 24, 2022

Thanks for the comments! I hope I've addressed everything

@winston-h-zhang winston-h-zhang requested a review from jsm28 May 25, 2022 16:31
jsm28
jsm28 reviewed May 27, 2022
View reviewed changes
@winston-h-zhang winston-h-zhang requested a review from jsm28 May 31, 2022 16:34
@winston-h-zhang
Copy link
Copy Markdown
Collaborator Author

winston-h-zhang commented Jun 3, 2022 •
edited
Loading

@jsm28 Please take a look at this again when you have the time! I've also requested Eric's review if you happen to be busy.

eric-wieser
eric-wieser reviewed Jun 3, 2022
View reviewed changes
@winston-h-zhang
Copy link
Copy Markdown
Collaborator Author

winston-h-zhang commented Jun 13, 2022 •
edited
Loading

@eric-wieser @urkud, I've put up a new definition of dilation and ratio that is well-defined. I still have the existential inside the structure, then as Yury suggested I defined ratio with if ... then ... else. This actually went quite smoothly. Let me know what you guys think!

@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Sep 1, 2022

I'm pretty short on time at the moment, I'm happy to let another maintainer take over

@urkud urkud added awaiting-review The author would like community review of the PR t-topology Topological spaces, uniform spaces, metric spaces, filters t-analysis Analysis (normed *, calculus) and removed awaiting-author A reviewer has asked the author a question or requested changes labels Sep 1, 2022
@j-loreaux j-loreaux self-assigned this Oct 4, 2022
j-loreaux
j-loreaux reviewed Oct 4, 2022
View reviewed changes
Copy link
Copy Markdown
Collaborator

@j-loreaux j-loreaux left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Lots of suggestions, all relatively small. Some are important though. Among them:

  • typos
  • style issues
  • golfs
  • protecting names which conflict with ones in the root namespace (this is important)
  • a suggestion about splitting the existential in some hypotheses

After these are all fixed it should be ready for merging.

@j-loreaux j-loreaux added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Oct 4, 2022
urkud and others added 2 commits November 5, 2022 01:25
@urkud @j-loreaux
Apply suggestions from code review
8154d26 
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
@JovanGerb
fix errors
9189b50
@urkud urkud mentioned this pull request May 23, 2023
Closed
@urkud urkud added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jun 8, 2023
@urkud
Copy link
Copy Markdown
Member

urkud commented Jun 9, 2023

@eric-wieser Should we merge it now?

eric-wieser
eric-wieser reviewed Jun 9, 2023
View reviewed changes
src/topology/metric_space/dilation.lean Outdated
Comment on lines +13 to +14
We define dilations, i.e., maps between emetric spaces that satisfy
`edist (f x) (f y) = r * edist x y`.
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser Jun 9, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This description is misleading because it doesn't allow r = 0 or r = \top. I think we should add an explanation of why we don't want to consider those cases in this module docstring.

@j-loreaux
Copy link
Copy Markdown
Collaborator

j-loreaux commented Jun 23, 2023

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 23, 2023

🚀 Pull request has been placed on the maintainer queue by j-loreaux.

@dupuisf
Copy link
Copy Markdown
Collaborator

dupuisf commented Jun 23, 2023

bors r+

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jun 23, 2023
bors bot pushed a commit that referenced this pull request Jun 23, 2023
@winston-h-zhang @urkud @JovanGerb
feat(topology/metric_space/dilation): Dilations on metric spaces (#14315
93f8809 
)


We define `dilation α β` as the type of maps that satisfy `edist (f x) (f y) = r * edist x y` for all `x y`. Here `r : ℝ≥0`, so we do not exclude the degenerate case of dilations which collapse into constant maps. 

After this I will extend to `{linear, affine}_dilation_{equiv}`s and `{linear, affine}_isometry_{equiv}`s.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: JovanGerb <jovan.gerbscheid@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Jun 23, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat(topology/metric_space/dilation): Dilations on metric spaces [Merged by Bors] - feat(topology/metric_space/dilation): Dilations on metric spaces Jun 23, 2023
@bors bors bot closed this Jun 23, 2023
@bors bors bot deleted the hzhang-dilations branch June 23, 2023 20:17
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

@jsm28 jsm28 Awaiting requested review from jsm28

3 more reviewers

@urkud urkud urkud left review comments

@eric-wieser eric-wieser eric-wieser left review comments

@j-loreaux j-loreaux j-loreaux left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

@j-loreaux j-loreaux

Labels

ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) t-analysis Analysis (normed *, calculus) t-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

7 participants

@winston-h-zhang @urkud @jsm28 @eric-wieser @j-loreaux @dupuisf @JovanGerb