Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(analysis/special_functions): the japanese bracket#16491

Closed
mcdoll wants to merge 20 commits intomasterfrom
mcdoll/integrable_rpow_add_one
Closed

[Merged by Bors] - feat(analysis/special_functions): the japanese bracket#16491
mcdoll wants to merge 20 commits intomasterfrom
mcdoll/integrable_rpow_add_one

Conversation

@mcdoll
Copy link
Copy Markdown
Member

@mcdoll mcdoll commented Sep 13, 2022

This PR defines and proves basic properties of the japanese bracket, in particular we prove the integrability criterion for negative powers.


Open in Gitpod

@mcdoll mcdoll added WIP Work in progress t-analysis Analysis (normed *, calculus) labels Sep 13, 2022
@ghost ghost added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Sep 15, 2022
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Sep 29, 2022
@ghost
Copy link
Copy Markdown

ghost commented Sep 29, 2022

@mcdoll mcdoll added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Oct 1, 2022
@ocfnash ocfnash 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 24, 2022
@mcdoll mcdoll requested a review from a team as a code owner October 24, 2022 11:45
@mcdoll mcdoll 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 25, 2022
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@leanprover-community-bot-assistant leanprover-community-bot-assistant 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 Nov 4, 2022
bors bot pushed a commit that referenced this pull request Nov 4, 2022
This PR defines and proves basic properties of the japanese bracket, in particular we prove the integrability criterion for negative powers.
@bors
Copy link
Copy Markdown

bors bot commented Nov 4, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Nov 4, 2022
This PR defines and proves basic properties of the japanese bracket, in particular we prove the integrability criterion for negative powers.
@bors
Copy link
Copy Markdown

bors bot commented Nov 4, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(analysis/special_functions): the japanese bracket [Merged by Bors] - feat(analysis/special_functions): the japanese bracket Nov 4, 2022
@bors bors bot closed this Nov 4, 2022
@bors bors bot deleted the mcdoll/integrable_rpow_add_one branch November 4, 2022 11:59
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) t-analysis Analysis (normed *, calculus)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants