Dobner's Lemma 3: a zero with a nonvanishing surrounding circle

Proved

DeBruijnNewman.Dobner.zeta_zero_disk

by adobner · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisnumber-theoryriemann-hypothesis

Fix $t<0$ , and let

Z_t(s)=\sum_{n=1}^{\infty}\exp\!\left(\frac{t}{4}\log^2n\right)n^{-s}.

There exist a center $c\in\mathbb C$ , a radius $r>0$ , and a constant $\delta>0$ such that

Z_t(c)=0, \qquad \delta\leq |Z_t(s)|\quad\text{whenever }|s-c|=r.

This combines the zero-existence conclusion of Dobner's Lemma 3 with the nonvanishing circle chosen in Section 3.1. The positive boundary margin allows the zero to persist under sufficiently small holomorphic perturbations.

Preamble

import Definitions.Def_DeBruijnNewman_Dobner
open Metric

Formal statement

theorem DeBruijnNewman.Dobner.zeta_zero_disk (t : ℝ) (ht : t < 0) :
    ∃ (c : ℂ) (r δ : ℝ), 0 < r ∧ 0 < δ ∧
      DeBruijnNewman.Dobner.zetaT t c = 0 ∧
      ∀ s ∈ sphere c r, δ ≤ ‖DeBruijnNewman.Dobner.zetaT t s‖ := by sorry

Source

Alexander Dobner, A proof of Newman's conjecture for the extended Selberg class, arXiv:2005.05142v2 (10 January 2026), https://arxiv.org/abs/2005.05142v2, Lemma 3: statement p. 15, proof p. 29; the choice of the circle and its positive minimum is in Section 3.1, p. 14. Specialized to F = zeta.

View graph