The left detour in Newman's contour argument

Newman's Tauberian theorem integrates a function g holomorphic on an open set Ω containing the closed half-plane 0 ≤ re z against dz / z over a closed contour around 0: the right semicircle of radius R, parametrized counterclockwise from -R * I to R * I by circleMap 0 R on [-π/2, π/2], followed by a detour back to -R * I through the left half-plane, close enough to the imaginary axis to stay inside Ω.

The detour used here is the parabolic arc newmanDetour R δ, parametrized on [-1, 1] by s ↦ -δ (1 - s²) - R s I. It runs from R * I to -R * I; for R ≥ 0 and δ > 0 it lies in the strip -δ ≤ re z ≤ 0, |im z| ≤ R, and meets the imaginary axis only at its endpoints. This file proves:

• exists_convex_newmanDetour_subset: by compactness of the segment [-R * I, R * I], for some δ > 0 the right semicircle and the detour lie in an open convex subset of Ω;
• integral_right_semicircle_add_integral_newmanDetour: Cauchy's integral formula for the closed contour formed by the right semicircle and the detour, for g holomorphic on such a convex set: the two integrals of g z / z add up to 2πi g 0;
• integral_left_semicircle_eq_integral_newmanDetour: the detour may replace the left semicircle in the integral of g z / z, for g holomorphic on a convex set containing both;
• tendsto_integral_newmanDetour_mul_cexp, tendsto_integral_newmanDetour_mul_kernel: for G continuous on the detour, the detour integral of G against Newman's kernel exp (T z) (1 + z² / R²) / z tends to 0 as T → ∞, by dominated convergence: exp (T z) → 0 on the interior of the detour, where re z < 0, and the endpoints have measure zero;
• intervalIntegrable_newmanDetour_mul_kernel: the detour integrand of a function continuous along the detour against Newman's kernel is interval integrable.

The deformation identities split g z / z into the removable-singularity quotient dslope g 0, which has a primitive on the convex set, and the polar part g 0 / z, whose integral over each of the three arcs is g 0 * π i, since dz / z integrates to π i there (the general splitting is TauCeti.Contour.integral_mul_div_eq_of_hasDerivAt_dslope).

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.newmanDetour (R δ s : ℝ) : ℂ

Newman's left detour. The parabolic arc s ↦ -δ (1 - s²) - R s I, which on [-1, 1] runs from R * I to -R * I; for R, δ ≥ 0 it stays in the strip -δ ≤ re z ≤ 0, |im z| ≤ R.

@[simp]

theorem TauCeti.LSeries.newmanDetour_re (R δ s : ℝ) : (newmanDetour R δ s).re = -(δ * (1 - s ^ 2))

The real part of the detour, -δ (1 - s²).

@[simp]

theorem TauCeti.LSeries.newmanDetour_im (R δ s : ℝ) : (newmanDetour R δ s).im = -(R * s)

The imaginary part of the detour, -R s.

@[simp]

theorem TauCeti.LSeries.newmanDetour_neg_one (R δ : ℝ) : newmanDetour R δ (-1) = ↑R * Complex.I

The detour starts at R * I.

@[simp]

theorem TauCeti.LSeries.newmanDetour_one (R δ : ℝ) : newmanDetour R δ 1 = -(↑R * Complex.I)

The detour ends at -R * I.

theorem TauCeti.LSeries.hasDerivAt_newmanDetour (R δ s : ℝ) : HasDerivAt (newmanDetour R δ) (2 * ↑δ * ↑s - ↑R * Complex.I) s

The velocity of the detour is 2 δ s - R I.

@[simp]

theorem TauCeti.LSeries.deriv_newmanDetour (R δ s : ℝ) : deriv (newmanDetour R δ) s = 2 * ↑δ * ↑s - ↑R * Complex.I

The velocity of the detour is 2 δ s - R I.

theorem TauCeti.LSeries.continuous_newmanDetour (R δ : ℝ) : Continuous (newmanDetour R δ)

The detour is continuous.

theorem TauCeti.LSeries.newmanDetour_ne_zero {R δ : ℝ} (hR : R ≠ 0) (hδ : δ ≠ 0) (s : ℝ) : newmanDetour R δ s ≠ 0

For R ≠ 0 and δ ≠ 0 the detour avoids 0.

theorem TauCeti.LSeries.newmanDetour_re_nonpos {R δ : ℝ} (hδ : 0 ≤ δ) {s : ℝ} (hs : s ∈ Set.Icc (-1) 1) : (newmanDetour R δ s).re ≤ 0

The detour stays in the closed left half-plane on [-1, 1].

theorem TauCeti.LSeries.newmanDetour_re_neg {R δ : ℝ} (hδ : 0 < δ) {s : ℝ} (hs : s ∈ Set.Ioo (-1) 1) : (newmanDetour R δ s).re < 0

Strictly inside [-1, 1] the detour lies in the open left half-plane.

theorem TauCeti.LSeries.exists_convex_newmanDetour_subset {R : ℝ} {Ω : Set ℂ} (hΩ : IsOpen Ω) (hcover : {z : ℂ | 0 ≤ z.re} ⊆ Ω) (hR : 0 ≤ R) : ∃ δ > 0, ∃ U ⊆ Ω, IsOpen U ∧ Convex ℝ U ∧ (∀ θ ∈ Set.Icc (-Real.pi / 2) (Real.pi / 2), circleMap 0 R θ ∈ U) ∧ ∀ s ∈ Set.Icc (-1) 1, newmanDetour R δ s ∈ U

The detour inside the continuation domain. If Ω is open and contains the closed half-plane 0 ≤ re z, then for some δ > 0 the right semicircle of radius R and the detour newmanDetour R δ lie in a common open convex subset of Ω.

theorem TauCeti.LSeries.integral_right_semicircle_add_integral_newmanDetour {R δ : ℝ} {U : Set ℂ} {g : ℂ → ℂ} (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 θ) / circleMap 0 R θ)) + ∫ (s : ℝ) in -1..1, deriv (newmanDetour R δ) s * (g (newmanDetour R δ s) / newmanDetour R δ s) = 2 * ↑Real.pi * Complex.I * g 0

Cauchy's formula for Newman's contour. 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. Then the integral of g z / z over the right semicircle, counterclockwise from -R * I to R * I, plus its integral over the detour, back from R * I to -R * I through the left half-plane, is 2πi g 0. Both integrals include the velocity of their parametrization.

theorem TauCeti.LSeries.integral_left_semicircle_eq_integral_newmanDetour {R δ : ℝ} {U : Set ℂ} {g : ℂ → ℂ} (hR : 0 < R) (hδ : 0 < δ) (hU : IsOpen U) (hconv : Convex ℝ U) (hg : DifferentiableOn ℂ g U) (hcirc : ∀ θ ∈ Set.Icc (Real.pi / 2) (3 * Real.pi / 2), circleMap 0 R θ ∈ U) (hdet : ∀ s ∈ Set.Icc (-1) 1, newmanDetour R δ s ∈ U) : ∫ (θ : ℝ) in Real.pi / 2..3 * Real.pi / 2, circleMap 0 R θ * Complex.I * (g (circleMap 0 R θ) / circleMap 0 R θ) = ∫ (s : ℝ) in -1..1, deriv (newmanDetour R δ) s * (g (newmanDetour R δ s) / newmanDetour R δ s)

The detour replaces the left semicircle. If g is holomorphic on an open convex set U containing the left semicircle of radius R > 0 and the detour newmanDetour R δ with δ > 0, then the integrals of g z / z over the left semicircle, counterclockwise from R * I to -R * I, and over the detour, which has the same endpoints, agree.

theorem TauCeti.LSeries.tendsto_integral_newmanDetour_mul_cexp {R δ : ℝ} {w : ℂ → ℂ} (hδ : 0 < δ) (hw : ContinuousOn w (newmanDetour R δ '' Set.Icc (-1) 1)) : Filter.Tendsto (fun (T : ℝ) => ∫ (s : ℝ) in -1..1, deriv (newmanDetour R δ) s * (w (newmanDetour R δ s) * Complex.exp (↑T * newmanDetour R δ s))) Filter.atTop (nhds 0)

The detour contribution vanishes in the limit. If w is continuous on the detour newmanDetour R δ with δ > 0, then ∫ w(z) exp (T z) dz over the detour tends to 0 as T → ∞: the integrand is dominated by |w(z) dz|, and exp (T z) → 0 wherever re z < 0, which holds except at the two endpoints.

theorem TauCeti.LSeries.tendsto_integral_newmanDetour_mul_kernel {R δ : ℝ} {G : ℂ → ℂ} (hR : 0 < R) (hδ : 0 < δ) (hG : ContinuousOn G (newmanDetour R δ '' Set.Icc (-1) 1)) : Filter.Tendsto (fun (T : ℝ) => ∫ (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)) Filter.atTop (nhds 0)

The detour contribution in Newman's argument vanishes in the limit. If G is continuous on the detour newmanDetour R δ with R, δ > 0, then the detour integral of G against Newman's kernel exp (T z) (1 + z² / R²) / z tends to 0 as T → ∞.

theorem TauCeti.LSeries.intervalIntegrable_newmanDetour_mul_kernel {R δ : ℝ} {w : ℂ → ℂ} {T : ℝ} (hR : 0 < R) (hδ : 0 < δ) (hw : ContinuousOn (fun (s : ℝ) => w (newmanDetour R δ s)) (Set.uIcc (-1) 1)) : IntervalIntegrable (fun (s : ℝ) => deriv (newmanDetour R δ) s * (w (newmanDetour R δ s) * Complex.exp (↑T * newmanDetour R δ s) * (1 + newmanDetour R δ s ^ 2 / ↑R ^ 2) / newmanDetour R δ s)) MeasureTheory.volume (-1) 1

For R, δ > 0, the detour integrand of a function w continuous along the detour newmanDetour R δ against Newman's kernel exp (T z) (1 + z² / R²) / z is interval integrable on [-1, 1].