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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat: function is differentiable outside of its tsupport #9669

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - feat: function is differentiable outside of its tsupport #9669

wants to merge 1 commit into from

Conversation

grunweg
Copy link
Collaborator

@grunweg grunweg commented Jan 11, 2024

From sphere-eversion; I'm just submitting it.

Also golf the proof of the preceding lemma slightly and add a docstring.

Open in Gitpod

@grunweg grunweg added awaiting-review The author would like community review of the PR t-differential-geometry Manifolds etc labels Jan 11, 2024
@ADedecker
Copy link
Member

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Jan 11, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jan 11, 2024
@grunweg
feat: function is differentiable outside of its tsupport (#9669)
709f51d 
From sphere-eversion; I'm just submitting it.

Also golf the proof of the preceding lemma slightly and add a docstring.
@mathlib-bors
Copy link

mathlib-bors bot commented Jan 12, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: function is differentiable outside of its tsupport [Merged by Bors] - feat: function is differentiable outside of its tsupport Jan 12, 2024
@mathlib-bors mathlib-bors bot closed this Jan 12, 2024
@mathlib-bors mathlib-bors bot deleted the MR-sphereeversion-contmdiff branch January 12, 2024 00:15
@alreadydone
Copy link
Contributor

These should be to_additivized from the mulTSupposrt versions. And you missed the opportunity to golf ContMDiff.extend_one below.

@ADedecker
Copy link
Member

My bad, I should have seen that in the review indeed. @grunweg could you open another PR implementing Junyan's suggestions please?

@grunweg
Copy link
Collaborator Author

grunweg commented Jan 14, 2024 •
edited

@ADedecker @alreadydone Thanks for the fast merge. I just implemented the to_additive suggestion, but failed to golf extend_one. Code is at 14f53396f450fe9d47443338ab6a33add7160a56. What do you think.

@ADedecker
Copy link
Member

I can't open that link

@grunweg
Copy link
Collaborator Author

grunweg commented Jan 15, 2024

Oops, fixed the link.

@ADedecker
Copy link
Member

Can you open a PR with that code? I'll write a suggestion there

@ADedecker
Copy link
Member

Okay I found the issue: you should state contMDiffWithinAt_of_not_mem_mulTSupport for any manifold with one, not only a normed space. I guess there are a lot of things in the file that could be generalized then, do you want to do so?

@grunweg
Copy link
Collaborator Author

grunweg commented Jan 15, 2024 •
edited

Okay I found the issue: you should state contMDiffWithinAt_of_not_mem_mulTSupport for any manifold with one, not only a normed space. I guess there are a lot of things in the file that could be generalized then, do you want to do so?

Thanks! I looked through that file, there was just this lemma to generalise; I just did so. Submitted as 9764.

@grunweg grunweg mentioned this pull request Jan 15, 2024
Closed
mathlib-bors bot pushed a commit that referenced this pull request Jan 16, 2024
@grunweg @ADedecker
refactor(ContMDiff/Basic): multiplicativise, generalise and golf cont…
22fea43 
…MDiff_of_support and friends (#9764)

- multiplicativise `contMDiff_of_support`, `contMDiffWithinAt_of_not_mem` and `contMDiffAt_of_not_mem` and use to_additive
- golf `extend_one` with the multiplicative version
- generalise these lemmas to manifolds with zero/one
- slight clean-up: remove unused variables and `open`s
- slight drive-by golfing of one proof
- deprecate `eventuallyEq_zero_nhds` in favor of `not_mem_tsupport_iff_eventuallyEq`

Addresses the post-merge review comments in #9669.




Co-authored-by: ADedecker <anatolededecker@gmail.com>
Co-authored-by: grunweg <grunweg@posteo.de>
mathlib-bors bot pushed a commit that referenced this pull request Jan 16, 2024
@grunweg @ADedecker
refactor(ContMDiff/Basic): multiplicativise, generalise and golf cont…
d602bc2 
…MDiff_of_support and friends (#9764)

- multiplicativise `contMDiff_of_support`, `contMDiffWithinAt_of_not_mem` and `contMDiffAt_of_not_mem` and use to_additive
- golf `extend_one` with the multiplicative version
- generalise these lemmas to manifolds with zero/one
- slight clean-up: remove unused variables and `open`s
- slight drive-by golfing of one proof
- deprecate `eventuallyEq_zero_nhds` in favor of `not_mem_tsupport_iff_eventuallyEq`

Addresses the post-merge review comments in #9669.




Co-authored-by: ADedecker <anatolededecker@gmail.com>
Co-authored-by: grunweg <grunweg@posteo.de>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
ready-to-merge This PR has been sent to bors. t-differential-geometry Manifolds etc
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@grunweg @ADedecker @alreadydone