Riemann zeta function

Continuation and zeros of ζ, zero-free regions, moments and subconvexity, RH criteria (Robin, Lagarias), de Bruijn–Newman constant, zeta values.

• De Bruijn–Newman constant
• Euler's evaluations of odd zeta and Dirichlet beta series
• Moments and subconvexity of the zeta function
• Paperfolding series for odd zeta values
• Riemann xi function
• Robin's inequality
• Stieltjes constants
• Stride series for zeta and eta values
• Zero-free regions for the Riemann zeta function
• Zeros of the Riemann zeta function

TheoremFranel–Landau theorem#●ready to prove

For a natural number \(N\), let \(F_N(0) < F_N(1) < \dots < F_N(L_N - 1)\) be the terms of the Farey sequence of order \(N\), and for \(k < L_N\) let \(\delta_{N,k} = F_N(k) - k/(L_N - 1)\). The Riemann hypothesis holds if and only if for every real \(\varepsilon > 0\), \(\sum_{k=0}^{L_N - 1} \delta_{N,k}^2 = O(N^{-1+\varepsilon})\) as \(N \to \infty\).

theorem_wanted franel_landau :
    RiemannHypothesis ↔
      ∀ ε : ℝ, 0 < ε →
        (fun N : ℕ => ∑ k : Fin (Farey.fareySeq N).length,
          ((((Farey.fareySeq N).get k : ℚ) : ℝ) -
            ((k : ℕ) : ℝ) / (((Farey.fareySeq N).length - 1 : ℕ) : ℝ)) ^ 2)
            =O[Filter.atTop]
        (fun N : ℕ => (N : ℝ) ^ (-1 + ε))

Sources

• https://en.wikipedia.org/wiki/Farey_sequence.

Uses 1

Statement usesFarey sequence

TheoremKachi–Tzermias infinite products for \(\zeta(3)\)#✓fully proved

Let \(\zeta\) be the Riemann zeta function and, for \(n \ge 1\), put \(a_n = \left(1 - \frac{1}{n+1}\right)^{(-1)^n n(n+1)/2}\). Then, as \(m \to \infty\),

\[\prod_{n=1}^{2m+1} e^{-1/4} a_n \to \exp\left(\frac{7\zeta(3)}{4\pi^2} + \frac{1}{4}\right), \qquad \prod_{n=1}^{2m} e^{1/4} a_n \to \exp\left(\frac{7\zeta(3)}{4\pi^2} - \frac{1}{4}\right),\]

and

\[\left(\prod_{n=1}^{m} \frac{(2n)^{(2n)^2}}{(2n-1)^{(2n-1)^2}}\right)^4 \left(\frac{(2m+2)^{4m+5}}{(2m+1)^{12m+9}}\right)^m \to \exp\left(\frac{7\zeta(3)}{\pi^2}\right).\]

MetaMathlibExt.zeta_three_infinite_product_formulas · 27 lines

public theorem zeta_three_infinite_product_formulas :
    Filter.Tendsto
      (fun m : ℕ =>
        ∏ n ∈ Finset.Icc 1 (2 * m + 1),
          (1 / Real.rpow (Real.exp 1) (1 / 4)) *
            (1 - 1 / ((n + 1 : ℕ) : ℝ)) ^
              (((n * (n + 1) / 2 : ℕ) : ℤ) * (-1 : ℤ) ^ n))
      Filter.atTop
      (nhds (Real.exp (7 * (riemannZeta (3 : ℂ)).re / (4 * Real.pi ^ 2) + 1 / 4))) ∧
    Filter.Tendsto
      (fun m : ℕ =>
        ∏ n ∈ Finset.Icc 1 (2 * m),
          Real.rpow (Real.exp 1) (1 / 4) *
            (1 - 1 / ((n + 1 : ℕ) : ℝ)) ^
              (((n * (n + 1) / 2 : ℕ) : ℤ) * (-1 : ℤ) ^ n))
      Filter.atTop
      (nhds (Real.exp (7 * (riemannZeta (3 : ℂ)).re / (4 * Real.pi ^ 2) - 1 / 4))) ∧
    Filter.Tendsto
      (fun m : ℕ =>
        ((∏ n ∈ Finset.Icc 1 m,
            (((2 * n : ℕ) : ℝ) ^ ((2 * n : ℕ) ^ 2))) /
          (∏ n ∈ Finset.Icc 1 m,
            (((2 * n - 1 : ℕ) : ℝ) ^ ((2 * n - 1 : ℕ) ^ 2)))) ^ 4 *
        ((((2 * m + 2 : ℕ) : ℝ) ^ (4 * m + 5)) /
          (((2 * m + 1 : ℕ) : ℝ) ^ (12 * m + 9))) ^ m)
      Filter.atTop
      (nhds (Real.exp (7 * (riemannZeta (3 : ℂ)).re / Real.pi ^ 2)))

Sources

• Yasuyuki Kachi and Pavlos Tzermias, "Infinite Products Involving zeta(3) and Catalan's Constant," Journal of Integer Sequences 15 (2012), Article 12.9.4, Proposition zeta3, equations zeta3i–zeta3iii, lines 124–144, https://cs.uwaterloo.ca/journals/JIS/VOL15/Tzermias/tzermias2.tex.

Uses 3

Proof usesClausen functions of order at least two as series (Chapter 9, Entry 13) · Clausen function of order one (Chapter 9, Entry 13) · Integrals of \(u^n \cot(u/2)\) via Clausen functions (Chapter 9, Entry 13)

TheoremLagarias' elementary criterion for the Riemann hypothesis#●ready to prove

The Riemann hypothesis holds (every zero \(s\) of the Riemann zeta function with \(s \ne 1\) that is not one of the trivial zeros \(-2, -4, -6, \dots\) has real part \(1/2\)) if and only if, for every positive integer \(n\),

\[\sigma(n) \le H_n + e^{H_n} \log H_n,\]

where \(\sigma(n)\) is the sum of the positive divisors of \(n\) and \(H_n = \sum_{k=1}^{n} 1/k\) is the \(n\)-th harmonic number.

public theorem_wanted riemann_hypothesis_iff_lagarias_elementary_criterion :
    RiemannHypothesis ↔ LagariasElementaryCriterion

Sources

• https://arxiv.org/abs/math/0008177. Problem riemann_hypothesis_iff_lagarias_elementary_criterion of the lean-eval benchmark.

TheoremMeromorphy of the Riemann zeta function#✓fully proved

The Riemann zeta function \(\zeta\) is meromorphic on all of \(\mathbb{C}\).

theorem meromorphicOn_riemannZeta : MeromorphicOn riemannZeta Set.univ

Used by 4

Used byRamanujan's distribution relation for the power-difference function · The Entry 10 zeta factor in Bernoulli form · Ramanujan's corollary to Entry 10 of Chapter 7 · Ramanujan's formula for the alternating zeta function at \(-r\)

TheoremRamanujan's formula for the alternating zeta function at \(-r\)#✓fully proved

Let \(\eta(s) = (1 - 2^{1-s})\,\zeta(s)\) for \(s \ne 1\) and \(\eta(1) = \log 2\), where \(\zeta\) is the Riemann zeta function, and let \(B^*(z) = 2\,\Gamma(z + 1)\,\zeta(z) / (2\pi)^z\). Then for every \(s \in \mathbb{C}\) with \(\mathrm{Re}\, s > 0\) the partial sums \(\sum_{j=0}^{N-1} (-1)^j / (j+1)^s\) tend to \(\eta(s)\) as \(N \to \infty\); the functions \(r \mapsto \eta(-r)\) and \(r \mapsto (2^{r+1} - 1)\, B^*(r + 1) \sin(\pi r/2) / (r + 1)\) are meromorphic on \(\mathbb{C}\); and these two functions agree outside a closed discrete subset of \(\mathbb{C}\).

theorem ramanujan_part1_ch7_entry2_faulhaber :
    (∀ s : ℂ, 0 < s.re →
      Tendsto (chapter7EtaPartialSum s) atTop (𝓝 (chapter7Eta s))) ∧
      MeromorphicOn (fun r : ℂ => chapter7Eta (-r)) Set.univ ∧
      MeromorphicOn chapter7Entry2Value Set.univ ∧
      (fun r : ℂ => chapter7Eta (-r)) =ᶠ[codiscrete ℂ] chapter7Entry2Value

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 7.

Uses 1

Proof usesMeromorphy of the Riemann zeta function

3 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.