[Merged by Bors] - feat(Topology/Algebra/InfiniteSum/Real): Add partition lemma by CBirkbeck · Pull Request #12446 · leanprover-community/mathlib4

CBirkbeck · 2024-04-26T10:07:12Z

We also summable_partition (and the required Set.sigmaEquiv), needed for #10377.

Ignore the typo in the PR name!

depends on: [Merged by Bors] - chore: move summable lemmas #12503

…rover-community/mathlib4 into CB_summable_partion_lemmas

grunweg

I can confirm that this PR is almost only code motion, replacing a proof by a commented more elegant version and two new declarations.

This PR would be easier to review if you split the move from the new code: I approve the code motion/porting TODO parts (but didn't scrutinize the others carefully).

Mathlib/Topology/Algebra/InfiniteSum/Real.lean

Mathlib/Topology/Instances/ENNReal.lean

CBirkbeck · 2024-04-29T08:44:45Z

OK I split this into two PRs. The code moving is now #12503. Once that goes in this will only have the two new results.

adomani · 2024-04-29T22:08:50Z

Again, the no_lost_declarations script reports

+ lemma summable_partition {κ ι: Type*} {f : ι → ℝ} (hf : 0 ≤ f) {s : κ → Set ι}

1 added declarations
0 removed declarations
9 paired declarations

We move some lemmas out of `Topology/Instances/ENNReal` into `Topology/Algebra/InfiniteSum/Real`. Also use this to address a porting TODO. This was originally part of #12446 Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>

loefflerd · 2024-04-30T16:32:16Z

This needs a rebase now #12503 is in, please feel free to ping me for a review once you've merged master

…_lemmas

Mathlib/Data/Set/Lattice.lean

Mathlib/Topology/Algebra/InfiniteSum/Real.lean

Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>

Mathlib/Data/Set/Lattice.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

loefflerd · 2024-05-02T16:24:37Z

LGTM, thanks!

maintainer merge

github-actions · 2024-05-02T16:24:48Z

🚀 Pull request has been placed on the maintainer queue by loefflerd.

ghost · 2024-05-03T08:21:23Z

This PR/issue depends on:

~~[Merged by Bors] - chore: move summable lemmas #12503~~
By Dependent Issues (🤖). Happy coding!

riccardobrasca · 2024-05-03T08:33:10Z

This is very small and I think we can just merge it, but if you start using partition a lot (meaning (s : κ → Set ι) (hs : ∀ i, ∃! j, i ∈ s j) we probably want a small API, but we will see. Thanks!

bors merge

We also `summable_partition` (and the required `Set.sigmaEquiv`), needed for #10377. Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>

CBirkbeck · 2024-05-03T08:35:32Z

This is very small and I think we can just merge it, but if you start using partition a lot (meaning (s : κ → Set ι) (hs : ∀ i, ∃! j, i ∈ s j) we probably want a small API, but we will see. Thanks!

Yeah I don't know how much it'll be used for example for the stuff Yael wanted the Finest.box for. But yes we can add more API if needed.

mathlib-bors · 2024-05-03T09:44:54Z

Pull request successfully merged into master.

Build succeeded:

We move some lemmas out of `Topology/Instances/ENNReal` into `Topology/Algebra/InfiniteSum/Real`. Also use this to address a porting TODO. This was originally part of #12446 Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>

We also `summable_partition` (and the required `Set.sigmaEquiv`), needed for #10377. Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>

We move some lemmas out of `Topology/Instances/ENNReal` into `Topology/Algebra/InfiniteSum/Real`. Also use this to address a porting TODO. This was originally part of #12446 Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>

We also `summable_partition` (and the required `Set.sigmaEquiv`), needed for #10377. Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>

summable lems move test

61b0056

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Apr 26, 2024

CBirkbeck added WIP Work in progress and removed new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! labels Apr 26, 2024

test2

e5e78c0

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Apr 26, 2024

do todo from port

a8380ae

CBirkbeck added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed WIP Work in progress new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! labels Apr 26, 2024

CBirkbeck mentioned this pull request Apr 26, 2024

[Merged by Bors] - Eisenstein series uniform convergence #10377

Closed

5 tasks

build fix

95f199f

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Apr 26, 2024

CBirkbeck added 2 commits April 26, 2024 13:09

fix

0472942

Merge branch 'CB_summable_partion_lemmas' of https://github.com/leanp…

a5f0f87

…rover-community/mathlib4 into CB_summable_partion_lemmas

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 26, 2024

CBirkbeck removed the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Apr 26, 2024

CBirkbeck changed the title ~~summable lems move test~~ Move/Add some summable lemmas of real valued functions Apr 26, 2024

CBirkbeck requested a review from loefflerd April 26, 2024 13:55

grunweg approved these changes Apr 26, 2024

View reviewed changes

Mathlib/Topology/Algebra/InfiniteSum/Real.lean Outdated Show resolved Hide resolved

Mathlib/Topology/Instances/ENNReal.lean Outdated Show resolved Hide resolved

CBirkbeck mentioned this pull request Apr 29, 2024

[Merged by Bors] - chore: move summable lemmas #12503

Closed

loefflerd added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Apr 30, 2024

Merge remote-tracking branch 'origin/master' into CB_summable_partion…

9c5df81

…_lemmas

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 Apr 30, 2024

CBirkbeck added the awaiting-review label Apr 30, 2024

loefflerd reviewed May 1, 2024

View reviewed changes

Mathlib/Data/Set/Lattice.lean Outdated Show resolved Hide resolved

Mathlib/Topology/Algebra/InfiniteSum/Real.lean Outdated Show resolved Hide resolved

Mathlib/Topology/Algebra/InfiniteSum/Real.lean Outdated Show resolved Hide resolved

loefflerd added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels May 1, 2024

CBirkbeck and others added 2 commits May 1, 2024 19:41

Update Mathlib/Data/Set/Lattice.lean

23df72e

Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>

Update Mathlib/Topology/Algebra/InfiniteSum/Real.lean

b482df9

Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>

github-actions bot reviewed May 1, 2024

View reviewed changes

Mathlib/Data/Set/Lattice.lean Outdated Show resolved Hide resolved

CBirkbeck and others added 2 commits May 1, 2024 19:46

notation fix

6c3bd70

Update Mathlib/Data/Set/Lattice.lean

a460ade

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

CBirkbeck added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels May 1, 2024

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 1, 2024

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 2, 2024

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels May 3, 2024

mathlib-bors bot changed the title ~~feat(Topology/Algebra/InfiniteSum/Real): Add partition lemma~~ [Merged by Bors] - feat(Topology/Algebra/InfiniteSum/Real): Add partition lemma May 3, 2024

mathlib-bors bot closed this May 3, 2024

mathlib-bors bot deleted the CB_summable_partion_lemmas branch May 3, 2024 09:44

apnelson1 pushed a commit that referenced this pull request May 12, 2024

feat(Topology/Algebra/InfiniteSum/Real): Add partition lemma (#12446)

2ae5987

We also `summable_partition` (and the required `Set.sigmaEquiv`), needed for #10377. Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>

callesonne pushed a commit that referenced this pull request May 16, 2024

feat(Topology/Algebra/InfiniteSum/Real): Add partition lemma (#12446)

e194fd3

We also `summable_partition` (and the required `Set.sigmaEquiv`), needed for #10377. Co-authored-by: Chris Birkbeck <c.birkbeck@uea.ac.uk>

Conversation

CBirkbeck commented Apr 26, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

grunweg left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

CBirkbeck commented Apr 29, 2024

Uh oh!

adomani commented Apr 29, 2024

Uh oh!

loefflerd commented Apr 30, 2024

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

loefflerd commented May 2, 2024

Uh oh!

github-actions bot commented May 2, 2024

Uh oh!

ghost commented May 3, 2024

Uh oh!

riccardobrasca commented May 3, 2024

Uh oh!

CBirkbeck commented May 3, 2024

Uh oh!

mathlib-bors bot commented May 3, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

CBirkbeck commented Apr 26, 2024 •

edited

Loading