[Merged by Bors] - feat(InfiniteSum/NatInt): lemmas on sums over ℤ #11069
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
loefflerd
changed the title
|
When you want a review, please add the awaiting-review label |
loefflerd
added
WIP
loefflerd
added
awaiting-review
This was referenced Mar 4, 2024
loefflerd
force-pushed
the
DL_nat_int_sums
branch
from
dcc991f
to
d4f8fe1
Compare
2 tasks
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
removed
the
merge-conflict
MichaelStollBayreuth
approved these changes
Mar 9, 2024
loefflerd
added
the
t-topology
sgouezel
added
awaiting-author
loefflerd
added
awaiting-review
|
bors r+ |
github-actions
bot
added
ready-to-merge
mathlib-bors bot
pushed a commit
that referenced
this pull request
Mar 16, 2024
This PR combines several results involving topological sums over `ℤ`. These results are used in #10011 (Hurwitz zeta functions) where sums over `ℤ` feature heavily. * Fill in `tsum` and `Summable` variants for lemmas proved for `HasSum` * Rename some lemmas (with deprecated aliases) to impose a consistent naming scheme * Generalise several lemmas to allow the target space to be a topological monoid rather than a group. * Speed up some slow proofs (the old `summable_int_of_summable_nat` took about 10s to compile on my machine, its replacement `Summable.of_nat_of_neg` is 1000 times faster)
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
dagurtomas
pushed a commit
that referenced
this pull request
Mar 22, 2024
This PR combines several results involving topological sums over `ℤ`. These results are used in #10011 (Hurwitz zeta functions) where sums over `ℤ` feature heavily. * Fill in `tsum` and `Summable` variants for lemmas proved for `HasSum` * Rename some lemmas (with deprecated aliases) to impose a consistent naming scheme * Generalise several lemmas to allow the target space to be a topological monoid rather than a group. * Speed up some slow proofs (the old `summable_int_of_summable_nat` took about 10s to compile on my machine, its replacement `Summable.of_nat_of_neg` is 1000 times faster)
utensil
pushed a commit
that referenced
this pull request
Mar 26, 2024
This PR combines several results involving topological sums over `ℤ`. These results are used in #10011 (Hurwitz zeta functions) where sums over `ℤ` feature heavily. * Fill in `tsum` and `Summable` variants for lemmas proved for `HasSum` * Rename some lemmas (with deprecated aliases) to impose a consistent naming scheme * Generalise several lemmas to allow the target space to be a topological monoid rather than a group. * Speed up some slow proofs (the old `summable_int_of_summable_nat` took about 10s to compile on my machine, its replacement `Summable.of_nat_of_neg` is 1000 times faster)
Louddy
pushed a commit
that referenced
this pull request
Apr 15, 2024
This PR combines several results involving topological sums over `ℤ`. These results are used in #10011 (Hurwitz zeta functions) where sums over `ℤ` feature heavily. * Fill in `tsum` and `Summable` variants for lemmas proved for `HasSum` * Rename some lemmas (with deprecated aliases) to impose a consistent naming scheme * Generalise several lemmas to allow the target space to be a topological monoid rather than a group. * Speed up some slow proofs (the old `summable_int_of_summable_nat` took about 10s to compile on my machine, its replacement `Summable.of_nat_of_neg` is 1000 times faster)
atarnoam
pushed a commit
that referenced
this pull request
Apr 16, 2024
This PR combines several results involving topological sums over `ℤ`. These results are used in #10011 (Hurwitz zeta functions) where sums over `ℤ` feature heavily. * Fill in `tsum` and `Summable` variants for lemmas proved for `HasSum` * Rename some lemmas (with deprecated aliases) to impose a consistent naming scheme * Generalise several lemmas to allow the target space to be a topological monoid rather than a group. * Speed up some slow proofs (the old `summable_int_of_summable_nat` took about 10s to compile on my machine, its replacement `Summable.of_nat_of_neg` is 1000 times faster)
uniwuni
pushed a commit
that referenced
this pull request
Apr 19, 2024
This PR combines several results involving topological sums over `ℤ`. These results are used in #10011 (Hurwitz zeta functions) where sums over `ℤ` feature heavily. * Fill in `tsum` and `Summable` variants for lemmas proved for `HasSum` * Rename some lemmas (with deprecated aliases) to impose a consistent naming scheme * Generalise several lemmas to allow the target space to be a topological monoid rather than a group. * Speed up some slow proofs (the old `summable_int_of_summable_nat` took about 10s to compile on my machine, its replacement `Summable.of_nat_of_neg` is 1000 times faster)
callesonne
pushed a commit
that referenced
this pull request
Apr 22, 2024
This PR combines several results involving topological sums over `ℤ`. These results are used in #10011 (Hurwitz zeta functions) where sums over `ℤ` feature heavily. * Fill in `tsum` and `Summable` variants for lemmas proved for `HasSum` * Rename some lemmas (with deprecated aliases) to impose a consistent naming scheme * Generalise several lemmas to allow the target space to be a topological monoid rather than a group. * Speed up some slow proofs (the old `summable_int_of_summable_nat` took about 10s to compile on my machine, its replacement `Summable.of_nat_of_neg` is 1000 times faster)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR combines several results involving topological sums over
ℤ. These results are used in #10011 (Hurwitz zeta functions) where sums overℤfeature heavily.Fill in
tsumandSummablevariants for lemmas proved forHasSumRename some lemmas (with deprecated aliases) to impose a consistent naming scheme
Generalise several lemmas to allow the target space to be a topological monoid rather than a group.
Speed up some slow proofs (the old
summable_int_of_summable_nattook about 10s to compile on my machine, its replacementSummable.of_nat_of_negis 1000 times faster)