Documentation

LeanPool.ZetaZeros.Zeta.Mass

The extremal test function has total mass one #

The normalisation that makes f₀ a probability density, and hence makes the Montgomery–Taylor constant the value of the pair-correlation functional at its self-convolution rather than a multiple of it.

The constant √2 sin(1/√2) in the denominator of f₀ is exactly what the substitution x ↦ √2 x produces, which is why the mass comes out at one on the nose.

The extremal test function has total mass one.