Newman's Tauberian theorem for bounded Laplace transforms

Let f : ℝ → ℂ be measurable and bounded by M on [0, ∞), and let G be holomorphic on an open set Ω containing the closed half-plane 0 ≤ re z, agreeing with the Laplace transform ∫ t in Ici 0, f t * exp (-z t) on 0 < re z. Newman's Tauberian theorem (newmanLaplace_tendsto_integral) states that the improper integral ∫ t in 0..T, f t converges to G 0 as T → ∞.

The proof assembles the contour estimates of the neighbouring files. Fix R > 0 and choose a detour newmanDetour R δ through the left half-plane inside Ω. With G_T z = ∫ t in 0..T, f t * exp (-z t) and Newman's kernel k_T z = exp (T z) (1 + z² / R²) / z:

• Cauchy's formula for (G - G_T) k_T on the right semicircle closed by the detour, together with the deformation of the left semicircle into the detour for the entire function G_T, gives integral_right_semicircle_add_integral_newmanDetour_mul_kernel: the right semicircle integral of (G - G_T) k_T plus the detour integral of G k_T equals 2πi (G 0 - ∫ t in 0..T, f t) plus the left semicircle integral of G_T k_T;
• the two semicircle contributions are at most M / R after division by 2πi, and the detour integral of G k_T tends to 0 as T → ∞, so eventually ‖G 0 - ∫ t in 0..T, f t‖ ≤ 2 M / R + ε (eventually_norm_sub_intervalIntegral_le);
• letting R → ∞ gives the theorem.

No radius-independent continuation width is used: the detour depends on R.

Since the Laplace transform is already holomorphic on 0 < re z, the continuation hypothesis only concerns the imaginary axis: newmanLaplace_tendsto_integral_of_analyticAt asks instead that G be analytic at each point of re z = 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.

theorem TauCeti.LSeries.integral_right_semicircle_add_integral_newmanDetour_mul_kernel {f : ℝ → ℂ} {G : ℂ → ℂ} {T R δ : ℝ} {U : Set ℂ} (hR : 0 < R) (hδ : 0 < δ) (hU : IsOpen U) (hconv : Convex ℝ U) (hG : DifferentiableOn ℂ G U) (hcirc : ∀ θ ∈ Set.Icc (-Real.pi / 2) (Real.pi / 2), circleMap 0 R θ ∈ U) (hdet : ∀ s ∈ Set.Icc (-1) 1, newmanDetour R δ s ∈ U) : (∫ (θ : ℝ) 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 θ)) + ∫ (s : ℝ) in -1..1, deriv (newmanDetour R δ) s * (G (newmanDetour R δ s) * Complex.exp (↑T * newmanDetour R δ s) * (1 + newmanDetour R δ s ^ 2 / ↑R ^ 2) / newmanDetour R δ s) = 2 * ↑Real.pi * Complex.I * (G 0 - ∫ (t : ℝ) in 0..T, f 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 θ)

Newman's contour identity. Let G be holomorphic on an open convex set U containing the right semicircle of radius R > 0 and the detour newmanDetour R δ with δ > 0, and let G_T z = ∫ t in 0..T, f t * exp (-z t). Against Newman's kernel k_T z = exp (T z) (1 + z² / R²) / z, the right semicircle integral of (G - G_T) k_T (counterclockwise from -R * I to R * I) plus the detour integral of G k_T (from R * I back to -R * I) equals 2πi (G 0 - ∫ t in 0..T, f t) plus the left semicircle integral of G_T k_T (counterclockwise from R * I to -R * I). All integrals include the velocity of their parametrization.

theorem TauCeti.LSeries.eventually_norm_sub_intervalIntegral_le {f : ℝ → ℂ} {G : ℂ → ℂ} {M R : ℝ} {Ω : Set ℂ} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ici 0))) (hbound : ∀ t ∈ Set.Ici 0, ‖f t‖ ≤ M) (hΩ : IsOpen Ω) (hcover : {z : ℂ | 0 ≤ z.re} ⊆ Ω) (hG : DifferentiableOn ℂ G Ω) (hLaplace : ∀ (z : ℂ), 0 < z.re → G z = ∫ (t : ℝ) in Set.Ici 0, f t * Complex.exp (-z * ↑t)) (hR : 0 < R) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (T : ℝ) in Filter.atTop, ‖G 0 - ∫ (t : ℝ) in 0..T, f t‖ ≤ 2 * M / R + ε

Newman's estimate at a fixed radius. Let f be measurable and bounded by M on [0, ∞), and let G be holomorphic on an open set Ω containing the closed half-plane 0 ≤ re z and equal to the Laplace transform of f on 0 < re z. For every R > 0 and ε > 0, eventually in T, ‖G 0 - ∫ t in 0..T, f t‖ ≤ 2 M / R + ε.

theorem TauCeti.LSeries.newmanLaplace_tendsto_integral {f : ℝ → ℂ} {G : ℂ → ℂ} {M : ℝ} {Ω : Set ℂ} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ici 0))) (hbound : ∀ t ∈ Set.Ici 0, ‖f t‖ ≤ M) (hΩ : IsOpen Ω) (hcover : {z : ℂ | 0 ≤ z.re} ⊆ Ω) (hG : DifferentiableOn ℂ G Ω) (hLaplace : ∀ (z : ℂ), 0 < z.re → G z = ∫ (t : ℝ) in Set.Ici 0, f t * Complex.exp (-z * ↑t)) : Filter.Tendsto (fun (T : ℝ) => ∫ (t : ℝ) in 0..T, f t) Filter.atTop (nhds (G 0))

Newman's Tauberian theorem. Let f : ℝ → ℂ be measurable and bounded on [0, ∞), and let G be holomorphic on an open set Ω containing the closed half-plane 0 ≤ re z, agreeing with the Laplace transform ∫ t in Ici 0, f t * exp (-z t) on the open half-plane 0 < re z. Then ∫ t in 0..T, f t converges to G 0 as T → ∞.

theorem TauCeti.LSeries.newmanLaplace_tendsto_integral_of_analyticAt {f : ℝ → ℂ} {G : ℂ → ℂ} {M : ℝ} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ici 0))) (hbound : ∀ t ∈ Set.Ici 0, ‖f t‖ ≤ M) (hG : ∀ (z : ℂ), z.re = 0 → AnalyticAt ℂ G z) (hLaplace : ∀ (z : ℂ), 0 < z.re → G z = ∫ (t : ℝ) in Set.Ici 0, f t * Complex.exp (-z * ↑t)) : Filter.Tendsto (fun (T : ℝ) => ∫ (t : ℝ) in 0..T, f t) Filter.atTop (nhds (G 0))

Newman's Tauberian theorem, with a pointwise continuation hypothesis. Let f : ℝ → ℂ be measurable and bounded on [0, ∞), and let G agree with the Laplace transform ∫ t in Ici 0, f t * exp (-z t) on the open half-plane 0 < re z and be analytic at every point of the imaginary axis re z = 0. Then ∫ t in 0..T, f t converges to G 0 as T → ∞.

Since the Laplace transform is holomorphic on 0 < re z, this hypothesis on G is equivalent to holomorphy on an open set containing the closed half-plane 0 ≤ re z, as in newmanLaplace_tendsto_integral.