Skip to content

[Merged by Bors] - feat(Data/Real/EReal): add inverse and division of ENNReals#14224

Closed
pitmonticone wants to merge 26 commits intomasterfrom
pitmonticone/ERealDiv
Closed

[Merged by Bors] - feat(Data/Real/EReal): add inverse and division of ENNReals#14224
pitmonticone wants to merge 26 commits intomasterfrom
pitmonticone/ERealDiv

Conversation

@pitmonticone
Copy link
Copy Markdown
Member

@pitmonticone pitmonticone commented Jun 28, 2024 •
edited
Loading

This PR adds API for inverse and division of extended reals.

Co-authored-by: @D-Thomine

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 28, 2024 •
edited
Loading

PR summary cbbfb55dff

Import changes

No significant changes to the import graph

Declarations diff

+ antitone_div_right_of_nonpos
+ bot_div_of_neg_ne_bot
+ bot_div_of_pos_ne_top
+ coe_div
+ coe_inv
+ div_bot
+ div_div
+ div_eq_inv_mul
+ div_le_div_right_of_nonneg
+ div_le_div_right_of_nonpos
+ div_le_iff_le_mul
+ div_lt_div_right_of_neg
+ div_lt_div_right_of_pos
+ div_mul_cancel
+ div_nonneg
+ div_nonneg_of_nonpos_of_nonpos
+ div_nonpos_of_nonneg_of_nonpos
+ div_nonpos_of_nonpos_of_nonneg
+ div_right_distrib_of_nonneg
+ div_self
+ div_top
+ div_zero
+ instance : DivInvMonoid EReal where inv := EReal.inv
+ instance : DivInvOneMonoid EReal
+ instance : Inv (EReal) := ⟨EReal.inv⟩
+ inv
+ inv_bot
+ inv_inv
+ inv_neg
+ inv_neg_of_neg_ne_bot
+ inv_nonneg_of_nonneg
+ inv_nonpos_of_nonpos
+ inv_pos_of_pos_ne_top
+ inv_top
+ inv_zero
+ le_div_iff_mul_le
+ monotone_div_right_of_nonneg
+ mul_div
+ mul_div_cancel
+ mul_div_mul_cancel
+ mul_div_right
+ mul_inv
+ sign_mul_inv_abs
+ sign_mul_inv_abs'
+ strictAnti_div_right_of_neg
+ strictMono_div_right_of_pos
+ top_div_of_neg_ne_bot
+ top_div_of_pos_ne_top
+ zero_div

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@pitmonticone pitmonticone mentioned this pull request Jun 28, 2024
Merged
@pitmonticone pitmonticone marked this pull request as ready for review June 28, 2024 12:49
@pitmonticone pitmonticone marked this pull request as draft June 28, 2024 12:53
sgouezel
sgouezel reviewed Jun 28, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@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.

It's a bad idea to define a non-homogeneous division on EReal → ENNReal → EReal. Instead, as I discussed with Damien, one should define an homogeneous division on EReal, first be defining an inverse function and then using (a, b) -> a * b⁻¹.

@pitmonticone pitmonticone marked this pull request as ready for review June 28, 2024 13:03
@pitmonticone pitmonticone changed the title feat(Data/Real/EReal): add division by ENNReals feat(Data/Real/EReal): add inverse of ENNReals Jun 28, 2024
@pitmonticone pitmonticone changed the title feat(Data/Real/EReal): add inverse of ENNReals feat(Data/Real/EReal): add inverse and division of ENNReals Jun 28, 2024
@pitmonticone pitmonticone requested a review from sgouezel June 28, 2024 13:39
@sgouezel sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 28, 2024
@pitmonticone
Copy link
Copy Markdown
Member Author

pitmonticone commented Jun 28, 2024

Yes, I believe that is the new API in BET/TopologicalEntropy.

@D-Thomine can you confirm?

@pitmonticone pitmonticone added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 29, 2024
@pitmonticone pitmonticone requested a review from sgouezel June 29, 2024 23:16
@pitmonticone @LorenzoLuccioli
Update EReal.lean
edd47f1 
Co-Authored-By: Lorenzo Luccioli <71074618+LorenzoLuccioli@users.noreply.github.com>
sgouezel
sgouezel reviewed Jun 30, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@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 very good. Minor tweaks are required about the naming of lemmas, though.

@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jun 30, 2024
@pitmonticone @LorenzoLuccioli
Address review comments
4ef7bf5 
Co-Authored-By: Lorenzo Luccioli <71074618+LorenzoLuccioli@users.noreply.github.com>
@pitmonticone
Copy link
Copy Markdown
Member Author

pitmonticone commented Jun 30, 2024

I should have addressed all review comments.

Thank you very much @sgouezel for your review!

@pitmonticone pitmonticone added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 30, 2024
@pitmonticone pitmonticone requested a review from sgouezel June 30, 2024 10:24
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 30, 2024
@sgouezel
Copy link
Copy Markdown
Contributor

sgouezel commented Jun 30, 2024

bors r+
Thanks!

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 30, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 30, 2024
@pitmonticone
feat(Data/Real/EReal): add inverse and division of ENNReals (#14224)
db17c10 
This PR adds API for inverse and division  of extended reals. 

Co-authored-by: @D-Thomine
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 30, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Data/Real/EReal): add inverse and division of ENNReals [Merged by Bors] - feat(Data/Real/EReal): add inverse and division of ENNReals Jun 30, 2024
@mathlib-bors mathlib-bors bot closed this Jun 30, 2024
@mathlib-bors mathlib-bors bot deleted the pitmonticone/ERealDiv branch June 30, 2024 14:30
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@pitmonticone @dagurtomas
feat(Data/Real/EReal): add inverse and division of ENNReals (#14224)
996ac08 
This PR adds API for inverse and division  of extended reals. 

Co-authored-by: @D-Thomine
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sgouezel sgouezel Awaiting requested review from sgouezel

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@pitmonticone @sgouezel