[Merged by Bors] - feat(NumberTheory): zeros of Riemann zeta on compact sets are finite

[Yu-Misaka]

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

---

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary 599a2dc81b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.NumberTheory.LSeries.ZetaZeros (new file)	3222

---

Declarations diff

+ IsCompact.inter_riemannZetaZeros_finite
+ _root_.riemannZeta_eventually_ne_zero_nhds_one
+ analyticOn_riemannZeta
+ compl_riemannZetaZeros_mem_codiscrete
+ differentiableOn_riemannZeta
+ isClosed_riemannZetaZeros
+ isDiscrete_riemannZetaZeros
+ mem_riemannZetaZeros
+ riemannZetaZeros
+ riemannZetaZeros_codiscreteWithin_compl_one
+ tendsto_riemannZeta_cofinite_cocompact

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[Copilot]

Pull request overview

This PR adds a new result to the L-series / zeta-function development showing that the zero set of riemannZeta is locally finite in ℂ (in particular, any compact set meets it in finitely many points), supporting downstream Prime Number Theorem developments.

Changes:

• Add Mathlib/NumberTheory/LSeries/ZetaZeros.lean proving riemannZeta_zeroes_on_Compact_finite.
• Add analytic/differentiability lemmas for riemannZeta on {1}ᶜ to support discreteness arguments.
• Add a punctured-neighborhood lemma riemannZeta_eventually_ne_zero near s = 1 to handle the excluded singularity.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 3 comments.

File	Description
Mathlib/NumberTheory/LSeries/ZetaZeros.lean	New proof that compact subsets of ℂ contain only finitely many zeros of riemannZeta.
Mathlib/NumberTheory/LSeries/RiemannZeta.lean	Adds differentiableOn_riemannZeta and analyticOn_riemannZeta on {1}ᶜ for use by analytic/discreteness lemmas.
Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean	Adds riemannZeta_eventually_ne_zero near s = 1 (punctured neighborhood).

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[plp127]

Surely none of this is specific to the riemann zeta function?

[loefflerd]

As Aaron points out, none of this is specific to Riemann zeta – it would apply to any non-constant meromorphic function – but unfortunately we do not yet have a proof that zeta is meromorphic, since Komyyyy's PR #27500 hasn't yet landed.

[loefflerd]

Here are a few golfing suggestions. I also think the AI review bot makes a good suggestion that we should have a lemma explicitly saying the Riemann zeros are discrete (& then we can perhaps make the statement about discreteness within {1}^c private).

[loefflerd]

I couldn't resist going back to this because I had a hunch there was a more direct method. Here's a version which directly deduces that the zeta zeroes are closed and discrete, and then shows they have finite intersection with any compact set from that.

[Yu-Misaka]

Thanks for the review and suggestions! I've implemented them all.

Sorry I didn't know Komyyyy's PR, for sure none of this is specific to Riemann zeta. So I wonder if it is better to move these lemmas somewhere else instead of creating a separate file.

And also, since Komyyyy has proven that riemannZeta is meromorphic, should we also have something like this?

variable {f : ℂ → ℂ} {U : Set ℂ} (hf : MeromorphicOn f U) (hU : IsCompact U)
  (hne : ∀ u : U, meromorphicOrderAt f u ≠ ⊤)

example : (U ∩ f ⁻¹' {0}).Finite := sorry

(I wrote a small example of the proof here)

[loefflerd]

The build is failing because of some unrelated glitch; merging the latest master should fix that.

BTW, I overlooked before that the spelling is slightly inconsistent between "zeros" and "zeroes". I believe "zeros" is the more common spelling (but it is not so important which we standardize on, the main thing is that we should choose one and stick with it).

Re Komyyy's PR: that PR has been "work in progress" for some months now, so I suggest not blocking this one on it.

[loefflerd]

I think this is good now modulo a minor naming suggestion

maintainer delegate

[loefflerd]

You could name this as IsCompact.inter_riemannZeta_zeros_finite so it can be used with dot notation. In any case please update the file-level docstring to match the actual lemma name

[loefflerd]

(see above)

[github-actions]

🚀 Pull request has been placed on the maintainer queue by loefflerd.

[ocfnash]

I'd be interested in @loefflerd 's opinion on whether we should add the following definition to this file:

/-- The zeros of Riemann's ζ-function. -/
def riemannZetaZero : Set ℂ := riemannZeta ⁻¹' {0}

lemma mem_riemannZetaZero {z : ℂ} :
    z ∈ riemannZetaZero ↔ riemannZeta z = 0 := by
  simp [riemannZetaZero]

Ordinarily we would not make such a thin definition but for something as important as this set, I for one would be in favour.

[loefflerd]

I'd be interested in @loefflerd 's opinion on whether we should add the following definition to this file:

/-- The zeros of Riemann's ζ-function. -/
def riemannZetaZero : Set ℂ := riemannZeta ⁻¹' {0}

lemma mem_riemannZetaZero {z : ℂ} :
    z ∈ riemannZetaZero ↔ riemannZeta z = 0 := by
  simp [riemannZetaZero]

Sure, that makes sense! At some point in future either Mathlib, or downstream projects (PNT+ perhaps?) might want to formalize zero-free regions, estimates for the density of the zeros, etc so it makes sense to have this defined. Very minor nit: I'd suggest calling it riemannZetaZeros (plural).

[ocfnash]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Post-Build Step
• ci (staging) / Lint style
• ci (staging) / Post-CI job