Transfer of the Hilbert-space inequalities to zeta zeros

Conjugation invariance of the rescaled zero multiset, the identification of its finite kernel sum with the canonical sum over zeros, and the transfer of the two abstract finite-set inequalities to the three zero-counting functions.

theorem ZetaZeros.simpleOnLineCount_lower {lam T : ℝ} {eta : ℝ → ℝ} (hT : 1 < T) (hη : IsAdmissible lam eta) : 2 * ↑(zeroCount T) - (unweightedKernelSum eta T).re ≤ ↑(simpleOnLineCount T)

The finite-set lower bound transferred to simple zeros on the critical line.

theorem ZetaZeros.distinctZeroCount_lower {lam T : ℝ} {eta : ℝ → ℝ} (hT : 1 < T) (hη : IsAdmissible lam eta) : 3 / 2 * ↑(zeroCount T) - (unweightedKernelSum eta T).re / 2 ≤ ↑(distinctZeroCount T)

The finite-set lower bound transferred to distinct zeros.