The negative-time De Bruijn–Newman heat integral is entire

Proved

DeBruijnNewman.H_entire_negative

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

analysiscomplex-analysisnumber-theory

For every real $t<0$ , the canonical De Bruijn–Newman heat integral

H_t(z)=\int_0^\infty e^{tu^2}\Phi(u)\cos(zu)\,du

is an entire function of $z\in\mathbb C$ , where

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

This gives the holomorphy needed to study the negative-time deformations and their normalized versions. Only negative time is asserted; the theorem uses the existing integral definition of the heat flow.

Formalization Note. Entirety is expressed as complex differentiability at every point of $\mathbb C$ .

Preamble

import Definitions.Def_DeBruijnNewman_core

Formal statement

theorem DeBruijnNewman.H_entire_negative (t : ℝ) (ht : t < 0) :
    Differentiable ℂ (DeBruijnNewman.H t) := 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, Introduction's theta kernel and deformed Fourier integral, pp. 2–3; holomorphy used in Section 3.1, p. 14. The submitted proof establishes the negative-time case directly by Gaussian domination.

View graph