Papers With

← All papers
First page of Cofinite Zeros of High Derivatives

Cofinite Zeros of High Derivatives

Eric Hou

math.CV Jul 23, 2026 · v5
formalization mathlib analysis probability
Read PDF arXiv abstract Code
TL;DR
The main theorem and its supporting estimates are machine-checked in Lean 4 with Mathlib, with a public repository and no sorry or custom axioms.
Abstract
We give a bounded-coefficient probabilistic construction of a transcendental entire function $f$ of order two such that every nonempty open subset of the complex plane contains a zero of $f^{(n)}$ for all sufficiently large $n$. This gives an affirmative answer to the transcendental form of Erdős Problem 906. Thus every fixed disk is zero-free for only finitely many successive derivatives. The function satisfies $|f(z)|\leq\sqrt2\exp(|z|^2)$ and is a counterexample to a theorem of Boas and Reddy as printed.
Problem

Erdős Problem 906 asks, in its transcendental form, whether there is a transcendental entire function such that every open set contains a zero of f^(n) for all sufficiently large n. A related printed theorem of Boas and Reddy asserts that functions of order at most 2 and finite type have some disk on which infinitely many derivatives are zero-free.

Approach

The construction is a random Fock series f(z)=Σ ξ_k z^k/√(k!) with independent coefficients uniform on the closed unit disk. Saddle-point estimates on the derivatives, combined with Jensen's formula, bound hole probabilities by summable stretched-exponential terms. A countable-base reduction and Borel–Cantelli-style extraction then yield a deterministic witness. The full argument is formalized in Lean 4.28.0 with Mathlib.

Results

There is a transcendental entire function with |f(z)| ≤ √2 exp(|z|^2) such that every open set contains zeros of f^(n) for all large n. This answers Erdős Problem 906 and shows Theorem 1 of Boas and Reddy is false as printed. The Lean development certifies the cofinite conclusion and the growth bound for the same witness.