Truncated Laplace transforms and the estimates of Newman's contour argument

Let f : ℝ → ℂ be bounded by M on [0, ∞). Newman's Tauberian theorem compares the Laplace transform G z = ∫ t in Ici 0, f t * exp (-z t) with its truncations G_T z = ∫ t in 0..T, f t * exp (-z t) against the kernel exp (T z) (1 + z² / R²) / z on the circle ‖z‖ = R. Combining the general Laplace estimates of TauCeti.Analysis.Complex.LaplaceTransform (truncations are entire, the transform is holomorphic on 0 < re z, and the tail and left half-plane bounds) with the identity ‖1 + z² / R²‖ = 2 |re z| / R on the circle ‖z‖ = R, this file proves:

• the kernel cancellation norm_mul_kernel_le_of_norm_eq: on the circle, if ‖w‖ ≤ M exp (-T re z) / |re z| then w times the kernel has norm at most 2 M / R²;
• consequently, both integrands of the contour argument are bounded by 2 M / R², uniformly in T;
• Cauchy's formula for the entire function G_T: its kernel integral over the full circle is 2πi ∫ t in 0..T, f t.

The factor exp (T z) cancels the decay exp (-T re z), making the bounds independent of T; the factor 1 + z² / R² cancels the small denominator re z on the circle, making them uniform up to the imaginary axis.

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.norm_mul_kernel_le_of_norm_eq {M T : ℝ} {w z : ℂ} {R : ℝ} (hz : ‖z‖ = R) (hR : 0 < R) (hre : z.re ≠ 0) (hw : ‖w‖ ≤ M * Real.exp (-z.re * T) / |z.re|) : ‖w * Complex.exp (↑T * z) * (1 + z ^ 2 / ↑R ^ 2) / z‖ ≤ 2 * M / R ^ 2

Kernel cancellation. On the circle ‖z‖ = R off the imaginary axis, if ‖w‖ is at most M exp (-T re z) / |re z|, then w multiplied by Newman's kernel exp (T z) (1 + z² / R²) / z has norm at most 2 M / R²: the factor exp (T z) cancels exp (-T re z) and the factor 1 + z² / R² cancels the denominator |re z|.

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

Right-arc integrand bound. On the circle ‖z‖ = R with 0 < re z, the difference between the Laplace transform of a function bounded by M on [0, ∞) and its truncation at T ≥ 0, multiplied by Newman's kernel exp (T z) (1 + z² / R²) / z, is at most 2 M / R².

theorem TauCeti.LSeries.norm_intervalIntegral_mul_kernel_le_of_re_neg {f : ℝ → ℂ} {M T : ℝ} (hbound : ∀ t ∈ Set.Icc 0 T, ‖f t‖ ≤ M) {z : ℂ} {R : ℝ} (hz : ‖z‖ = R) (hR : 0 < R) (hre : z.re < 0) (hT : 0 ≤ T) : ‖(∫ (t : ℝ) in 0..T, f t * Complex.exp (-z * ↑t)) * Complex.exp (↑T * z) * (1 + z ^ 2 / ↑R ^ 2) / z‖ ≤ 2 * M / R ^ 2

Left-arc integrand bound. On the circle ‖z‖ = R with re z < 0, the truncation at T ≥ 0 of the Laplace transform of a function bounded by M on [0, T], multiplied by Newman's kernel exp (T z) (1 + z² / R²) / z, is at most 2 M / R².

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

Cauchy's formula for a truncated transform. For R > 0, the integral of the truncated Laplace transform against Newman's kernel exp (T z) (1 + z² / R²) / z over the circle ‖z‖ = R is 2πi times its value at 0, namely 2πi ∫ t in 0..T, f t.