Zeros of the Riemann zeta function

DefinitionZero-counting function of the Riemann zeta function#✓fully proved

For a real number \(T\), \(N(T)\) is the number of zeros \(\rho = \beta + i\gamma\) of the Riemann zeta function with \(0 < \beta < 1\) and \(0 < \gamma \le T\), each counted with its multiplicity as a zero.

MetaMathlibExt.zetaZeroCount · 24 lines

noncomputable def zetaZeroCount (T : ℝ) : ℕ :=
  have hfin : (riemannZetaZeros ∩ {s : ℂ | 0 < s.re ∧ s.re < 1 ∧ 0 < s.im ∧ s.im ≤ T}).Finite := by
    have hsub : (riemannZetaZeros ∩ {s : ℂ | 0 < s.re ∧ s.re < 1 ∧ 0 < s.im ∧ s.im ≤ T})
        ⊆ Metric.closedBall 0 (|T| + 2) ∩ riemannZetaZeros := by
      intro ρ h
      obtain ⟨hmem, hre0, hre1, him0, himT⟩ := h
      refine ⟨?_, hmem⟩
      rw [Metric.mem_closedBall, dist_zero_right]
      have hre : |ρ.re| < 1 := abs_lt.mpr ⟨by linarith, hre1⟩
      have him : |ρ.im| ≤ |T| :=
        abs_le.mpr ⟨by linarith [abs_nonneg T], le_trans himT (le_abs_self T)⟩
      have h1 : ρ.re ^ 2 ≤ 1 := by nlinarith [hre0, hre1]
      have h2 : ρ.im ^ 2 ≤ T ^ 2 := sq_le_sq.mpr him
      have hnorm : ‖ρ‖ ^ 2 = ρ.re ^ 2 + ρ.im ^ 2 := by
        rw [← Complex.normSq_eq_norm_sq, Complex.normSq_apply]
        ring
      have h3 : ‖ρ‖ ^ 2 ≤ (|T| + 2) ^ 2 := by
        rw [hnorm]
        nlinarith [h1, h2, sq_abs T, abs_nonneg T]
      have h4 := sq_le_sq.mp h3
      rwa [abs_of_nonneg (norm_nonneg ρ), abs_of_nonneg (by positivity : (0 : ℝ) ≤ |T| + 2)] at h4
    exact (isCompact_closedBall 0 _).inter_riemannZetaZeros_finite.subset hsub
  Finset.sum hfin.toFinset
    (fun ρ => (WithTop.untopD 0 (meromorphicOrderAt riemannZeta ρ)).toNat)

Used by 2

Used byFirst Bellotti–Wong bound on the zero-counting function · Second Bellotti–Wong bound on the zero-counting function

TheoremFirst Bellotti–Wong bound on the zero-counting function#●ready to prove

For every real number \(T \ge e\), the number \(N(T)\) of zeros \(\rho = \beta + i\gamma\) of the Riemann zeta function with \(0 < \beta < 1\) and \(0 < \gamma \le T\), counted with multiplicity, satisfies

\[ N(T) \le \frac{T}{2\pi} \log \frac{T}{2\pi e} + 0.10076 \log T + 0.24460 \log \log T + 8.08344. \]

This bound is sharper than the second Bellotti–Wong bound for \(T\) above about \(e^{447.981}\).

public theorem_wanted bellotti_wong_zero_count_bound (T : ℝ) (hT : Real.exp 1 ≤ T) :
    (zetaZeroCount T : ℝ) ≤ T / (2 * Real.pi) * Real.log (T / (2 * Real.pi * Real.exp 1))
      + 0.10076 * Real.log T + 0.24460 * Real.log (Real.log T) + 8.08344

Uses 1

Statement usesZero-counting function of the Riemann zeta function

TheoremSecond Bellotti–Wong bound on the zero-counting function#●ready to prove

For every real number \(T \ge e\), the number \(N(T)\) of zeros \(\rho = \beta + i\gamma\) of the Riemann zeta function with \(0 < \beta < 1\) and \(0 < \gamma \le T\), counted with multiplicity, satisfies

\[ N(T) \le \frac{T}{2\pi} \log \frac{T}{2\pi e} + 0.11200 \log T + 0.12567 \log \log T + 3.77417. \]

This bound is sharper than the first Bellotti–Wong bound for \(T\) below about \(e^{447.981}\).

public theorem_wanted bellotti_wong_zero_count_bound_small (T : ℝ) (hT : Real.exp 1 ≤ T) :
    (zetaZeroCount T : ℝ) ≤ T / (2 * Real.pi) * Real.log (T / (2 * Real.pi * Real.exp 1))
      + 0.11200 * Real.log T + 0.12567 * Real.log (Real.log T) + 3.77417

Uses 1

Statement usesZero-counting function of the Riemann zeta function

TheoremPlatt–Trudgian verification of the Riemann hypothesis to height \(3 \cdot 10^{12}\)#●ready to prove

Every zero \(\rho\) of the Riemann zeta function with \(0 < \operatorname{Im} \rho \le 3000175332800\) satisfies \(\operatorname{Re} \rho = 1/2\).

public theorem_wanted platt_trudgian_rh_to_height (ρ : ℂ)
    (hzero : riemannZeta ρ = 0) (hpos : 0 < ρ.im)
    (hlt : ρ.im ≤ 3000175332800) :
    ρ.re = 1 / 2

1 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.