Discreteness of the zeros of the Riemann zeta function

We show that the zeros of the Riemann zeta function form a discrete subset of ℂ, so that in particular any compact subset of ℂ contains only finitely many zeros.

Main declarations

• riemannZetaZeros: The zeros of Riemann zeta function.

Main results

• isClosed_riemannZetaZeros: riemannZetaZeros is closed.

• isDiscrete_riemannZetaZeros: riemannZetaZeros is discrete.

• IsCompact.inter_riemannZetaZeros_finite: for any compact set S : Set ℂ, the intersection S ∩ riemannZetaZeros is finite.

def riemannZetaZeros : Set ℂ

The zeros of Riemann's ζ-function.

Equations

• riemannZetaZeros = riemannZeta ⁻¹' {0}

theorem mem_riemannZetaZeros {z : ℂ} : z ∈ riemannZetaZeros ↔ riemannZeta z = 0

theorem isClosed_riemannZetaZeros : IsClosed riemannZetaZeros

theorem isDiscrete_riemannZetaZeros : IsDiscrete riemannZetaZeros

theorem IsCompact.inter_riemannZetaZeros_finite {S : Set ℂ} (hS : IsCompact S) : (S ∩ riemannZetaZeros).Finite

Any compact subset of ℂ contains only finitely many zeros of the Riemann zeta function.

theorem tendsto_riemannZeta_cofinite_cocompact : Filter.Tendsto Subtype.val Filter.cofinite (Filter.cocompact ℂ)