The truncated Perron kernel

Perron's formula recovers a summatory function from a Dirichlet series by integrating x ^ s / s up a vertical line. At finite height the integral is not the sharp step function it approximates, and this file makes the finite-height object visible before any estimate is applied to it.

TauCeti.truncatedPerronKernel x c T is the value of (2πi)⁻¹ ∫ x ^ s / s ds over the segment from c - iT to c + iT. Parameterizing that segment by s = c + i t with t real turns ds into i dt, so the i in (2πi)⁻¹ cancels and the visible prefactor is (2π)⁻¹; the integrand along the segment is TauCeti.perronIntegrand.

Away from the endpoint the kernel is a smoothed step: it is close to 1 for x > 1 and close to 0 for x < 1, with an error that is proved here with the explicit constant π⁻¹. Both estimates come from moving the segment of integration horizontally, towards the side on which x ^ s decays; for x > 1 that move crosses the pole of x ^ s / s at the origin, and the residue is what produces the step.

Main results

• TauCeti.truncatedPerronKernel_one: at x = 1 the kernel is exactly π⁻¹ * Real.arctan (T / c).
• TauCeti.truncatedPerronKernel_one_ne_half: consequently it is never 1 / 2, at any finite height. The value 1 / 2 conventionally attached to the endpoint x = 1 is only a limit.
• TauCeti.tendsto_truncatedPerronKernel_one: that limit, as the height tends to infinity.
• TauCeti.truncatedPerronKernel_im: the kernel is real, because the integrand takes conjugate values at opposite heights.
• TauCeti.norm_truncatedPerronKernel_sub_step_le: the smoothed-step estimate ‖K x c T - perronStep x‖ ≤ x ^ c / (π * T * |log x|) for x ≠ 1, together with its two halves TauCeti.norm_truncatedPerronKernel_le_of_lt_one and TauCeti.norm_truncatedPerronKernel_sub_one_le_of_one_lt.
• TauCeti.norm_truncatedPerronKernel_one_le and TauCeti.norm_perronStep_le_one: the kernel at the endpoint and the sharp step are each bounded by one in modulus, uniformly in the height.
• TauCeti.tendsto_truncatedPerronKernel: consequently the kernel tends to the sharp step TauCeti.perronStep, which carries the customary half-weight at the endpoint, as the height tends to infinity, at every positive x.

References

• E. C. Titchmarsh, revised by D. R. Heath-Brown, The Theory of the Riemann Zeta-Function, Lemma 3.12.
• H. Davenport, Multiplicative Number Theory, Chapter 17.

noncomputable def TauCeti.perronIntegrand (x c t : ℝ) : ℂ

The integrand of the truncated Perron integral: the value of s ↦ x ^ s / s at the point s = c + i t of the vertical line Re s = c.

@[simp]

theorem TauCeti.perronIntegrand_one (c t : ℝ) : perronIntegrand 1 c t = (↑c + ↑t * Complex.I)⁻¹

At the endpoint x = 1 the Perron integrand is the reciprocal of the point of the line.

theorem TauCeti.perronIntegrand_def (x c t : ℝ) : perronIntegrand x c t = ↑x ^ (↑c + ↑t * Complex.I) / (↑c + ↑t * Complex.I)

Defining equation of the Perron integrand. Its value at height t is x ^ s / s for s = c + i t. Use this rather than unfolding the definition.

@[simp]

theorem TauCeti.perronIntegrand_zero (c t : ℝ) : perronIntegrand 0 c t = 0

The Perron integrand vanishes at the ratio 0, on every vertical line and at every height. At the origin this uses the convention that division by zero is zero.

theorem TauCeti.norm_perronIntegrand {x : ℝ} (hx : 0 < x) (c t : ℝ) : ‖perronIntegrand x c t‖ = x ^ c / √(c ^ 2 + t ^ 2)

The modulus of the Perron integrand: the numerator contributes x ^ c, independently of the height, and the denominator the distance from the origin to c + i t.

theorem TauCeti.continuous_perronIntegrand {x c : ℝ} (hx : x ≠ 0) (hc : c ≠ 0) : Continuous (perronIntegrand x c)

The Perron integrand is continuous in the height along any vertical line off the imaginary axis.

theorem TauCeti.intervalIntegrable_perronIntegrand {x c : ℝ} (hx : x ≠ 0) (hc : c ≠ 0) (a b : ℝ) : IntervalIntegrable (perronIntegrand x c) MeasureTheory.volume a b

The Perron integrand is integrable over every bounded piece of a vertical line off the imaginary axis.

theorem TauCeti.conj_perronIntegrand {x : ℝ} (hx : 0 ≤ x) (c t : ℝ) : (starRingEnd ℂ) (perronIntegrand x c t) = perronIntegrand x c (-t)

The Perron integrand takes complex conjugate values at opposite heights.

noncomputable def TauCeti.truncatedPerronKernel (x c T : ℝ) : ℂ

The truncated Perron kernel of height T on the vertical line Re s = c: the value of (2πi)⁻¹ ∫ x ^ s / s ds over the segment from c - iT to c + iT.

The segment is parameterized by s = c + i t for t in [-T, T], so ds = i dt and the visible prefactor is (2π)⁻¹ rather than (2πi)⁻¹.

theorem TauCeti.truncatedPerronKernel_def (x c T : ℝ) : truncatedPerronKernel x c T = (↑(2 * Real.pi))⁻¹ * ∫ (t : ℝ) in -T..T, perronIntegrand x c t

Defining equation of the truncated Perron kernel. Use this rather than unfolding the definition.

@[simp]

theorem TauCeti.truncatedPerronKernel_height_zero (x c : ℝ) : truncatedPerronKernel x c 0 = 0

At zero height the truncated Perron kernel vanishes: the segment of integration is a point.

@[simp]

theorem TauCeti.truncatedPerronKernel_zero (c T : ℝ) : truncatedPerronKernel 0 c T = 0

The truncated Perron kernel vanishes at the ratio 0, on every vertical line and at every truncation height.

@[simp]

theorem TauCeti.truncatedPerronKernel_im {x : ℝ} (hx : 0 ≤ x) (c T : ℝ) : (truncatedPerronKernel x c T).im = 0

The truncated Perron kernel is real: the two halves of the segment contribute conjugate values.

theorem TauCeti.truncatedPerronKernel_one {c : ℝ} (hc : c ≠ 0) (T : ℝ) : truncatedPerronKernel 1 c T = ↑(Real.pi⁻¹ * Real.arctan (T / c))

The exact value of the truncated Perron kernel at the endpoint x = 1.

theorem TauCeti.truncatedPerronKernel_one_ne_half {c : ℝ} (hc : 0 < c) (T : ℝ) : truncatedPerronKernel 1 c T ≠ 1 / 2

At any finite height the Perron kernel at the endpoint x = 1 is not 1 / 2; the customary half-weight there is only the limit TauCeti.tendsto_truncatedPerronKernel_one.

theorem TauCeti.tendsto_truncatedPerronKernel_one {c : ℝ} (hc : 0 < c) : Filter.Tendsto (truncatedPerronKernel 1 c) Filter.atTop (nhds (1 / 2))

As the height tends to infinity the Perron kernel at the endpoint x = 1 tends to 1 / 2.

Moving the segment sideways

The estimates below all rest on the same device: the integral of x ^ s / s over the boundary of a rectangle vanishes when the origin is outside it, so the segment of integration may be pushed horizontally at the cost of the two horizontal sides. The material of this section is the book keeping that device needs: the integrand as a function of s, its size on horizontal and vertical sides, and the integral of x ^ σ that bounds a horizontal side.

Below the endpoint

For x < 1 the function x ^ s decays as Re s grows, so the segment may be pushed to the line Re s = B with B → ∞. The far side then vanishes in the limit and only the two horizontal sides survive; each of them is at most x ^ c / (T * |log x|).

theorem TauCeti.norm_truncatedPerronKernel_le_of_lt_one {x c T : ℝ} (hx : 0 < x) (hx1 : x < 1) (hc : 0 < c) (hT : 0 < T) : ‖truncatedPerronKernel x c T‖ ≤ x ^ c / (Real.pi * T * |Real.log x|)

Below the endpoint the truncated Perron kernel is small. For 0 < x < 1 it differs from 0 by at most x ^ c / (π * T * |log x|).

Above the endpoint

For x > 1 the function x ^ s decays as Re s decreases, so the segment is pushed to the left instead. That move crosses the pole of x ^ s / s at the origin. Rather than invoke a residue theorem, the integrand is split as (x ^ s - 1) / s + 1 / s: the first summand extends across the origin as dslope, so Cauchy's theorem applies to it verbatim, and the second is integrated in closed form, its four sides contributing the four arctangents that add up to 2 π i.

theorem TauCeti.norm_truncatedPerronKernel_sub_one_le_of_one_lt {x c T : ℝ} (hx1 : 1 < x) (hc : 0 < c) (hT : 0 < T) : ‖truncatedPerronKernel x c T - 1‖ ≤ x ^ c / (Real.pi * T * |Real.log x|)

Above the endpoint the truncated Perron kernel is close to one. For 1 < x it differs from 1 by at most x ^ c / (π * T * |log x|).

noncomputable def TauCeti.perronStep (x : ℝ) : ℂ

The sharp step that the truncated Perron kernel approximates: 1 above the endpoint, 0 below it, and the customary Perron half-weight 1 / 2 at the endpoint x = 1, which is the value the kernel tends to there (TauCeti.tendsto_truncatedPerronKernel_one) even though it never attains it at finite height (TauCeti.truncatedPerronKernel_one_ne_half).

@[simp]

theorem TauCeti.perronStep_of_one_lt {x : ℝ} (hx : 1 < x) : perronStep x = 1

@[simp]

theorem TauCeti.perronStep_one : perronStep 1 = 1 / 2

@[simp]

theorem TauCeti.perronStep_of_lt_one {x : ℝ} (hx : x < 1) : perronStep x = 0

theorem TauCeti.norm_truncatedPerronKernel_sub_step_le {x c T : ℝ} (hx : 0 < x) (hx1 : x ≠ 1) (hc : 0 < c) (hT : 0 < T) : ‖truncatedPerronKernel x c T - perronStep x‖ ≤ x ^ c / (Real.pi * T * |Real.log x|)

The truncated Perron kernel is a smoothed step. Away from the endpoint x = 1 it differs from TauCeti.perronStep by at most x ^ c / (π * T * |log x|).

The endpoint x = 1 is genuinely excluded: there the error is |π⁻¹ arctan (T / c) - 1 / 2|, which no bound of this shape controls, and the kernel never attains the half-weight (TauCeti.truncatedPerronKernel_one_ne_half).

theorem TauCeti.tendsto_truncatedPerronKernel {x c : ℝ} (hx : 0 < x) (hc : 0 < c) : Filter.Tendsto (truncatedPerronKernel x c) Filter.atTop (nhds (perronStep x))

As the height tends to infinity the truncated Perron kernel tends to the sharp step, at every positive x; at the endpoint x = 1 this is the half-weight limit TauCeti.tendsto_truncatedPerronKernel_one.

theorem TauCeti.norm_truncatedPerronKernel_one_le {c : ℝ} (hc : c ≠ 0) (T : ℝ) : ‖truncatedPerronKernel 1 c T‖ ≤ 1

At the endpoint the kernel is π⁻¹ arctan (T / c), so it never exceeds one in modulus, uniformly in the height. This is the index the smoothed-step estimate excludes.

theorem TauCeti.norm_perronStep_le_one (y : ℝ) : ‖perronStep y‖ ≤ 1

The sharp step never exceeds one in modulus.