[Merged by Bors] - feat(topology, analysis) : add lemmas about `has_neg.neg` (preliminaries for L'Hopital's rule) #3392

ADedecker · 2020-07-13T21:46:13Z

This PR contains a few lemmas about the has_neg.neg function, such as :

its limit along at_top and at_bot
its limit along nhds a, nhds_within a (Ioi a) and similar filters
its differentiability and derivative

This is a small part of the preliminaries for proving L'Hopital's rule. I am still working on it, but I thought I'd start PR-ing small parts already. The whole discussion is at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/L'Hopital's.20rule/near/203526328

A small comment about naming : in most of the library, concept.neg describes how negating a function acts on its interaction with the concept, whereas concept_neg describes the way the has_neg.neg function interacts with the concept (this is the same for inv btw).

But that isn't the case for deriv and deriv_within so I ended up creating deriv_neg2 and deriv_within_neg2 (yes that's awful). What do you think about that ?

src/topology/algebra/ordered.lean

src/order/filter/at_top_bot.lean

src/topology/algebra/group.lean

urkud · 2020-07-15T10:40:34Z

I golfed some proofs and removed tendsto_inv_nhds, use continuous_inv.tendsto instead.

ADedecker · 2020-07-15T10:49:37Z

I golfed some proofs and removed tendsto_inv_nhds, use continuous_inv.tendsto instead.

Out of curiosity, is there a way to make an alias for this ? It would be easier to guess the name

urkud · 2020-07-15T11:25:32Z

I golfed some proofs and removed tendsto_inv_nhds, use continuous_inv.tendsto instead.

Out of curiosity, is there a way to make an alias for this ? It would be easier to guess the name

@PatrickMassot @sgouezel What do you think about this? Should we have tendsto_inv as a separate lemma or use tendsto_id.inv/continuous_inv.tendsto?

sgouezel · 2020-07-15T11:27:17Z

For coherence and least surprise for newcomers, I think tendsto_inv can not be bad, so I'm willing to add it.

urkud · 2020-07-15T11:29:23Z

Should we rename the normed_field version to tendsto_inv'?

ADedecker · 2020-07-15T12:21:24Z

Since you added tendsto_at_bot I just added tendsto_at_bot', which corresponds to tendsto_at_top'

PatrickMassot · 2020-07-15T20:37:34Z

I don't mind having a couple more aliases.

ADedecker · 2020-07-17T15:28:46Z

Hmm unless I missed something, I think I added the requested changes 🤔 Do I misunderstand the way we use labels @semorrison ?

bryangingechen · 2020-07-17T15:48:14Z

@semorrison might have added the label since there are unresolved comments above – if those are all resolved, please click the "resolve" button beneath them to make it easier for reviewers to see what remains to be done.

ADedecker · 2020-07-17T15:55:19Z

Thanks a lot, I didn't knew that @bryangingechen ! i'm not used to GitHub yes, so I'll keep that in mind

ADedecker · 2020-07-17T19:49:42Z

I did a few other silly mistakes in my last commit, I'm correcting them right now

sgouezel · 2020-07-17T21:05:23Z

src/analysis/normed_space/basic.lean

@@ -619,7 +619,7 @@ begin
  rwa [dist_comm, dist_eq_norm, add_sub_cancel'],
 end

-lemma tendsto_inv [normed_field α] {r : α} (r0 : r ≠ 0) : tendsto (λq, q⁻¹) (𝓝 r) (𝓝 r⁻¹) :=
+lemma tendsto_inv' [normed_field α] {r : α} (r0 : r ≠ 0) : tendsto (λq, q⁻¹) (𝓝 r) (𝓝 r⁻¹) :=


I don't think you need to add a ' on this lemma and the next one, they are in the normed_field namespace so they wouldn't clash with anything else

Ok, and I guess it's the same for continuous_on_inv ?

src/topology/algebra/group.lean

urkud · 2020-07-19T07:38:09Z

src/topology/algebra/ordered.lean

@@ -1944,3 +1944,23 @@ lemma tendsto_of_monotone {ι α : Type*} [preorder ι] [topological_space α]
  tendsto f at_top at_top ∨ (∃ l, tendsto f at_top (𝓝 l)) :=
 if H : bdd_above (range f) then or.inr ⟨_, tendsto_at_top_csupr h_mono H⟩
 else or.inl $ tendsto_at_top_at_top_of_monotone' h_mono H
+
+lemma tendsto_neg_nhds_within_Ioi {α : Type*} [ordered_add_comm_group α]


@jcommelin Should we have a multiplicative version of this? I don't know if we're going to have any topological ordered_comm_groups.

If yes, then @[to_additive] should be able to transfer this lemma from multiplicative to additive.

It doesn't cost anything, so I made it anyway

urkud · 2020-07-19T08:15:06Z

Feel free to merge either as is, or with multiplicative version of various lemmas (and @[to_additive] creating additive versions for you).
bors d+

bors · 2020-07-19T08:15:07Z

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

urkud · 2020-07-19T14:15:23Z

bors merge

…ies for L'Hopital's rule) (#3392) This PR contains a few lemmas about the `has_neg.neg` function, such as : - its limit along `at_top` and `at_bot` - its limit along `nhds a`, `nhds_within a (Ioi a)` and similar filters - its differentiability and derivative Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Anatole Dedecker <48656793+ADedecker@users.noreply.github.com>

bors · 2020-07-19T15:29:40Z

Pull request successfully merged into master.

Build succeeded:

ADedecker added 2 commits July 13, 2020 23:17

feat(topology, analysis) : add lemmas about has_neg.neg

0ca6091

Forgotten lemma x)

590c97f

ADedecker added the awaiting-review The author would like community review of the PR label Jul 13, 2020

Unused argument

033d0f1

sgouezel reviewed Jul 14, 2020

View reviewed changes

src/topology/algebra/ordered.lean Outdated Show resolved Hide resolved

ADedecker added 2 commits July 14, 2020 13:22

Less instances

d428204

Less instances 2

fcd949c

sgouezel reviewed Jul 14, 2020

View reviewed changes

src/topology/algebra/ordered.lean Outdated Show resolved Hide resolved

src/topology/algebra/ordered.lean Outdated Show resolved Hide resolved

src/topology/algebra/ordered.lean Outdated Show resolved Hide resolved

src/order/filter/at_top_bot.lean Outdated Show resolved Hide resolved

Changes

0d30824

sgouezel reviewed Jul 14, 2020

View reviewed changes

src/order/filter/at_top_bot.lean Outdated Show resolved Hide resolved

ADedecker added 2 commits July 14, 2020 21:45

Class cleaning + tendsto_at_bot

7ac8e71

smaller requirements + generalization

f423c02

ADedecker commented Jul 14, 2020

View reviewed changes

src/order/filter/at_top_bot.lean Show resolved Hide resolved

#check

ff9a327

urkud reviewed Jul 15, 2020

View reviewed changes

src/topology/algebra/group.lean Outdated Show resolved Hide resolved

urkud added 3 commits July 15, 2020 06:16

Golf some proofs, move {α} to variables

ec7567a

Merge branch 'master' into neg_limit_deriv

0e2438c

Drop tendsto_inv_nhds, golf some proofs

4fc67be

tendsto_at_bot'

a6be96f

Merge branch 'master' into neg_limit_deriv

2d54a56

Add tendsto_inv, continuous_inv, and rename the normed field versions

f3e9185

semorrison 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 Jul 17, 2020

bryangingechen 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 Jul 17, 2020

Simplify tendsto_inv and add continuous_on_inv

ffc09b5

sgouezel reviewed Jul 17, 2020

View reviewed changes

sgouezel 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 Jul 17, 2020

Undo some renames

6792a61

urkud reviewed Jul 19, 2020

View reviewed changes

Multiplicative versions

543721f

urkud removed the awaiting-author A reviewer has asked the author a question or requested changes label Jul 19, 2020

github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Jul 19, 2020

bors bot changed the title ~~feat(topology, analysis) : add lemmas about has_neg.neg (preliminaries for L'Hopital's rule)~~ [Merged by Bors] - feat(topology, analysis) : add lemmas about has_neg.neg (preliminaries for L'Hopital's rule) Jul 19, 2020

bors bot closed this Jul 19, 2020

bors bot deleted the neg_limit_deriv branch July 19, 2020 15:29

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(topology, analysis) : add lemmas about `has_neg.neg` (preliminaries for L'Hopital's rule) #3392

[Merged by Bors] - feat(topology, analysis) : add lemmas about `has_neg.neg` (preliminaries for L'Hopital's rule) #3392

ADedecker commented Jul 13, 2020 •

edited by bryangingechen

urkud commented Jul 15, 2020

ADedecker commented Jul 15, 2020

urkud commented Jul 15, 2020

sgouezel commented Jul 15, 2020

urkud commented Jul 15, 2020

ADedecker commented Jul 15, 2020

PatrickMassot commented Jul 15, 2020

ADedecker commented Jul 17, 2020

bryangingechen commented Jul 17, 2020

ADedecker commented Jul 17, 2020

ADedecker commented Jul 17, 2020

sgouezel Jul 17, 2020

ADedecker Jul 17, 2020

urkud Jul 19, 2020

urkud Jul 19, 2020

ADedecker Jul 19, 2020

urkud commented Jul 19, 2020

bors bot commented Jul 19, 2020

urkud commented Jul 19, 2020

bors bot commented Jul 19, 2020

[Merged by Bors] - feat(topology, analysis) : add lemmas about has_neg.neg (preliminaries for L'Hopital's rule) #3392

[Merged by Bors] - feat(topology, analysis) : add lemmas about has_neg.neg (preliminaries for L'Hopital's rule) #3392

Conversation

ADedecker commented Jul 13, 2020 • edited by bryangingechen

urkud commented Jul 15, 2020

ADedecker commented Jul 15, 2020

urkud commented Jul 15, 2020

sgouezel commented Jul 15, 2020

urkud commented Jul 15, 2020

ADedecker commented Jul 15, 2020

PatrickMassot commented Jul 15, 2020

ADedecker commented Jul 17, 2020

bryangingechen commented Jul 17, 2020

ADedecker commented Jul 17, 2020

ADedecker commented Jul 17, 2020

sgouezel Jul 17, 2020

Choose a reason for hiding this comment

ADedecker Jul 17, 2020

Choose a reason for hiding this comment

urkud Jul 19, 2020

Choose a reason for hiding this comment

urkud Jul 19, 2020

Choose a reason for hiding this comment

ADedecker Jul 19, 2020

Choose a reason for hiding this comment

urkud commented Jul 19, 2020

bors bot commented Jul 19, 2020

urkud commented Jul 19, 2020

bors bot commented Jul 19, 2020

[Merged by Bors] - feat(topology, analysis) : add lemmas about `has_neg.neg` (preliminaries for L'Hopital's rule) #3392

[Merged by Bors] - feat(topology, analysis) : add lemmas about `has_neg.neg` (preliminaries for L'Hopital's rule) #3392

ADedecker commented Jul 13, 2020 •

edited by bryangingechen