De Bruijn–Newman constant

DefinitionSummands of Newman's kernel#✓fully proved

For real \(u\) and a natural number \(n\), the \(n\)-th summand of Newman's kernel, counted from \(n = 0\), is

\[\left(2\pi^2 (n+1)^4 e^{9u} - 3\pi (n+1)^2 e^{5u}\right) e^{-\pi (n+1)^2 e^{4u}}.\]

noncomputable def phiTerm (u : ℝ) (n : ℕ) : ℝ :=
  (2 * π ^ 2 * (n + 1 : ℝ) ^ 4 * Real.exp (9 * u) -
    3 * π * (n + 1 : ℝ) ^ 2 * Real.exp (5 * u)) *
    Real.exp (-π * (n + 1 : ℝ) ^ 2 * Real.exp (4 * u))

Used by 1

Used byNewman's kernel

DefinitionNewman's kernel#✓fully proved

For real \(u\), Newman's kernel is the sum of the series

\[\Phi(u) = \sum_{n=1}^{\infty} (2\pi^2 n^4 e^{9u} - 3\pi n^2 e^{5u}) e^{-\pi n^2 e^{4u}},\]

which converges absolutely for every real \(u\).

noncomputable def phi (u : ℝ) : ℝ :=
  ∑' n : ℕ, phiTerm u n

Uses 1 · Used by 1

Statement usesSummands of Newman's kernel

Used byThe de Bruijn–Newman deformation

DefinitionThe de Bruijn–Newman deformation#✓fully proved

For real \(\lambda\) and complex \(z\),

\[H_\lambda(z) = \int_0^\infty e^{\lambda u^2}\, \Phi(u) \cos(zu)\, du,\]

where \(\Phi\) is Newman's kernel and the integral runs over \(u > 0\).

The integral is a Lebesgue integral, taken to be \(0\) when the integrand is not integrable.

noncomputable def H (lam : ℝ) (z : ℂ) : ℂ :=
  ∫ u in Set.Ioi (0 : ℝ), ((Real.exp (lam * u ^ 2) * phi u : ℝ) : ℂ) *
    Complex.cos (z * (u : ℂ))

Uses 1 · Used by 1

Statement usesNewman's kernel

Used byReal-rootedness of the de Bruijn–Newman deformation

DefinitionReal-rootedness of the de Bruijn–Newman deformation#✓fully proved

For real \(\lambda\), this is the statement that every zero of the de Bruijn–Newman deformation \(H_\lambda\) is real: every complex \(z\) with \(H_\lambda(z) = 0\) has imaginary part \(0\).

def ZerosAllReal (lam : ℝ) : Prop :=
  ∀ z : ℂ, H lam z = 0 → z.im = 0

Uses 1 · Used by 3

Statement usesThe de Bruijn–Newman deformation

Used byThe de Bruijn–Newman constant · All zeros of the de Bruijn–Newman deformation are real at time 1/5 · Nonreal zeros of the de Bruijn–Newman deformation at negative times

DefinitionThe de Bruijn–Newman constant#✓fully proved

The de Bruijn–Newman constant \(\Lambda\) is the infimum of the set of real numbers \(\lambda\) such that every zero of the de Bruijn–Newman deformation \(H_\lambda\) is real. The infimum is taken in \(\mathbb{R}\), with the convention that it is \(0\) when this set is empty or not bounded below.

Newman's theorem, that every zero of \(H_\lambda\) is real exactly when \(\lambda \ge \Lambda\), is not part of this definition.

noncomputable def deBruijnNewmanConstant : ℝ :=
  sInf { lam : ℝ | ZerosAllReal lam }

Uses 1

Statement usesReal-rootedness of the de Bruijn–Newman deformation

TheoremNonreal zeros of the de Bruijn–Newman deformation at negative times#●ready to prove

For every real \(\lambda < 0\), not every zero of the de Bruijn–Newman deformation \(H_\lambda\) is real: there is a complex \(z\) with \(H_\lambda(z) = 0\) and nonzero imaginary part.

theorem_wanted rodgersTaoNegativeTime_wanted :
    ∀ lam : ℝ, lam < 0 → ¬ ZerosAllReal lam

Sources

• Rodgers and Tao, The de Bruijn--Newman constant is non-negative, Forum Math. Pi 8 (2020): at every negative deformation time, H has a nonreal zero.

Uses 1

Statement usesReal-rootedness of the de Bruijn–Newman deformation

TheoremAll zeros of the de Bruijn–Newman deformation are real at time 1/5#●ready to prove

Every zero of the de Bruijn–Newman deformation \(H_{1/5}\) is real: every complex \(z\) with \(H_{1/5}(z) = 0\) has imaginary part \(0\).

theorem_wanted plattTrudgianUpperBound_wanted :
    ZerosAllReal (1 / 5 : ℝ)

Sources

• Platt and Trudgian, The Riemann hypothesis is true up to 3·10¹², Bull. Lond. Math. Soc. 53 (2021), via the Polymath15 criterion: at time 1 / 5 all zeros of H are real (catalogue upper bound 0.2).

Uses 1

Statement usesReal-rootedness of the de Bruijn–Newman deformation

5 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.