The semicircle contributions in Newman's argument

The right semicircle is parametrized counterclockwise from -R * I to R * I by circleMap 0 R on [-π/2, π/2]. The left semicircle continues counterclockwise back to -R * I on [π/2, 3π/2]. All integrals below include the velocity z * I of this parametrization.

For a bounded function on the positive half-line, the right semicircle contribution of the Laplace-transform tail and the left semicircle contribution of the truncated transform each have norm at most M / R after division by 2πi. Continuity of the continuation on the closed right arc gives integrability at the imaginary endpoints; the kernel's polynomial factor vanishes there. No estimate divides by the real part at an endpoint.

The final identity splits Cauchy's formula for the truncated transform into these two oriented semicircles. Together these results isolate the circular contributions from the separate left-detour contribution for a holomorphic continuation.

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.

theorem TauCeti.LSeries.intervalIntegrable_right_semicircle_mul_kernel {f : ℝ → ℂ} {G : ℂ → ℂ} {T R : ℝ} (hG : ContinuousOn G (circleMap 0 R '' Set.Icc (-Real.pi / 2) (Real.pi / 2))) : IntervalIntegrable (fun (θ : ℝ) => circleMap 0 R θ * Complex.I * ((G (circleMap 0 R θ) - ∫ (t : ℝ) in 0..T, f t * Complex.exp (-circleMap 0 R θ * ↑t)) * Complex.exp (↑T * circleMap 0 R θ) * (1 + circleMap 0 R θ ^ 2 / ↑R ^ 2) / circleMap 0 R θ)) MeasureTheory.volume (-Real.pi / 2) (Real.pi / 2)

The right-arc tail integrand is integrable, including both imaginary endpoints, whenever the continuation is continuous on that closed arc.

theorem TauCeti.LSeries.intervalIntegrable_circleMap_intervalIntegral_mul_kernel {f : ℝ → ℂ} {T R a b : ℝ} : IntervalIntegrable (fun (θ : ℝ) => circleMap 0 R θ * Complex.I * ((∫ (t : ℝ) in 0..T, f t * Complex.exp (-circleMap 0 R θ * ↑t)) * Complex.exp (↑T * circleMap 0 R θ) * (1 + circleMap 0 R θ ^ 2 / ↑R ^ 2) / circleMap 0 R θ)) MeasureTheory.volume a b

The truncated-transform kernel integrand along a circle is integrable on every finite angle interval, including the imaginary endpoints of either semicircle.

theorem TauCeti.LSeries.norm_integral_right_semicircle_mul_kernel_le {f : ℝ → ℂ} {G : ℂ → ℂ} {M T R : ℝ} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ici 0))) (hbound : ∀ t ∈ Set.Ici 0, ‖f t‖ ≤ M) (hG : ∀ (z : ℂ), 0 < z.re → G z = ∫ (t : ℝ) in Set.Ici 0, f t * Complex.exp (-z * ↑t)) (hR : 0 < R) (hT : 0 ≤ T) : ‖(∫ (θ : ℝ) in -Real.pi / 2..Real.pi / 2, circleMap 0 R θ * Complex.I * ((G (circleMap 0 R θ) - ∫ (t : ℝ) in 0..T, f t * Complex.exp (-circleMap 0 R θ * ↑t)) * Complex.exp (↑T * circleMap 0 R θ) * (1 + circleMap 0 R θ ^ 2 / ↑R ^ 2) / circleMap 0 R θ)) / (2 * ↑Real.pi * Complex.I)‖ ≤ M / R

The normalized right semicircle integral of the Laplace-transform tail has norm at most M / R. The contour runs from -R * I to R * I through the right half-plane. Only agreement with the Laplace transform in the open right half-plane is needed for the bound; intervalIntegrable_right_semicircle_mul_kernel supplies integrability from continuity.

theorem TauCeti.LSeries.norm_integral_left_semicircle_mul_kernel_le {f : ℝ → ℂ} {M T R : ℝ} (hbound : ∀ t ∈ Set.Icc 0 T, ‖f t‖ ≤ M) (hR : 0 < R) (hT : 0 ≤ T) : ‖(∫ (θ : ℝ) in Real.pi / 2..3 * Real.pi / 2, circleMap 0 R θ * Complex.I * ((∫ (t : ℝ) in 0..T, f t * Complex.exp (-circleMap 0 R θ * ↑t)) * Complex.exp (↑T * circleMap 0 R θ) * (1 + circleMap 0 R θ ^ 2 / ↑R ^ 2) / circleMap 0 R θ)) / (2 * ↑Real.pi * Complex.I)‖ ≤ M / R

The normalized left semicircle integral of the truncated transform has norm at most M / R. The contour runs from R * I to -R * I through the left half-plane.

theorem TauCeti.LSeries.integral_semicircles_intervalIntegral_mul_kernel {f : ℝ → ℂ} {T R : ℝ} (hR : 0 < R) : ((∫ (θ : ℝ) in -Real.pi / 2..Real.pi / 2, circleMap 0 R θ * Complex.I * ((∫ (t : ℝ) in 0..T, f t * Complex.exp (-circleMap 0 R θ * ↑t)) * Complex.exp (↑T * circleMap 0 R θ) * (1 + circleMap 0 R θ ^ 2 / ↑R ^ 2) / circleMap 0 R θ)) + ∫ (θ : ℝ) in Real.pi / 2..3 * Real.pi / 2, circleMap 0 R θ * Complex.I * ((∫ (t : ℝ) in 0..T, f t * Complex.exp (-circleMap 0 R θ * ↑t)) * Complex.exp (↑T * circleMap 0 R θ) * (1 + circleMap 0 R θ ^ 2 / ↑R ^ 2) / circleMap 0 R θ)) / (2 * ↑Real.pi * Complex.I) = ∫ (t : ℝ) in 0..T, f t

Cauchy's formula for the truncated transform, split into the counterclockwise right and left semicircles and normalized by 2πi. Both arcs are traversed in increasing angle.