Zero-free regions for the Riemann zeta function

TheoremKadiri's zero-free region for the Riemann zeta function#●ready to prove

Let \(\zeta\) be the Riemann zeta function and \(\log\) the natural logarithm. For every complex number \(s = \sigma + it\) with \(|t| \ge 2\) and \(\sigma \ge 1 - \frac{1}{5.70176 \log |t|}\), we have \(\zeta(s) \ne 0\).

public theorem_wanted kadiri_zero_free_region (s : ℂ)
    (ht : 2 ≤ |s.im|)
    (hσ : 1 - 1 / (5.70176 * Real.log |s.im|) ≤ s.re) :
    riemannZeta s ≠ 0

TheoremKadiri's refined zero-free region for the Riemann zeta function#●ready to prove

Let \(\zeta\) be the Riemann zeta function and \(\log\) the natural logarithm. For every complex number \(s = \sigma + it\) with \(|t| \ge 2\) and \(\sigma \ge 1 - \frac{1}{5.69693 \log |t|}\), we have \(\zeta(s) \ne 0\).

public theorem_wanted kadiri_zero_free_region_refined (s : ℂ)
    (ht : 2 ≤ |s.im|)
    (hσ : 1 - 1 / (5.69693 * Real.log |s.im|) ≤ s.re) :
    riemannZeta s ≠ 0

Sources

• Kadiri's refined constant as cited in Dusart 2016; this is the region required by dusart2016_tail_theorem.

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.