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

[Merged by Bors] - feat(analysis/special_functions): limit of x^s * exp(-x) for s real #12540

Closed
wants to merge 4 commits into from

Conversation

loefflerd
Copy link
Collaborator


This is a preliminary step for the Gamma function (#12494)

Open in Gitpod

@loefflerd loefflerd added the awaiting-review The author would like community review of the PR label Mar 9, 2022
@sgouezel
Copy link
Collaborator

I have golfed and cleaned up things a little bit. Please revert anything you don't like!

@loefflerd
Copy link
Collaborator Author

Looks good, thanks! I'll have to remember "dsimp", I didn't know about that one -- I guess it is ok to use this mid-argument (without closing the goal), unlike "simp"?

@jcommelin
Copy link
Member

@loefflerd Indeed, dsimp is much less dangerous in the middle of the proof. So that's totally fine.

Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
@semorrison
Copy link
Collaborator

bors merge

@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 Mar 11, 2022
bors bot pushed a commit that referenced this pull request Mar 11, 2022
…12540)

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
@bors
Copy link

bors bot commented Mar 11, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(analysis/special_functions): limit of x^s * exp(-x) for s real [Merged by Bors] - feat(analysis/special_functions): limit of x^s * exp(-x) for s real Mar 11, 2022
@bors bors bot closed this Mar 11, 2022
@bors bors bot deleted the exp_rpow_limits branch March 11, 2022 10:13
laurentbartholdi pushed a commit that referenced this pull request Mar 17, 2022
…12540)

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
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
Development

Successfully merging this pull request may close these issues.

None yet

6 participants