Hardy's Z function

Hardy's Z function is the real-valued function on ℝ whose zeros are exactly the heights of the zeros of ζ on the critical line. It is defined here by dividing the completed zeta function Λ on the critical line by the modulus of its archimedean factor:

$$ Z(t) = \frac{\Lambda(1/2 + it)}{|\Gamma_{\mathbb{R}}(1/2 + it)|}. $$

The numerator is real, by completedRiemannZeta_conj together with the functional equation completedRiemannZeta_one_sub, and the denominator is a positive real, so Z is real-valued.

Main results

• hardyZ: the definition, as a function ℝ → ℝ.
• abs_hardyZ: |Z t| = ‖ζ (1/2 + i t)‖.
• hardyZ_neg: Z is even.
• hardyZ_eq_zero_iff: Z t = 0 ↔ ζ (1/2 + i t) = 0, the reason the definition exists.
• continuous_hardyZ: Z is continuous, so the intermediate value theorem applies to it and sign changes of Z locate zeros of ζ on the critical line.

TODO

• Add the relation to the Riemann–Siegel theta function, see https://en.wikipedia.org/wiki/Riemann%E2%80%93Siegel_theta_function.

References

• E. C. Titchmarsh, The theory of the Riemann zeta-function, §4.17

theorem conj_completedRiemannZeta_half_add_mul_I (t : ℝ) : (starRingEnd ℂ) (completedRiemannZeta (1 / 2 + ↑t * Complex.I)) = completedRiemannZeta (1 / 2 + ↑t * Complex.I)

The completed zeta function is real on the critical line.

theorem completedRiemannZeta_half_add_mul_I_im (t : ℝ) : (completedRiemannZeta (1 / 2 + ↑t * Complex.I)).im = 0

noncomputable def hardyZ (t : ℝ) : ℝ

Hardy's Z function: the real-valued function on ℝ obtained by dividing Λ on the critical line by the modulus of its archimedean factor. Its zeros are exactly the heights of the zeros of ζ on the critical line.

Equations

• hardyZ t = (completedRiemannZeta (1 / 2 + ↑t * Complex.I)).re / ‖(1 / 2 + ↑t * Complex.I).Gammaℝ‖

theorem ofReal_hardyZ (t : ℝ) : ↑(hardyZ t) = completedRiemannZeta (1 / 2 + ↑t * Complex.I) / ↑‖(1 / 2 + ↑t * Complex.I).Gammaℝ‖

theorem abs_hardyZ (t : ℝ) : |hardyZ t| = ‖riemannZeta (1 / 2 + ↑t * Complex.I)‖

Z has the same modulus as ζ on the critical line.

theorem hardyZ_neg (t : ℝ) : hardyZ (-t) = hardyZ t

Z is an even function.

theorem hardyZ_eq_zero_iff (t : ℝ) : hardyZ t = 0 ↔ riemannZeta (1 / 2 + ↑t * Complex.I) = 0

The zeros of Z on ℝ are exactly the heights of the zeros of ζ on the critical line.

theorem continuous_hardyZ : Continuous hardyZ

Hardy's Z-function is continuous.