The step correction of a bounded Dirichlet series

For coefficients a : ℕ → ℂ, the step function t ↦ a ⌊exp t⌋₊ has, at least formally, Laplace transform ∑ n ≥ 1, a n ∫ x in n..n+1, x ^ (-z - 1). Comparing each integral with the value n ^ (-z - 1) at the left endpoint, this differs from the shifted Dirichlet series ∑ n ≥ 1, a n n ^ (-z - 1) by the step correction H z = ∑ n ≥ 1, a n (∫ x in n..n+1, x ^ (-z - 1) - n ^ (-z - 1)).

When a is bounded, the Dirichlet series is only guaranteed to converge absolutely for re z > 0, whereas the step correction is guaranteed to be holomorphic on the larger half-plane -1 < re z: by the mean value theorem its n-th term is at most ‖a n‖ ‖z + 1‖ n ^ (-re z - 2). This is what lets the bounded-Laplace (Newman) Tauberian theorem for the step function transfer to ordered partial sums ∑ n ≤ N, a n / n of the Dirichlet series at s = 1, where the step correction takes the absolutely convergent value ∑ n ≥ 1, a n (log (1 + 1 / n) - 1 / n).

Main declarations

• TauCeti.LSeries.stepCorrectionTerm a n z: the n-th term of the step correction, zero for n = 0;
• TauCeti.LSeries.stepCorrection a z: the step correction H z;
• TauCeti.LSeries.norm_stepCorrectionTerm_le: the mean value bound on the terms;
• TauCeti.LSeries.hasSum_stepCorrection: absolute convergence for -1 < re z;
• TauCeti.LSeries.differentiableOn_stepCorrection: holomorphy on -1 < re z;
• TauCeti.LSeries.stepCorrection_zero: the value ∑ a n (log (1 + 1 / n) - 1 / n) at 0.

References

• D. J. Newman, Simple analytic proof of the prime number theorem, Amer. Math. Monthly 87 (1980), 693–696.
• D. Zagier, Newman's short proof of the prime number theorem, Amer. Math. Monthly 104 (1997), 705–708.

noncomputable def TauCeti.LSeries.stepCorrectionTerm (a : ℕ → ℂ) (n : ℕ) (z : ℂ) : ℂ

The n-th term of the step correction of the coefficients a at z: it is 0 for n = 0, and otherwise a n * (∫ x in n..n+1, x ^ (-z - 1) - n ^ (-z - 1)), the difference between the contribution of the step [n, n + 1) to the Laplace transform of t ↦ a ⌊exp t⌋₊ and the n-th term of the Dirichlet series of a at z + 1.

noncomputable def TauCeti.LSeries.stepCorrection (a : ℕ → ℂ) (z : ℂ) : ℂ

The step correction ∑ n ≥ 1, a n (∫ x in n..n+1, x ^ (-z - 1) - n ^ (-z - 1)) of the coefficients a. For bounded a the series converges absolutely and is holomorphic on -1 < re z (hasSum_stepCorrection, differentiableOn_stepCorrection).

theorem TauCeti.LSeries.stepCorrection_def (a : ℕ → ℂ) (z : ℂ) : stepCorrection a z = ∑' (n : ℕ), stepCorrectionTerm a n z

The step correction is the sum of its terms (unconditionally, as a tsum).

@[simp]

theorem TauCeti.LSeries.stepCorrectionTerm_zero (a : ℕ → ℂ) : stepCorrectionTerm a 0 = 0

The 0-th term of the step correction vanishes identically.

theorem TauCeti.LSeries.stepCorrectionTerm_of_ne_zero (a : ℕ → ℂ) {n : ℕ} (hn : n ≠ 0) (z : ℂ) : stepCorrectionTerm a n z = a n * ((∫ (x : ℝ) in ↑n..↑n + 1, ↑x ^ (-z - 1)) - ↑n ^ (-z - 1))

For n ≠ 0, the n-th term of the step correction is a n * (∫ x in n..n+1, x ^ (-z - 1) - n ^ (-z - 1)).

theorem TauCeti.LSeries.differentiable_stepCorrectionTerm (a : ℕ → ℂ) (n : ℕ) : Differentiable ℂ (stepCorrectionTerm a n)

Each term of the step correction is entire in z.

theorem TauCeti.LSeries.norm_stepCorrectionTerm_le {z : ℂ} (a : ℕ → ℂ) (n : ℕ) (hz : -2 ≤ z.re) : ‖stepCorrectionTerm a n z‖ ≤ ‖a n‖ * ‖z + 1‖ * ↑n ^ (-z.re - 2)

Mean value bound. For -2 ≤ re z, the n-th term of the step correction is at most ‖a n‖ ‖z + 1‖ n ^ (-re z - 2): on [n, n + 1] the derivative -(z + 1) x ^ (-z - 2) of x ^ (-z - 1) has norm at most ‖z + 1‖ n ^ (-re z - 2).

theorem TauCeti.LSeries.summable_norm_stepCorrectionTerm {a : ℕ → ℂ} {M : ℝ} {z : ℂ} (hbound : ∀ (n : ℕ), 1 ≤ n → ‖a n‖ ≤ M) (hz : -1 < z.re) : Summable fun (n : ℕ) => ‖stepCorrectionTerm a n z‖

For coefficients bounded from n = 1 on, the step correction converges absolutely on -1 < re z.

theorem TauCeti.LSeries.hasSum_stepCorrection {a : ℕ → ℂ} {M : ℝ} {z : ℂ} (hbound : ∀ (n : ℕ), 1 ≤ n → ‖a n‖ ≤ M) (hz : -1 < z.re) : HasSum (fun (n : ℕ) => stepCorrectionTerm a n z) (stepCorrection a z)

For coefficients bounded from n = 1 on, the series defining the step correction converges (absolutely) to stepCorrection a z on -1 < re z.

theorem TauCeti.LSeries.differentiableOn_stepCorrection {a : ℕ → ℂ} {M : ℝ} (hbound : ∀ (n : ℕ), 1 ≤ n → ‖a n‖ ≤ M) : DifferentiableOn ℂ (stepCorrection a) {z : ℂ | -1 < z.re}

Holomorphy of the step correction. For coefficients bounded from n = 1 on, the step correction is holomorphic on the half-plane -1 < re z: near z₀, the terms are bounded uniformly by a multiple of the summable n ^ (-1 - ε) for ε = (re z₀ + 1) / 2.

theorem TauCeti.LSeries.stepCorrectionTerm_apply_zero (a : ℕ → ℂ) (n : ℕ) : stepCorrectionTerm a n 0 = a n * ↑(Real.log (1 + 1 / ↑n) - 1 / ↑n)

At z = 0, the n-th term of the step correction is a n (log (1 + 1 / n) - 1 / n); for n = 0 both sides vanish.

theorem TauCeti.LSeries.stepCorrection_zero (a : ℕ → ℂ) : stepCorrection a 0 = ∑' (n : ℕ), a n * ↑(Real.log (1 + 1 / ↑n) - 1 / ↑n)

The step correction at 0: stepCorrection a 0 = ∑' n, a n (log (1 + 1 / n) - 1 / n).