Elementary asymptotic consequences of Riemann--von Mangoldt

This file turns the epsilon-form external input into the filter form used by the final proportion argument and records the eventual positivity needed to divide by the zero count.

noncomputable def ZetaZeros.zeroScale (T : ℝ) : ℝ

The main scale in the Riemann--von Mangoldt and pair-correlation formulae.

Equations

• ZetaZeros.zeroScale T = T / (2 * Real.pi) * Real.log T

theorem ZetaZeros.zeroScale_pos_eventually : ∀ᶠ (T : ℝ) in Filter.atTop, 0 < zeroScale T

The Riemann--von Mangoldt scale is positive at all sufficiently large heights.

theorem ZetaZeros.RiemannVonMangoldt.tendsto (hRvM : RiemannVonMangoldt) : Filter.Tendsto (fun (T : ℝ) => ↑(zeroCount T) / zeroScale T) Filter.atTop (nhds 1)

Epsilon-form Riemann--von Mangoldt is convergence of the normalized count to one.

theorem ZetaZeros.RiemannVonMangoldt.zeroCount_pos_eventually (hRvM : RiemannVonMangoldt) : ∀ᶠ (T : ℝ) in Filter.atTop, 0 < ↑(zeroCount T)

Riemann--von Mangoldt in particular makes the zero count positive eventually.