[Merged by Bors] - feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 2)#20660
[Merged by Bors] - feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 2)#20660
Conversation
PR summary dd85552035Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
…ients (part 1) (#20661) We prove several results involving partial sums of coefficients (or norm of coefficients) of L-series. The two main results of this PR are: - `LSeriesSummable_of_sum_norm_bigO`: for `f : ℕ → ℂ`, if the partial sums `∑ k ∈ Icc 1 n, ‖f k‖` are `O(n ^ r)` for some real `0 ≤ r`, then the L-series `Lseries f` converges at `s : ℂ` for all `s` such that `r < s.re`. - `LSeries_eq_mul_integral` : for `f : ℕ → ℂ`, if the partial sums `∑ k ∈ Icc 1 n, f k` are `O(n ^ r)` for some real `0 ≤ r` and the L-series `LSeries f` converges at `s : ℂ` with `r < s.re`, then `LSeries f s = s * ∫ t in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * t ^ (- (s + 1))`. More results will be proved in #20660
loefflerd
left a comment
There was a problem hiding this comment.
Hi Xavier,
I won't have time to actually try compiling this and experimenting with it for a day or two, so here are some stylistic comments based only on reading the code on github.
Thanks for the first comments. Don't worry, there is no need to hurry. |
loefflerd
left a comment
There was a problem hiding this comment.
Here are some more detailed ocmments on the first half (up to line 250 of the main file)
loefflerd
left a comment
There was a problem hiding this comment.
Here are some further comments. All my remarks are quite "localised", I'm completely happy with the general strategy. I've just tried to suggest a few places where more automated tactics can be used; this is slower, but makes things less likely to break in future.
(It's a pity the automated tactics can't do more; it would be nice if linarith could see through the definition of Set.Icc etc. But I'm no expert on tactic hacking so I don't know how easy or hard that is.)
…f' into xfr_lseries_sumcoeff
loefflerd
left a comment
There was a problem hiding this comment.
Looks good to me now, thanks!
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by loefflerd. |
|
Thanks! bors merge |
…ients (part 2) (#20660) We prove the following result : if `f : ℕ → ℂ` is such that `(∑ k ∈ Icc 1 n, f k) / n` tends to some complex number `l` when `n → ∞` and that the L-series `LSeries f` converges for all `s : ℝ` such that `1 < s`, then `(s - 1) * LSeries f s` tends to `l` when `s → 1` with `1 < s`. Co-authored-by: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
We prove the following result : if
f : ℕ → ℂis such that(∑ k ∈ Icc 1 n, f k) / ntends to some complex numberlwhenn → ∞and that the L-seriesLSeries fconverges for alls : ℝsuch that1 < s, then(s - 1) * LSeries f stends tolwhens → 1with1 < s.protectedto results that already exists in root namespace #21454