Partial sums of coefficients of L-series

We prove several results involving partial sums of coefficients (or norm of coefficients) of L-series.

Main results

• 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)).

• LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div : assume that f : ℕ → ℂ satisfies 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.

theorem LSeriesSummable_of_sum_norm_bigO {f : ℕ → ℂ} {r : ℝ} {s : ℂ} (hO : (fun (n : ℕ) => ∑ k ∈ Finset.Icc 1 n, ‖f k‖) =O[Filter.atTop] fun (n : ℕ) => ↑n ^ r) (hr : 0 ≤ r) (hs : r < s.re) : LSeriesSummable f s

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.

theorem LSeriesSummable_of_sum_norm_bigO_and_nonneg {r : ℝ} {s : ℂ} {f : ℕ → ℝ} (hO : (fun (n : ℕ) => ∑ k ∈ Finset.Icc 1 n, f k) =O[Filter.atTop] fun (n : ℕ) => ↑n ^ r) (hf : ∀ (n : ℕ), 0 ≤ f n) (hr : 0 ≤ r) (hs : r < s.re) : LSeriesSummable (fun (n : ℕ) => ↑(f n)) s

If f takes nonnegative real values and 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.

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

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)).

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

A version of LSeries_eq_mul_integral where we use the stronger condition that the partial sums ∑ k ∈ Icc 1 n, ‖f k‖ are O(n ^ r) to deduce the integral representation.

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

If f takes nonnegative real values and the partial sums ∑ k ∈ Icc 1 n, f k are O(n ^ r) for some real 0 ≤ r, then for s : ℂ with r < s.re, we have LSeries f s = s * ∫ t in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * t ^ (-(s + 1)).

theorem LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div {f : ℕ → ℂ} {l : ℂ} (hlim : Filter.Tendsto (fun (n : ℕ) => (∑ k ∈ Finset.Icc 1 n, f k) / ↑n) Filter.atTop (nhds l)) (hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s) : Filter.Tendsto (fun (s : ℝ) => (↑s - 1) * LSeries f ↑s) (nhdsWithin 1 (Set.Ioi 1)) (nhds l)

theorem LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_and_nonneg (f : ℕ → ℝ) {l : ℝ} (hf : Filter.Tendsto (fun (n : ℕ) => (∑ k ∈ Finset.Icc 1 n, f k) / ↑n) Filter.atTop (nhds l)) (hf' : ∀ (n : ℕ), 0 ≤ f n) : Filter.Tendsto (fun (s : ℝ) => (↑s - 1) * LSeries (fun (n : ℕ) => ↑(f n)) ↑s) (nhdsWithin 1 (Set.Ioi 1)) (nhds ↑l)