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: lemmas about monotonicity and asymptotics of rpow #6140

Closed
wants to merge 16 commits into from
Closed

[Merged by Bors] - feat: lemmas about monotonicity and asymptotics of rpow #6140

wants to merge 16 commits into from

Conversation

dupuisf
Copy link
Contributor

@dupuisf dupuisf commented Jul 25, 2023

Open in Gitpod

@dupuisf dupuisf added awaiting-review The author would like community review of the PR awaiting-CI labels Jul 25, 2023
@dupuisf dupuisf changed the title feat: lemmas about monotonicity and asymptotics of rpow and exp feat: lemmas about monotonicity and asymptotics of rpow Jul 26, 2023
@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes t-analysis Analysis (normed *, calculus) and removed awaiting-review The author would like community review of the PR labels Aug 1, 2023
dupuisf and others added 4 commits August 2, 2023 20:52
@dupuisf @sgouezel
Update Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
b7029a9 
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
@dupuisf @sgouezel
Update Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
17ba6a3 
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
@dupuisf @sgouezel
Update Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
fab740f 
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
@dupuisf
using lt_trichotomy
d2506ba
@dupuisf dupuisf 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 Aug 2, 2023
j-loreaux
j-loreaux reviewed Aug 8, 2023
View reviewed changes
Copy link
Collaborator

@j-loreaux j-loreaux left a comment •
edited

Choose a reason for hiding this comment

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

These are just golfs, but I think they actually improve readability rather than hindering it. In particular, it put the main content in a single refine so that we can see these are all just the same pattern: tendsto_exp_at{Bot,Top}.comp <| tendsto_const_mul_at{Bot,Top}_...

This also avoids a lot of unnecessary haves and shows.

Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean Outdated Show resolved Hide resolved
Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean Outdated Show resolved Hide resolved
Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean Outdated Show resolved Hide resolved
Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean Outdated Show resolved Hide resolved
Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean Outdated Show resolved Hide resolved
Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean Outdated Show resolved Hide resolved
Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean Outdated Show resolved Hide resolved
@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 Aug 8, 2023
@j-loreaux j-loreaux self-assigned this Aug 8, 2023
dupuisf and others added 6 commits August 12, 2023 19:43
@dupuisf @j-loreaux
Update Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
92d33f8 
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
@dupuisf @j-loreaux
Update Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
eb7e86e 
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
@dupuisf @j-loreaux
Update Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
8b52af1 
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
@dupuisf @j-loreaux
Update Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
6676349 
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
@dupuisf @j-loreaux
Update Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
e4b47be 
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
@dupuisf @j-loreaux
Update Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
a4c7803 
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
@dupuisf @j-loreaux
Update Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
0d19a7a 
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
@dupuisf dupuisf 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 Aug 12, 2023
@sgouezel
Copy link
Contributor

bors r+
Thanks!

@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 Aug 13, 2023
bors bot pushed a commit that referenced this pull request Aug 13, 2023
@dupuisf
feat: lemmas about monotonicity and asymptotics of rpow (#6140)
f697ccc 
Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
@bors
Copy link

bors bot commented Aug 13, 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: lemmas about monotonicity and asymptotics of rpow [Merged by Bors] - feat: lemmas about monotonicity and asymptotics of rpow Aug 13, 2023
@bors bors bot closed this Aug 13, 2023
@bors bors bot deleted the dupuisf/akra_bazzi_lemmas_batch4 branch August 13, 2023 08:45
semorrison pushed a commit that referenced this pull request Aug 14, 2023
@dupuisf @semorrison
feat: lemmas about monotonicity and asymptotics of rpow (#6140)
bf06930 
Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
semorrison pushed a commit that referenced this pull request Aug 15, 2023
@dupuisf @semorrison
feat: lemmas about monotonicity and asymptotics of rpow (#6140)
42ea209 
Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
semorrison pushed a commit that referenced this pull request Aug 15, 2023
@dupuisf @semorrison
feat: lemmas about monotonicity and asymptotics of rpow (#6140)
3ed4e09 
Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
semorrison pushed a commit that referenced this pull request Aug 17, 2023
@dupuisf @semorrison
feat: lemmas about monotonicity and asymptotics of rpow (#6140)
89372ed 
Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

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

@sgouezel sgouezel sgouezel left review comments

Assignees

@j-loreaux j-loreaux

Labels
ready-to-merge This PR has been sent to bors. t-analysis Analysis (normed *, calculus)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@dupuisf @sgouezel @j-loreaux