Skip to content

[Merged by Bors] - feat: Positivity extension for Finset.sum#10538

Closed
YaelDillies wants to merge 25 commits intomasterfrom
positivity_finset_prod
Closed

[Merged by Bors] - feat: Positivity extension for Finset.sum#10538
YaelDillies wants to merge 25 commits intomasterfrom
positivity_finset_prod

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Feb 14, 2024 •
edited
Loading

Also define a new aesop rule-set and an auxiliary metaprogram proveFinsetNonempty for dealing with Finset.Nonempty conditions.

From LeanAPAP

Co-authored-by: Alex J. Best alex.j.best@gmail.com

Open in Gitpod

YaelDillies and others added 12 commits December 30, 2023 22:35
@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 <alex.j.best@gmail.com>
@YaelDillies
remove unused instance synthesis
eb70e94
@YaelDillies
golf downstream
5aa5b0e
@eric-wieser
hack
e964bfd
@alexjbest
beta expand if needed
695ea52
@eric-wieser
Merge remote-tracking branch 'origin/master' into positivity_finset_sum
ca61d08
@eric-wieser
simplify logic
c3d02ea
@YaelDillies
better logic
738c7cc
@YaelDillies
check for debug
4c0225b
@eric-wieser
fix
2285697
@YaelDillies
remove unreachable failure
d7456a3
@YaelDillies
add todo
6161d23
@YaelDillies YaelDillies added awaiting-review blocked-by-core-PR This PR depends on a PR to Core/Std t-algebra Algebra (groups, rings, fields, etc) t-order Order theory labels Feb 14, 2024
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 14, 2024
@YaelDillies YaelDillies mentioned this pull request Feb 14, 2024
Closed
2 tasks
@YaelDillies YaelDillies force-pushed the positivity_finset_prod branch from 72d04bd to 300250c Compare February 14, 2024 20:35
eric-wieser
eric-wieser reviewed Feb 14, 2024
View reviewed changes
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Feb 14, 2024

I think you've marked the dependency backwards?

eric-wieser
eric-wieser reviewed Feb 14, 2024
View reviewed changes
eric-wieser
eric-wieser reviewed Feb 14, 2024
View reviewed changes
@YaelDillies YaelDillies removed the blocked-by-core-PR This PR depends on a PR to Core/Std label Feb 15, 2024
@YaelDillies YaelDillies changed the title feat: Positivity extension for Finset.prod feat: Positivity extension for Finset.sum Feb 15, 2024
@YaelDillies YaelDillies removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 15, 2024
YaelDillies and others added 2 commits February 17, 2024 10:07
@YaelDillies @Vierkantor
option failure, not monadic failure
c0e9c37 
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@YaelDillies
revert
bcddd3f
@mcdoll mcdoll mentioned this pull request Feb 17, 2024
Closed
YaelDillies and others added 2 commits February 18, 2024 14:51
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 19, 2024
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 20, 2024
@Vierkantor
Copy link
Copy Markdown
Contributor

Vierkantor commented Feb 20, 2024

@eric-wieser can I ping you to take a look again?

jcommelin
jcommelin approved these changes Feb 22, 2024
View reviewed changes
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

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Feb 22, 2024
mathlib-bors bot pushed a commit that referenced this pull request Feb 22, 2024
@YaelDillies @eric-wieser @alexjbest
feat: Positivity extension for Finset.sum (#10538)
f2d8a00 
Also define a new `aesop` rule-set and an auxiliary metaprogram `proveFinsetNonempty` for dealing with `Finset.Nonempty` conditions.

From LeanAPAP

Co-authored-by: Alex J. Best <alex.j.best@gmail.com>



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Alex J Best <alex.j.best@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 22, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: Positivity extension for Finset.sum [Merged by Bors] - feat: Positivity extension for Finset.sum Feb 22, 2024
@mathlib-bors mathlib-bors bot closed this Feb 22, 2024
@mathlib-bors mathlib-bors bot deleted the positivity_finset_prod branch February 22, 2024 14:00
thorimur pushed a commit that referenced this pull request Feb 24, 2024
@YaelDillies @eric-wieser
@alexjbest @thorimur
feat: Positivity extension for Finset.sum (#10538)
10dbf97 
Also define a new `aesop` rule-set and an auxiliary metaprogram `proveFinsetNonempty` for dealing with `Finset.Nonempty` conditions.

From LeanAPAP

Co-authored-by: Alex J. Best <alex.j.best@gmail.com>



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Alex J Best <alex.j.best@gmail.com>
thorimur pushed a commit that referenced this pull request Feb 26, 2024
@YaelDillies @eric-wieser
@alexjbest @thorimur
feat: Positivity extension for Finset.sum (#10538)
d791177 
Also define a new `aesop` rule-set and an auxiliary metaprogram `proveFinsetNonempty` for dealing with `Finset.Nonempty` conditions.

From LeanAPAP

Co-authored-by: Alex J. Best <alex.j.best@gmail.com>



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Alex J Best <alex.j.best@gmail.com>
riccardobrasca pushed a commit that referenced this pull request Mar 1, 2024
@YaelDillies @eric-wieser
@alexjbest @riccardobrasca
feat: Positivity extension for Finset.sum (#10538)
ca9016d 
Also define a new `aesop` rule-set and an auxiliary metaprogram `proveFinsetNonempty` for dealing with `Finset.Nonempty` conditions.

From LeanAPAP

Co-authored-by: Alex J. Best <alex.j.best@gmail.com>



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Alex J Best <alex.j.best@gmail.com>
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
@YaelDillies @eric-wieser
@alexjbest @dagurtomas
feat: Positivity extension for Finset.sum (#10538)
f9696cb 
Also define a new `aesop` rule-set and an auxiliary metaprogram `proveFinsetNonempty` for dealing with `Finset.Nonempty` conditions.

From LeanAPAP

Co-authored-by: Alex J. Best <alex.j.best@gmail.com>



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Alex J Best <alex.j.best@gmail.com>
mathlib-bors bot pushed a commit that referenced this pull request Mar 22, 2024
@mcdoll
feat: Positivity extension for Bochner integral (#10661)
9025876 
Inspired by #10538 add a positivity extension for Bochner integrals.
mathlib-bors bot pushed a commit that referenced this pull request Mar 23, 2024
@mcdoll
feat: Positivity extension for Bochner integral (#10661)
2e4644e 
Inspired by #10538 add a positivity extension for Bochner integrals.
mathlib-bors bot pushed a commit that referenced this pull request Mar 23, 2024
@mcdoll
feat: Positivity extension for Bochner integral (#10661)
8b3fbc9 
Inspired by #10538 add a positivity extension for Bochner integrals.
utensil pushed a commit that referenced this pull request Mar 26, 2024
@mcdoll @utensil
feat: Positivity extension for Bochner integral (#10661)
7b2b40c 
Inspired by #10538 add a positivity extension for Bochner integrals.
xgenereux pushed a commit that referenced this pull request Apr 15, 2024
@YaelDillies @eric-wieser
@alexjbest @xgenereux
feat: Positivity extension for Finset.sum (#10538)
6ca6ab7 
Also define a new `aesop` rule-set and an auxiliary metaprogram `proveFinsetNonempty` for dealing with `Finset.Nonempty` conditions.

From LeanAPAP

Co-authored-by: Alex J. Best <alex.j.best@gmail.com>



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Alex J Best <alex.j.best@gmail.com>
xgenereux pushed a commit that referenced this pull request Apr 15, 2024
@mcdoll @xgenereux
feat: Positivity extension for Bochner integral (#10661)
75b5521 
Inspired by #10538 add a positivity extension for Bochner integrals.
atarnoam pushed a commit that referenced this pull request Apr 16, 2024
@mcdoll @atarnoam
feat: Positivity extension for Bochner integral (#10661)
cb5e5fb 
Inspired by #10538 add a positivity extension for Bochner integrals.
uniwuni pushed a commit that referenced this pull request Apr 19, 2024
@mcdoll @uniwuni
feat: Positivity extension for Bochner integral (#10661)
0d17895 
Inspired by #10538 add a positivity extension for Bochner integrals.
callesonne pushed a commit that referenced this pull request Apr 22, 2024
@mcdoll @callesonne
feat: Positivity extension for Bochner integral (#10661)
611a64b 
Inspired by #10538 add a positivity extension for Bochner integrals.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

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

@Vierkantor Vierkantor Vierkantor approved these changes

@jcommelin jcommelin jcommelin approved these changes

Assignees

@Vierkantor Vierkantor

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. 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.

5 participants

@YaelDillies @eric-wieser @Vierkantor @jcommelin @alexjbest