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: Positivity extension for Finset.prod #9365

Closed
wants to merge 29 commits into from
Closed

[Merged by Bors] - feat: Positivity extension for Finset.prod #9365

wants to merge 29 commits into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Dec 30, 2023 •
edited by Parcly-Taxel
Loading

@YaelDillies @alexjbest
feat: Positivity extension for Finset.sum
64fa1c5 
Note this extension is pretty unopinionated about deriving `Finset.Nonempty` assumptions. We might want to buff it up in the future but it's already a big improvement over the nothing we currently have.

From LeanAPAP

Co-authored-by: Alex J. Best <[email protected]>
@YaelDillies YaelDillies added awaiting-review t-meta Tactics, attributes or user commands t-algebra Algebra (groups, rings, fields, etc) t-order Order theory labels Dec 30, 2023
@YaelDillies
Copy link
Collaborator Author

YaelDillies commented Dec 31, 2023 •
edited
Loading

Computability.AkraBazzi errors with ...

EDIT: Now fixed

@eric-wieser
Copy link
Member

Here's a simpler test-case:

example (s : Finset (ℕ)) : 0 ≤ ∑ j in s, j := by positivity  --ok
example (s : Finset (ℕ)) : 0 ≤ s.sum id := by positivity -- fails

@alexjbest
Copy link
Member

I pushed an attempt at a fix, we beta expand if the f is not already a lambda

@YaelDillies YaelDillies mentioned this pull request Feb 13, 2024
Merged
@dwrensha dwrensha mentioned this pull request Mar 7, 2024
Open
thorimur
thorimur reviewed Mar 7, 2024
View reviewed changes
Copy link
Collaborator

@thorimur thorimur left a comment

Choose a reason for hiding this comment

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

Love how much can be replaced with by positivity due to this PR! :)

This review is shorter than it appears: almost all of these 12 comments are about $, with only a couple potentially "meaningful" review comments.

Mathlib/Algebra/BigOperators/Order.lean Outdated Show resolved Hide resolved
Mathlib/Algebra/BigOperators/Order.lean Outdated Show resolved Hide resolved
Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean Outdated Show resolved Hide resolved
Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean Outdated Show resolved Hide resolved
Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean Outdated Show resolved Hide resolved
Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean Outdated Show resolved Hide resolved
Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean Outdated Show resolved Hide resolved
Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean Outdated Show resolved Hide resolved
Mathlib/MeasureTheory/Integral/TorusIntegral.lean Outdated Show resolved Hide resolved
Mathlib/Algebra/BigOperators/Order.lean Outdated Show resolved Hide resolved
Vierkantor
Vierkantor reviewed Apr 3, 2024
View reviewed changes
Copy link
Contributor

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

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

Looks good with @thorimur's comments. (I am neutral about the <| vs $ issue, but the style guide takes precedence.) @robertylewis, any suggestions or shall we delegate it to @thorimur?

Mathlib/Algebra/BigOperators/Order.lean Outdated Show resolved Hide resolved
Mathlib/Algebra/BigOperators/Order.lean Outdated Show resolved Hide resolved
@Vierkantor Vierkantor added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Apr 3, 2024
@YaelDillies YaelDillies added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 3, 2024
@YaelDillies @Vierkantor
whitespace for clarity
bc25cf0 
Co-authored-by: Anne Baanen <[email protected]>
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 5, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 5, 2024
@thorimur
Copy link
Collaborator

thorimur commented Apr 6, 2024

LGTM! :)

@eric-wieser
Copy link
Member

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit e6a642d.
There were no significant changes against commit d5a796b.

@kim-em
Copy link
Contributor

kim-em commented May 7, 2024

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels May 7, 2024
mathlib-bors bot pushed a commit that referenced this pull request May 7, 2024
@YaelDillies @eric-wieser @alexjbest
feat: Positivity extension for Finset.prod (#9365)
ba9d411 
Followup to #9365

From LeanAPAP



Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Alex J Best <[email protected]>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented May 8, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: Positivity extension for Finset.prod [Merged by Bors] - feat: Positivity extension for Finset.prod May 8, 2024
@mathlib-bors mathlib-bors bot closed this May 8, 2024
@mathlib-bors mathlib-bors bot deleted the positivity_finset_sum branch May 8, 2024 00:17
apnelson1 pushed a commit that referenced this pull request May 12, 2024
@YaelDillies @eric-wieser
@alexjbest @apnelson1
feat: Positivity extension for Finset.prod (#9365)
77b3751 
Followup to #9365

From LeanAPAP



Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Alex J Best <[email protected]>
callesonne pushed a commit that referenced this pull request May 16, 2024
@YaelDillies @eric-wieser
@alexjbest @callesonne
feat: Positivity extension for Finset.prod (#9365)
cb1349d 
Followup to #9365

From LeanAPAP



Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Alex J Best <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@thorimur thorimur thorimur left review comments

@adomani adomani adomani left review comments

@Vierkantor Vierkantor Vierkantor left review comments

@alexjbest alexjbest alexjbest left review comments

@dwrensha dwrensha dwrensha left review comments

@eric-wieser eric-wieser eric-wieser left review comments

Assignees

@robertylewis robertylewis

Labels
ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc) t-meta Tactics, attributes or user commands t-order Order theory
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.