feat(NumberTheory): zeros of Riemann zeta on compact sets are finite (leanprover-community#37328)

Greetings! This PR proves that any compact subset of `ℂ` meets the zero set of the Riemann zeta function in only finitely many points (`riemannZeta_zeroes_on_Compact_finite`). This result in used in AlexKontorovich/PrimeNumberTheoremAnd#750

Author: Yu-Misaka

Mathlib.lean

@@ -5558,6 +5558,7 @@ public import Mathlib.NumberTheory.LSeries.PrimesInAP
 public import Mathlib.NumberTheory.LSeries.RiemannZeta
 public import Mathlib.NumberTheory.LSeries.SumCoeff
 public import Mathlib.NumberTheory.LSeries.ZMod
+public import Mathlib.NumberTheory.LSeries.ZetaZeros
 public import Mathlib.NumberTheory.LegendreSymbol.AddCharacter
 public import Mathlib.NumberTheory.LegendreSymbol.Basic
 public import Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean

@@ -420,6 +420,10 @@ lemma _root_.riemannZeta_one_ne_zero : riemannZeta 1 ≠ 0 := by
     exact (lt_trans Real.exp_one_lt_d9 (by norm_num)).trans_le
       <| mul_le_mul_of_nonneg_left two_le_pi (by simp)
 
+lemma _root_.riemannZeta_eventually_ne_zero_nhds_one : ∀ᶠ s in 𝓝 1, riemannZeta s ≠ 0 := by
+  filter_upwards [eventually_nhdsWithin_iff.1 <| riemannZeta_residue_one.eventually_ne one_ne_zero]
+  grind [riemannZeta_one_ne_zero]
+
 end val_at_one
 
 end ZetaAsymptotics

Mathlib/NumberTheory/LSeries/RiemannZeta.lean

@@ -137,6 +137,14 @@ lemma HurwitzZeta.expZeta_zero : expZeta 0 = riemannZeta := by
 theorem differentiableAt_riemannZeta {s : ℂ} (hs' : s ≠ 1) : DifferentiableAt ℂ riemannZeta s :=
   differentiableAt_hurwitzZetaEven _ hs'
 
+lemma differentiableOn_riemannZeta :
+    DifferentiableOn ℂ riemannZeta {1}ᶜ :=
+  fun _ hs ↦ (differentiableAt_riemannZeta hs).differentiableWithinAt
+
+lemma analyticOn_riemannZeta :
+    AnalyticOnNhd ℂ riemannZeta {1}ᶜ :=
+  differentiableOn_riemannZeta.analyticOnNhd isOpen_compl_singleton
+
 /-- We have `ζ(0) = -1 / 2`. -/
 theorem riemannZeta_zero : riemannZeta 0 = -1 / 2 := by
   simp_rw [riemannZeta, hurwitzZetaEven, Function.update_self, if_true]

Mathlib/NumberTheory/LSeries/ZetaZeros.lean

@@ -0,0 +1,74 @@
+/-
+Copyright (c) 2026 Huanyu Zheng. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Huanyu Zheng
+-/
+module
+
+public import Mathlib.NumberTheory.LSeries.Nonvanishing
+
+/-!
+# 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.
+-/
+
+@[expose] public section
+
+/-- The zeros of Riemann's ζ-function. -/
+def riemannZetaZeros : Set ℂ := riemannZeta ⁻¹' {0}
+
+lemma mem_riemannZetaZeros {z : ℂ} :
+    z ∈ riemannZetaZeros ↔ riemannZeta z = 0 := .rfl
+
+/-- The complement of the zero set of `riemannZeta` is codiscrete within `{1}ᶜ`. -/
+private lemma riemannZetaZeros_codiscreteWithin_compl_one :
+    riemannZetaZerosᶜ ∈ Filter.codiscreteWithin {1}ᶜ := by
+  refine analyticOn_riemannZeta.preimage_zero_mem_codiscreteWithin (x := 2) ?_ (by simp) ?_
+  · exact riemannZeta_ne_zero_of_one_le_re Nat.one_le_ofNat
+  · exact isConnected_compl_singleton_of_one_lt_rank (by simp) 1
+
+/-- The complement of the zero set of `riemannZeta` is codiscrete. -/
+private lemma compl_riemannZetaZeros_mem_codiscrete :
+    riemannZetaZerosᶜ ∈ Filter.codiscrete ℂ := by
+  have := riemannZetaZeros_codiscreteWithin_compl_one
+  simp only [mem_codiscreteWithin, Set.mem_compl_iff, Set.mem_singleton_iff, sdiff_compl,
+    Set.inf_eq_inter, Filter.disjoint_principal_right, mem_codiscrete, compl_compl] at this ⊢
+  intro x
+  rcases eq_or_ne x 1 with rfl | hx
+  · exact riemannZeta_eventually_ne_zero_nhds_one.filter_mono nhdsWithin_le_nhds
+  · exact Filter.mem_of_superset (this x hx)
+      (by grind [riemannZeta_one_ne_zero, mem_riemannZetaZeros])
+
+lemma isClosed_riemannZetaZeros : IsClosed riemannZetaZeros :=
+  by simpa using (mem_codiscrete'.mp compl_riemannZetaZeros_mem_codiscrete).1
+
+lemma isDiscrete_riemannZetaZeros : IsDiscrete riemannZetaZeros :=
+  by simpa using (mem_codiscrete'.mp compl_riemannZetaZeros_mem_codiscrete).2
+
+/-- Any compact subset of `ℂ` contains only finitely many zeros of the Riemann zeta function. -/
+lemma IsCompact.inter_riemannZetaZeros_finite {S : Set ℂ} (hS : IsCompact S) :
+    (S ∩ riemannZetaZeros).Finite := by
+  apply (hS.inter_right isClosed_riemannZetaZeros).finite
+  exact isDiscrete_riemannZetaZeros.mono Set.inter_subset_right
+
+open Filter in
+lemma tendsto_riemannZeta_cofinite_cocompact :
+    Tendsto ((↑) : riemannZetaZeros → ℂ) cofinite (cocompact ℂ) :=
+  isClosed_riemannZetaZeros.tendsto_coe_cofinite_of_isDiscrete isDiscrete_riemannZetaZeros
+
+end