Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

extended distance #986

Merged
merged 3 commits into from
Jul 26, 2023
Merged

extended distance #986

merged 3 commits into from
Jul 26, 2023

Conversation

zstone1
Copy link
Contributor

@zstone1 zstone1 commented Jul 19, 2023

Motivation for this change

Rather than wait on HB to introduce a structure with a "standard" distance, we can introduce this "extended" distance function for pseudometrics to finish Urysohn's Lemma. This is part of track A of #965.

Things done/to do
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers
Compatibility with MathComp 2.0
  • I added the label TODO: HB port to make sure someone ports this PR to
    the hierarchy-builder branch or I already opened an issue or PR (please cross reference).
Automatic note to reviewers

Read this Checklist and put a milestone if possible.

@zstone1 zstone1 added the TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done. label Jul 19, 2023
@zstone1 zstone1 marked this pull request as ready for review July 19, 2023 16:07
@affeldt-aist affeldt-aist self-requested a review July 26, 2023 01:51
Copy link
Member

@affeldt-aist affeldt-aist left a comment

Choose a reason for hiding this comment

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

I suggest to move inf/sup lemmas to reals.v and to rename imply_orE to implyE which seems to agree better with the naming convention used so far. I think I spotted a few missing trivial lemmas and that a few computational steps could be shortened, hence the last commit.

@zstone1 zstone1 merged commit 7da8655 into math-comp:master Jul 26, 2023
@CohenCyril
Copy link
Member

Nice! I would rather advocate for a curried distance function edist : T -> T -> T. Was there a particular reason for the uncurried version?

@zstone1
Copy link
Contributor Author

zstone1 commented Jul 26, 2023

Yes, stating continuity from the product does not require dealing with function space topologies. Uncurrying is not generally continuous, and requires extra assumptions on the domain (like locally compact). However, continuity from the product is stronger, and true here. So it's the right thing to prove regardless.

I suppose we could define edist as curried, and prove uncurry edist is continuous. I would be fine with that, if you'd rather make make the curried version the default.

I have #926 proving all this stuff about continuity of curry/uncurry, anyway. (It's barely a draft. Proofs are done, it just need a linting/reorganizing pass).

affeldt-aist added a commit to affeldt-aist/analysis that referenced this pull request Jul 29, 2023
* extended distance

* adding docs

* shorten computations, factor out lemmas

---------

Co-authored-by: Reynald Affeldt <[email protected]>
proux01 pushed a commit that referenced this pull request Jul 31, 2023
* extended distance

* adding docs

* shorten computations, factor out lemmas

---------

Co-authored-by: Reynald Affeldt <[email protected]>
@proux01 proux01 removed the TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done. label Jul 31, 2023
IshiguroYoshihiro pushed a commit to IshiguroYoshihiro/analysis that referenced this pull request Sep 7, 2023
* extended distance

* adding docs

* shorten computations, factor out lemmas

---------

Co-authored-by: Reynald Affeldt <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants