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(analysis/calculus/times_cont_diff, analysis/calculus/inverse): smooth inverse function theorem #4407

Closed
wants to merge 26 commits into from
Closed

[Merged by Bors] - feat(analysis/calculus/times_cont_diff, analysis/calculus/inverse): smooth inverse function theorem #4407

wants to merge 26 commits into from

Conversation

hrmacbeth
Copy link
Member

@hrmacbeth hrmacbeth commented Oct 4, 2020 •
edited

The inverse function theorem, in the C^k and smooth categories.

Co-authored-by: Yury G. Kudryashov urkud@urkud.name

There are a couple of lemmas which seem like they should be much shorter if approached the right way, or refactored to extract the right simp-lemmas: continuous_linear_equiv.is_open, image_to_local_homeomorph_image_basepoint. Perhaps @urkud or @sgouezel could take a look. (Update: these lemmas have been cleaned up thanks to @urkud.)

bryangingechen
bryangingechen reviewed Oct 4, 2020
View reviewed changes
src/analysis/calculus/fderiv.lean Outdated Show resolved Hide resolved
src/analysis/calculus/fderiv.lean Outdated Show resolved Hide resolved
@hrmacbeth @bryangingechen
Apply suggestions from code review
f0d963c 
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
@hrmacbeth hrmacbeth added the awaiting-review The author would like community review of the PR label Oct 4, 2020
@urkud
Copy link
Member

urkud commented Oct 5, 2020

I have some golfing in mind but it requires moving code between files. I'll try it later.

@urkud
Copy link
Member

urkud commented Oct 6, 2020 •
edited

@sgouezel What do you think about merging this as is? I want to have timed_cont_diff_at real.sqrt (easy after this PR) for #4458. UPD: I think I found a way to simplify some proofs (see below). @hrmacbeth could you test if it works, please?

@urkud urkud 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 6, 2020
@hrmacbeth hrmacbeth 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 Oct 7, 2020
@hrmacbeth hrmacbeth mentioned this pull request Oct 7, 2020
Closed
1 task
hrmacbeth and others added 5 commits October 7, 2020 01:46
@hrmacbeth
authors and module doc
3eb9fed
@urkud
Golf a proof
096023e
@urkud
More subsingleton/unique instances
2caa90b
@urkud
Merge branch 'master' into smooth-inverse
abf1821
@urkud
chore(*): add a few more unique instances
ff8bc11 
* `linear_map.unique_of_left`, `linear_map.unique_of_right`,
  `continuous_linear_map.unique_of_left`,
  `continuous_linear_map.unique_of_right`: if either `M` or `M₂` is a
  `subsingleton`, then both `M →ₗ[R] M₂` and `M →L[R] M₂` are
  `unique`;
* `pi.unique`: if each `β a` is `unique`, then `Π a, β a` is `unique`;
* rename `function.injective.comap_subsingleton` to
  `function.injective.subsingleton`;
* add `unique.mk'` and `function.injective.unique`;
* add a few `simp` lemmas for `default`;
* drop `nonempty_unique_or_exists_ne` and `subsingleton_or_exists_ne`.
@urkud urkud mentioned this pull request Oct 7, 2020
Closed
@urkud urkud added blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. and removed awaiting-review The author would like community review of the PR labels Oct 7, 2020
bors bot pushed a commit that referenced this pull request Oct 8, 2020
@urkud
chore(*): add a few more unique instances (#4511)
306e949 
* `linear_map.unique_of_left`, `linear_map.unique_of_right`,
  `continuous_linear_map.unique_of_left`,
  `continuous_linear_map.unique_of_right`: if either `M` or `M₂` is a
  `subsingleton`, then both `M →ₗ[R] M₂` and `M →L[R] M₂` are
  `unique`;
* `pi.unique`: if each `β a` is `unique`, then `Π a, β a` is `unique`;
* rename `function.injective.comap_subsingleton` to
  `function.injective.subsingleton`;
* add `unique.mk'` and `function.injective.unique`;
* add a few `simp` lemmas for `default`;
* drop `nonempty_unique_or_exists_ne` and `subsingleton_or_exists_ne`;
* rename `linear_map.coe_inj` to `coe_injective` and `continuous_linear_map.coe_inj` to `coe_fn_injective`,
  make them use `function.injective`.

Motivated by #4407
bors bot pushed a commit that referenced this pull request Oct 8, 2020
@urkud
chore(*): add a few more unique instances (#4511)
f3f7f70 
* `linear_map.unique_of_left`, `linear_map.unique_of_right`,
  `continuous_linear_map.unique_of_left`,
  `continuous_linear_map.unique_of_right`: if either `M` or `M₂` is a
  `subsingleton`, then both `M →ₗ[R] M₂` and `M →L[R] M₂` are
  `unique`;
* `pi.unique`: if each `β a` is `unique`, then `Π a, β a` is `unique`;
* rename `function.injective.comap_subsingleton` to
  `function.injective.subsingleton`;
* add `unique.mk'` and `function.injective.unique`;
* add a few `simp` lemmas for `default`;
* drop `nonempty_unique_or_exists_ne` and `subsingleton_or_exists_ne`;
* rename `linear_map.coe_inj` to `coe_injective` and `continuous_linear_map.coe_inj` to `coe_fn_injective`,
  make them use `function.injective`.

Motivated by #4407
bors bot pushed a commit that referenced this pull request Oct 8, 2020
@urkud
chore(*): add a few more unique instances (#4511)
e74bd26 
* `linear_map.unique_of_left`, `linear_map.unique_of_right`,
  `continuous_linear_map.unique_of_left`,
  `continuous_linear_map.unique_of_right`: if either `M` or `M₂` is a
  `subsingleton`, then both `M →ₗ[R] M₂` and `M →L[R] M₂` are
  `unique`;
* `pi.unique`: if each `β a` is `unique`, then `Π a, β a` is `unique`;
* rename `function.injective.comap_subsingleton` to
  `function.injective.subsingleton`;
* add `unique.mk'` and `function.injective.unique`;
* add a few `simp` lemmas for `default`;
* drop `nonempty_unique_or_exists_ne` and `subsingleton_or_exists_ne`;
* rename `linear_map.coe_inj` to `coe_injective` and `continuous_linear_map.coe_inj` to `coe_fn_injective`,
  make them use `function.injective`.

Motivated by #4407
@urkud urkud added awaiting-review The author would like community review of the PR and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Oct 8, 2020
sgouezel
sgouezel reviewed Oct 11, 2020
View reviewed changes
Copy link
Collaborator

@sgouezel sgouezel left a comment

Choose a reason for hiding this comment

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

This looks good.

There are two obvious refactors that are calling here:

  • do not deduce the continuity of bounded bilinear maps from their differentiability, to be able to put several facts at more natural places
  • Generalize real stuff to is_R_or_C fields (or another typeclass if necessary)

All this can wait for later PRs.

src/analysis/calculus/inverse.lean Outdated Show resolved Hide resolved
src/analysis/calculus/times_cont_diff.lean Outdated Show resolved Hide resolved
src/analysis/calculus/times_cont_diff.lean Outdated Show resolved Hide resolved
src/analysis/calculus/times_cont_diff.lean Outdated Show resolved Hide resolved
hrmacbeth and others added 3 commits October 11, 2020 13:28
@hrmacbeth @sgouezel
Apply suggestions from code review
55793e6 
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
@hrmacbeth
remove simp
f15cdb8
@hrmacbeth
fix build
01b0723
@sgouezel
Copy link
Collaborator

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 Oct 11, 2020
bors bot pushed a commit that referenced this pull request Oct 11, 2020
@hrmacbeth @urkud
feat(analysis/calculus/times_cont_diff, analysis/calculus/inverse): s…
b1ca33e 
…mooth inverse function theorem (#4407)

The inverse function theorem, in the C^k and smooth categories.

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
@bors
Copy link

bors bot commented Oct 11, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(analysis/calculus/times_cont_diff, analysis/calculus/inverse): smooth inverse function theorem [Merged by Bors] - feat(analysis/calculus/times_cont_diff, analysis/calculus/inverse): smooth inverse function theorem Oct 11, 2020
@bors bors bot closed this Oct 11, 2020
@bors bors bot deleted the smooth-inverse branch October 11, 2020 21:16
@urkud urkud mentioned this pull request Oct 12, 2020
Closed
5 tasks
@hrmacbeth hrmacbeth mentioned this pull request Sep 25, 2021
Closed
bors bot pushed a commit that referenced this pull request Sep 28, 2021
@hrmacbeth @sgouezel
feat(analysis/normed_space/is_bounded_bilinear_map): direct proof of …
1db626e 
…continuity (#9390)

Previously `is_bounded_bilinear_map.continuous`, the continuity of a bounded bilinear map, was deduced from its differentiability and lived in `analysis.calculus.fderiv`.  This PR gives a direct proof so it can live in `analysis.normed_space.bounded_linear_maps`.

Two consequences of this lemma are also moved earlier in the hierarchy:
- `continuous_linear_equiv.is_open`, the openness of the set of continuous linear equivalences in the space of continuous linear maps, moves from `analysis.calculus.fderiv` to `analysis.normed_space.bounded_linear_maps`
- `continuous_inner`, the continuity of the inner product, moves from `analysis.inner_product_space.calculus` to `analysis.inner_product_space.basic`.

Previously discussed at
#4407 (review)



Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@urkud urkud urkud left review comments

@bryangingechen bryangingechen bryangingechen left review comments

@sgouezel sgouezel sgouezel left review comments

Assignees

@sgouezel sgouezel

Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@hrmacbeth @urkud @sgouezel @bryangingechen