Commit 2025-01-27 10:18 c33fe046

feat(NumberTheory/LSeries): results involving partial sums of coefficients (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