Analytic continuation of an L-series from a bound on its partial sums

If the partial sums A(n) = ∑_{k=1}^n f k of a sequence f : ℕ → ℂ are O(n ^ r), Mathlib's LSeries_eq_mul_integral (from Mathlib/NumberTheory/LSeries/SumCoeff.lean) writes the L-series of f as

LSeries f s = s * ∫ t in Set.Ioi 1, A(⌊t⌋₊) * t ^ (-(s + 1))

wherever LSeries f converges and r < Re s. The right-hand side makes sense on the whole half-plane r < Re s, independently of the convergence of the series, and this file proves that it is holomorphic there: it is s times the Mellin transform of the step function t ↦ A(⌊t⌋₊) at -s, and Mathlib's mellin_differentiableAt_of_isBigO_rpow applies because the step function vanishes on (0, 1) and is O(t ^ r) at infinity.

Together the two statements continue LSeries f analytically from its half-plane of convergence to Re s > r; this is the classical continuation of a Dirichlet series with cancelling coefficients by partial summation (see e.g. Tenenbaum, Introduction to Analytic and Probabilistic Number Theory, Chapter II.1).

Main results

• TauCeti.LSeries.differentiableOn_mul_integral_of_isBigO: under the bound A(n) = O(n ^ r), the function s ↦ s * ∫ t in Set.Ioi 1, A(⌊t⌋₊) * t ^ (-(s + 1)) is complex-differentiable on {s | r < s.re}.

theorem TauCeti.LSeries.differentiableOn_mul_integral_of_isBigO (f : ℕ → ℂ) {r : ℝ} (hO : (fun (n : ℕ) => ∑ k ∈ Finset.Icc 1 n, f k) =O[Filter.atTop] fun (n : ℕ) => ↑n ^ r) : DifferentiableOn ℂ (fun (s : ℂ) => s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Finset.Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))) {s : ℂ | r < s.re}

Holomorphy of the partial-summation integral. If the partial sums ∑ k ∈ Icc 1 n, f k are O(n ^ r), then s ↦ s * ∫ t in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * t ^ (-(s + 1)) is complex-differentiable on the half-plane r < Re s.

By Mathlib's LSeries_eq_mul_integral this function agrees with LSeries f wherever the series converges in that half-plane, so it is an analytic continuation of LSeries f to Re s > r.