Construction of the pair-correlation kernel

The cutoff construction packages the unweighted pair sum, proves that the normalized cutoff is admissible, and develops the analytic identities needed to apply pair correlation.

noncomputable def ZetaZeros.unweightedKernelSum (eta : ℝ → ℝ) (T : ℝ) : ℂ

The unweighted second moment of the test kernel over ordered pairs of zeta zeros.

Equations

• One or more equations did not get rendered due to their size.

theorem ZetaZeros.integrable_cutoffTestSq {delta : ℝ} (hd : 0 < delta) (hd4 : delta < 1 / 4) {psi : ℝ → ℝ} (hpsi : IsCutoff delta psi) : MeasureTheory.Integrable (cutoffTestSq psi) MeasureTheory.volume

The square of the normalized cutoff is integrable.

theorem ZetaZeros.integrable_cutoffSelfConv {delta : ℝ} (hd : 0 < delta) (hd4 : delta < 1 / 4) {psi : ℝ → ℝ} (hpsi : IsCutoff delta psi) : MeasureTheory.Integrable (cutoffSelfConv psi) MeasureTheory.volume

The self-convolution is integrable.

theorem ZetaZeros.hasCompactSupport_iteratedDeriv_two_cutoffSelfConv {delta : ℝ} {psi : ℝ → ℝ} (hpsi : IsCutoff delta psi) : HasCompactSupport (iteratedDeriv 2 (cutoffSelfConv psi))

The second derivative of the self-convolution has compact support.

theorem ZetaZeros.integrable_iteratedDeriv_two_cutoffSelfConv {delta : ℝ} {psi : ℝ → ℝ} (hpsi : IsCutoff delta psi) : MeasureTheory.Integrable (iteratedDeriv 2 (cutoffSelfConv psi)) MeasureTheory.volume

The second derivative of the self-convolution is integrable.

theorem ZetaZeros.fourierC_iteratedDeriv_two_cutoffSelfConv {delta : ℝ} {psi : ℝ → ℝ} (hpsi : IsCutoff delta psi) (z : ℂ) : fourierC (iteratedDeriv 2 (cutoffSelfConv psi)) z = -4 * ↑Real.pi ^ 2 * z ^ 2 * testKernel (cutoffTest psi) z ^ 2

The complex-frequency Fourier transform of the second derivative has the expected quadratic multiplier.

theorem ZetaZeros.fourierC_correctedTest {delta : ℝ} {psi : ℝ → ℝ} (hpsi : IsCutoff delta psi) {T : ℝ} (hT : 1 < T) (z : ℂ) : fourierC (correctedTest psi T) z = (1 + ↑Real.pi ^ 2 * z ^ 2 / ↑(Real.log T) ^ 2) * testKernel (cutoffTest psi) z ^ 2

Fourier transform of the corrected pair-correlation test function.

theorem ZetaZeros.correctedTest_weight_cancel {delta : ℝ} {psi : ℝ → ℝ} (hpsi : IsCutoff delta psi) {T : ℝ} (hT : 1 < T) {rho rho' : ℂ} (hrho0 : 0 < rho.re) (hrho1 : rho.re < 1) (hrho0' : 0 < rho'.re) (hrho1' : rho'.re < 1) : fourierC (correctedTest psi T) (rescaledDiff T rho rho') * pairWeight (rho - rho') = testKernel (cutoffTest psi) (rescaledDiff T rho rho') ^ 2

At a rescaled pair of zeros, the correction factor cancels the unconditional pair-correlation weight.

theorem ZetaZeros.cutoffSelfConv_isPairTestFunction {delta : ℝ} (hd : 0 < delta) (hd4 : delta < 1 / 4) {psi : ℝ → ℝ} (hpsi : IsCutoff delta psi) : IsPairTestFunction (cutoffSelfConv psi)

The self-convolution is an admissible pair-correlation test function.

theorem ZetaZeros.iteratedDeriv_two_cutoffSelfConv_isPairTestFunction {delta : ℝ} {psi : ℝ → ℝ} (hpsi : IsCutoff delta psi) : IsPairTestFunction (iteratedDeriv 2 (cutoffSelfConv psi))

The second derivative of the self-convolution is an admissible pair-correlation test function.

theorem ZetaZeros.unweightedKernelSum_cutoffTest_eq_pairCorrelationSum {delta : ℝ} {psi : ℝ → ℝ} (hpsi : IsCutoff delta psi) {T : ℝ} (hT : 1 < T) : unweightedKernelSum (cutoffTest psi) T = pairCorrelationSum (cutoffSelfConv psi) T - pairCorrelationSum (iteratedDeriv 2 (cutoffSelfConv psi)) T / ↑(4 * Real.log T ^ 2)

The unweighted kernel sum is the difference of the two pair-correlation sums supplied by the corrected test function, expanded linearly.

theorem ZetaZeros.PairCorrelation.tendsto (hPC : PairCorrelation) {f : ℝ → ℝ} (hf : IsPairTestFunction f) : Filter.Tendsto (fun (T : ℝ) => pairCorrelationSum f T / ↑(zeroScale T)) Filter.atTop (nhds ↑(pairMainTerm f))

The quantitative pair-correlation hypothesis implies convergence to its stated main term.

theorem ZetaZeros.unweightedKernelSum_cutoffTest_tendsto (hPC : PairCorrelation) {delta : ℝ} (hd : 0 < delta) (hd4 : delta < 1 / 4) {psi : ℝ → ℝ} (hpsi : IsCutoff delta psi) : Filter.Tendsto (fun (T : ℝ) => unweightedKernelSum (cutoffTest psi) T / ↑(zeroScale T)) Filter.atTop (nhds ↑(pairMainTerm (cutoffSelfConv psi)))

The normalized unweighted cutoff-kernel sum converges to the pair-correlation functional of the self-convolution. The second-derivative correction vanishes because of its log T squared denominator.

Removing the cutoff

The last step of the construction. We choose a cutoff at scale 1 / (n + 5), use dominated convergence first for its normalising constant and then for the two convolution integrals, and finally pass to the pair-correlation functional.

theorem ZetaZeros.exists_cutoff_pairMainTerm_close (ε : ℝ) (hε : 0 < ε) : ∃ (delta : ℝ) (psi : ℝ → ℝ), 0 < delta ∧ delta < 1 / 4 ∧ IsCutoff delta psi ∧ |pairMainTerm (cutoffSelfConv psi) - montgomeryTaylorConst| < ε

The cutoff constants converge to the Montgomery--Taylor constant (lem_C_delta_limit).

theorem ZetaZeros.kernelConstruction (hPC : PairCorrelation) (ε : ℝ) (hε : 0 < ε) : ∃ (eta : ℝ → ℝ) (C : ℝ), IsAdmissible (1 / 2) eta ∧ |C - montgomeryTaylorConst| < ε ∧ Filter.Tendsto (fun (T : ℝ) => (unweightedKernelSum eta T).re / zeroScale T) Filter.atTop (nhds C)

Kernel construction (lem_kernel_construction). The cutoff test is admissible, its pair-correlation constant is arbitrarily close to the Montgomery--Taylor constant, and the normalized unweighted kernel sum converges to that constant.