The Montgomery--Taylor computation

A(Q_0) = C_MT: the pair-correlation functional at the self-convolution of the extremal test function is the Montgomery--Taylor constant. It is proved here rather than assumed.

The three preceding files supply the pieces: the functional is the integral of f_0 against G (Reduction), G is constant (AffineKernel), and that constant is C_MT (Evaluation). With f_0 of total mass one, the integral collapses to the constant.

theorem ZetaZeros.montgomeryTaylor : extremalSelfConv 0 + 2 * ∫ (α : ℝ) in 0..1, α * extremalSelfConv α = montgomeryTaylorConst

The Montgomery--Taylor computation (lem_montgomery_taylor). See Montgomery, Distribution of the zeros of the Riemann zeta function, Proc. ICM (Vancouver, 1974), Vol. 1, 379--381.