N(T)

Stream: PrimeNumberTheorem+

[Terence Tao]

Do we have (either in Mathlib or PNT+) some machinery to define N(T), the number of zeroes of zeta up to height T (counting multiplicity)? I am realizing that the effective prime number theorem literature relies at one point on effective Riemann-von Mangoldt functions, and am wondering if we already have any Lean code in this direction.

Closely related question: what is the best way to describe sums over non-trivial zeroes of zeta with multiplicity? From what I can tell, this notion hasn't yet been introduced into PNT, although a few of the lemmas in Strong PNT do mention sums or products over zeroes. Perhaps it is worth defining a set riemannZeta.nontrivial_zeroes : Set ℂ and a multiplicity function?

[Alex Kontorovich]

We don't have it in Mathlib or PNT+ (yet), but something like it (locally) exists in Gauss's Strong PNT repo, and would be very straightforward to add to PNT+. For example, see the definition of the set $K_f(R)$ of zeros of a function $f$ in a ball of radius $R$ about the origin. Then you can look, e.g., at their "Final Bound" Lemma 383 for how they use it in practice. There's the analyticOrderAt function in Mathlib for the multiplicity.

[Alex Kontorovich]

That doesn't mean it's the best way to implement such a thing. For example, their definition:

def zerosetKfR (R : ℝ) (hR : 0 < R) (f : ℂ → ℂ) : Set ℂ :=
  {ρ : ℂ | ρ ∈ Metric.closedBall (0 : ℂ) R ∧ f ρ = 0}

assumes hR which it should not (it should be an assumption in theorems, not definitions). This means the code using it is uglier than it should be...

[Terence Tao]

OK, for now I am going to put the following definitions in PrimaryDefinitions.lean:

noncomputable def riemannZeta.zeroes : Set ℂ := {s : ℂ | s ≠ 1 ∧ riemannZeta s = 0 } -- Explicitly excluded the pole at 1 to avoid issues with junk values

noncomputable def riemannZeta.zeroes_rect (I J: Set ℝ) : Set ℂ := { s : ℂ | s.re ∈ I ∧ s.im ∈ J ∧ s ∈ zeroes }

def WithTop.top_to_zero {α : Type*} [Zero α] (a : WithTop α) : α := match a with
| ⊤ => 0
| (some x) => x

noncomputable def riemannZeta.order (s : ℂ) : ℤ := (meromorphicOrderAt (riemannZeta) s).top_to_zero

and then work with sums of the form ∑' ρ : zeroes_rect I J, riemannZeta.order ρ * f ρfor various I J f, which are the expressions that show up a lot for me (and I expect will also show up elsewhere in PNT related work). We can rework the definitions later but this is probably good enough for now.

[Snir Broshi]

I think WithTop.top_to_zero is WithTop.untopD 0

[Alex Kontorovich]

Terence Tao said:

noncomputable def riemannZeta.zeroes : Set ℂ := {s : ℂ | s ≠ 1 ∧ riemannZeta s = 0 } -- Explicitly excluded the pole at 1 to avoid issues with junk values

I think it'll be cleaner if the definition doesn't explicitly exclude s = 1; we can develop API to remind Lean whenever needed that the junk value of $\zeta(s)$ at $s=1$ is not zero (which is in Mathlib).

[Alastair Irving]

Mathlib has some support for divisors of meromorphic functions so perhaps we should try and use that API where possible.