[Merged by Bors] - feat(NumberTheory/EulerProduct/Basic): use infinite products, golf #12161
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
MichaelStollBayreuth
added
awaiting-review
|
!bench |
|
Here are the benchmark results for commit 33b2a2b. |
|
Mathlib.NumberTheory.EulerProduct.Basic instructions: 12,643 Mrd. -1,52 Mrd. -12,023 % 11,123 Mrd. |
loefflerd
reviewed
Apr 16, 2024
loefflerd
added
awaiting-author
Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
loefflerd
approved these changes
Apr 17, 2024
|
🚀 Pull request has been placed on the maintainer queue by loefflerd. |
MichaelStollBayreuth
added
awaiting-review
|
Thanks! bors merge |
github-actions
bot
added
ready-to-merge
mathlib-bors bot
pushed a commit
that referenced
this pull request
Apr 18, 2024
…12161) This adds versions of the various Euler product statements in terms of the new topological products, namely `HasProd (fun p : Primes ↦ ∑' e, f (p ^ e)) (∑' n, f n)` and `∏' p : Primes, ∑' e, f (p ^ e) = ∑' n, f n` (and similar for completely multiplicative `f` in terms of `(1 - f p)⁻¹`). At the same time, I have reworked the proofs to some extent (in particular removing a few slow `convert`s). I also added a bunch of local instances that speed up instance synthesis by a factor of 2 (from 1.4 to 0.7 seconds on my laptop). Unfortunately, this means that the diff is fairly large. See [here](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/432666616) and [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Infinite.20products/near/431508883) on Zulip. Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>
|
Build failed (retrying...): |
|
Re-adding to the queue: |
|
Canceled. |
|
bors r+ |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Apr 18, 2024
…12161) This adds versions of the various Euler product statements in terms of the new topological products, namely `HasProd (fun p : Primes ↦ ∑' e, f (p ^ e)) (∑' n, f n)` and `∏' p : Primes, ∑' e, f (p ^ e) = ∑' n, f n` (and similar for completely multiplicative `f` in terms of `(1 - f p)⁻¹`). At the same time, I have reworked the proofs to some extent (in particular removing a few slow `convert`s). I also added a bunch of local instances that speed up instance synthesis by a factor of 2 (from 1.4 to 0.7 seconds on my laptop). Unfortunately, this means that the diff is fairly large. See [here](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/432666616) and [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Infinite.20products/near/431508883) on Zulip. Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>
|
Build failed (retrying...): |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Apr 18, 2024
…12161) This adds versions of the various Euler product statements in terms of the new topological products, namely `HasProd (fun p : Primes ↦ ∑' e, f (p ^ e)) (∑' n, f n)` and `∏' p : Primes, ∑' e, f (p ^ e) = ∑' n, f n` (and similar for completely multiplicative `f` in terms of `(1 - f p)⁻¹`). At the same time, I have reworked the proofs to some extent (in particular removing a few slow `convert`s). I also added a bunch of local instances that speed up instance synthesis by a factor of 2 (from 1.4 to 0.7 seconds on my laptop). Unfortunately, this means that the diff is fairly large. See [here](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/432666616) and [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Infinite.20products/near/431508883) on Zulip. Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
uniwuni
pushed a commit
that referenced
this pull request
Apr 19, 2024
…12161) This adds versions of the various Euler product statements in terms of the new topological products, namely `HasProd (fun p : Primes ↦ ∑' e, f (p ^ e)) (∑' n, f n)` and `∏' p : Primes, ∑' e, f (p ^ e) = ∑' n, f n` (and similar for completely multiplicative `f` in terms of `(1 - f p)⁻¹`). At the same time, I have reworked the proofs to some extent (in particular removing a few slow `convert`s). I also added a bunch of local instances that speed up instance synthesis by a factor of 2 (from 1.4 to 0.7 seconds on my laptop). Unfortunately, this means that the diff is fairly large. See [here](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/432666616) and [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Infinite.20products/near/431508883) on Zulip. Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>
callesonne
pushed a commit
that referenced
this pull request
Apr 22, 2024
…12161) This adds versions of the various Euler product statements in terms of the new topological products, namely `HasProd (fun p : Primes ↦ ∑' e, f (p ^ e)) (∑' n, f n)` and `∏' p : Primes, ∑' e, f (p ^ e) = ∑' n, f n` (and similar for completely multiplicative `f` in terms of `(1 - f p)⁻¹`). At the same time, I have reworked the proofs to some extent (in particular removing a few slow `convert`s). I also added a bunch of local instances that speed up instance synthesis by a factor of 2 (from 1.4 to 0.7 seconds on my laptop). Unfortunately, this means that the diff is fairly large. See [here](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/432666616) and [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Infinite.20products/near/431508883) on Zulip. Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>
Jun2M
pushed a commit
that referenced
this pull request
Apr 24, 2024
…12161) This adds versions of the various Euler product statements in terms of the new topological products, namely `HasProd (fun p : Primes ↦ ∑' e, f (p ^ e)) (∑' n, f n)` and `∏' p : Primes, ∑' e, f (p ^ e) = ∑' n, f n` (and similar for completely multiplicative `f` in terms of `(1 - f p)⁻¹`). At the same time, I have reworked the proofs to some extent (in particular removing a few slow `convert`s). I also added a bunch of local instances that speed up instance synthesis by a factor of 2 (from 1.4 to 0.7 seconds on my laptop). Unfortunately, this means that the diff is fairly large. See [here](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/432666616) and [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Infinite.20products/near/431508883) on Zulip. Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>
mathlib-bors bot
pushed a commit
that referenced
this pull request
May 17, 2024
…t and L-series (#12809) This is a follow-up to [#12161](#12161). It adds `HasProd` and `tsum` versions of the Euler Product statements for the Riemann zeta function and Dirichlet L-series (in the latter case, also replacing the explicit infinite sum by `L ↗χ s`). See [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/L-series/near/438037266).
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 adds versions of the various Euler product statements in terms of the new topological products, namely
HasProd (fun p : Primes ↦ ∑' e, f (p ^ e)) (∑' n, f n)and∏' p : Primes, ∑' e, f (p ^ e) = ∑' n, f n(and similar for completely multiplicativefin terms of(1 - f p)⁻¹).At the same time, I have reworked the proofs to some extent (in particular removing a few slow
converts). I also added a bunch of local instances that speed up instance synthesis by a factor of 2 (from 1.4 to 0.7 seconds on my laptop).Unfortunately, this means that the diff is fairly large.
See here and here on Zulip.