The arithmetic Perron formula

TauCeti.truncatedPerronKernel is the Perron kernel of a single ratio x. This file applies it to an absolutely convergent L-series: the integral over the truncated segment of the series against the Perron integrand is the series of the individual kernels, one for each x / n.

Main results

• TauCeti.integral_LSeries_mul_perronIntegrand: the interchange of the integral with the series.
• TauCeti.truncatedPerron_LSeries: the truncated summatory formula, as a series of truncated Perron kernels at the ratios x / n.
• TauCeti.norm_truncatedPerron_LSeries_sub_sum_le: the off-norm form, comparing the truncated integral with the sharp partial sum ∑_{n < x} f n.
• TauCeti.tendsto_truncatedPerron_LSeries: the limiting form, at every positive x.
• TauCeti.tsum_mul_perronStep_natCast: the limit at an integer endpoint, where the endpoint enters with the customary half weight f N / 2.
• TauCeti.tendsto_truncatedPerron_LSeries_natCast: that limit read off directly, as the finite sum below N together with f N / 2.

References

• H. Davenport, Multiplicative Number Theory, chapter 17, for Perron's formula and the half weight at an integer endpoint.

theorem TauCeti.integral_LSeries_mul_perronIntegrand {f : ℕ → ℂ} {x c T : ℝ} (hx : 0 < x) (hc : 0 < c) (h : LSeriesSummable f ↑c) : ∫ (t : ℝ) in Set.Ioc (-T) T, (∑' (n : ℕ), LSeries.term f (↑c + ↑t * Complex.I) n) * perronIntegrand x c t = ∑' (n : ℕ), ∫ (t : ℝ) in Set.Ioc (-T) T, LSeries.term f (↑c + ↑t * Complex.I) n * perronIntegrand x c t

The interchange. Where the L-series converges absolutely on the line Re s = c, the integral over the truncated segment of the series times the Perron integrand is the series of the integrals.

theorem TauCeti.term_mul_perronIntegrand {f : ℕ → ℂ} {x c : ℝ} (hx : 0 ≤ x) (hc : c ≠ 0) (n : ℕ) (t : ℝ) : LSeries.term f (↑c + ↑t * Complex.I) n * perronIntegrand x c t = f n * perronIntegrand (x / ↑n) c t

Collecting a term into the integrand. The n-th L-series term against the Perron integrand at x is the coefficient f n against the Perron integrand at the ratio x / n.

theorem TauCeti.truncatedPerron_LSeries {f : ℕ → ℂ} {x c T : ℝ} (hx : 0 < x) (hc : 0 < c) (hT : 0 ≤ T) (h : LSeriesSummable f ↑c) : (↑(2 * Real.pi))⁻¹ * ∫ (t : ℝ) in -T..T, LSeries f (↑c + ↑t * Complex.I) * perronIntegrand x c t = ∑' (n : ℕ), f n * truncatedPerronKernel (x / ↑n) c T

The truncated Perron formula for an L-series. Where the series converges absolutely on the line Re s = c, the truncated Perron integral of the series is the series of the truncated Perron kernels at the ratios x / n.

theorem TauCeti.tsum_mul_perronStep_div {x : ℝ} (f : ℕ → ℂ) (hoff : ∀ (n : ℕ), f n ≠ 0 → x ≠ ↑n) : ∑' (n : ℕ), f n * perronStep (x / ↑n) = ∑ n ∈ Finset.Ico 1 ⌈x⌉₊, f n

The Perron step series is a sharp partial sum. When x is not a natural number at which f is nonzero, the step weights are 1 at the indices below x and 0 at those above it, so only n < x contributes.

theorem TauCeti.norm_truncatedPerron_LSeries_sub_sum_le {f : ℕ → ℂ} {x c T : ℝ} (hx : 0 < x) (hc : 0 < c) (hT : 0 < T) (hoff : ∀ (n : ℕ), f n ≠ 0 → x ≠ ↑n) (h : LSeriesSummable f ↑c) : ‖((↑(2 * Real.pi))⁻¹ * ∫ (t : ℝ) in -T..T, LSeries f (↑c + ↑t * Complex.I) * perronIntegrand x c t) - ∑ n ∈ Finset.Ico 1 ⌈x⌉₊, f n‖ ≤ ∑' (n : ℕ), ‖f n‖ * ((x / ↑n) ^ c / (Real.pi * T * |Real.log (x / ↑n)|))

The off-norm arithmetic Perron formula. When x is not a natural number at which f is nonzero, the truncated integral differs from the sharp partial sum ∑_{n < x} f n by at most the series of the smoothed-step kernel errors, a series that absolute convergence on the line makes summable.

theorem TauCeti.tendsto_truncatedPerron_LSeries {f : ℕ → ℂ} {x c : ℝ} (hx : 0 < x) (hc : 0 < c) (h : LSeriesSummable f ↑c) : Filter.Tendsto (fun (T : ℝ) => (↑(2 * Real.pi))⁻¹ * ∫ (t : ℝ) in -T..T, LSeries f (↑c + ↑t * Complex.I) * perronIntegrand x c t) Filter.atTop (nhds (∑' (n : ℕ), f n * perronStep (x / ↑n)))

The limiting arithmetic Perron formula. As the truncation height grows the integral tends to the series of sharp steps ∑' n, f n * perronStep (x / n). This holds at every positive x, integer endpoints included; TauCeti.tsum_mul_perronStep_natCast evaluates the limit there.

theorem TauCeti.tsum_mul_perronStep_natCast {N : ℕ} (hN : 0 < N) (f : ℕ → ℂ) : ∑' (n : ℕ), f n * perronStep (↑N / ↑n) = ∑ n ∈ Finset.Ico 1 N, f n + f N / 2

The half weight at an integer endpoint. At x = N the step series is the partial sum below N together with the customary half of the endpoint term.

theorem TauCeti.tendsto_truncatedPerron_LSeries_natCast {f : ℕ → ℂ} {c : ℝ} {N : ℕ} (hN : 0 < N) (hc : 0 < c) (h : LSeriesSummable f ↑c) : Filter.Tendsto (fun (T : ℝ) => (↑(2 * Real.pi))⁻¹ * ∫ (t : ℝ) in -T..T, LSeries f (↑c + ↑t * Complex.I) * perronIntegrand (↑N) c t) Filter.atTop (nhds (∑ n ∈ Finset.Ico 1 N, f n + f N / 2))

The arithmetic Perron formula at an integer endpoint. At x = N the truncated integral tends to the sum of f below N together with half of the endpoint term.