Proportion bounds for zeta zeros

This combines the kernel construction, the finite-set bounds transferred to zeta zeros, and the Riemann--von Mangoldt asymptotic to obtain the two asymptotic proportion bounds.

theorem ZetaZeros.simple_proportion_lower (hRvM : RiemannVonMangoldt) (hPC : PairCorrelation) (ε : ℝ) (hε : 0 < ε) : ∃ (T₀ : ℝ), ∀ T ≥ T₀, 3 / 2 - 1 / √2 * (1 / √2).cot - ε < ↑(simpleOnLineCount T) / ↑(zeroCount T)

theorem ZetaZeros.distinct_proportion_lower (hRvM : RiemannVonMangoldt) (hPC : PairCorrelation) (ε : ℝ) (hε : 0 < ε) : ∃ (T₀ : ℝ), ∀ T ≥ T₀, 5 / 4 - 1 / (2 * √2) * (1 / √2).cot - ε < ↑(distinctZeroCount T) / ↑(zeroCount T)

theorem ZetaZeros.simple_proportion_d4 (hRvM : RiemannVonMangoldt) (hPC : PairCorrelation) : ∃ (T₀ : ℝ), ∀ T ≥ T₀, 0.6725 < ↑(simpleOnLineCount T) / ↑(zeroCount T)

thm_simple_numeric. Beyond some height, more than 67.25% of the non-trivial zeros of the Riemann zeta function are simple and lie on the critical line.

theorem ZetaZeros.distinct_proportion_d5 (hRvM : RiemannVonMangoldt) (hPC : PairCorrelation) : ∃ (T₀ : ℝ), ∀ T ≥ T₀, 0.83625 < ↑(distinctZeroCount T) / ↑(zeroCount T)

thm_distinct_numeric. Beyond some height, more than 83.625% of the non-trivial zeros of the Riemann zeta function are distinct.