A Poisson L² Lower Bound for Weil-Square Test Functions at Mesoscopic Bandwidth
Mathematics verified. Core theorems are machine-checked in Lean 4.
Prose and presentation may not have been human-reviewed.
Summary
Let `L = L(T) > 0` and `η_*(T) = (1/2 + η/2) \log\log T / \log T`
for `T \to \infty` and a fixed `η \in (0, 1/2)`.
Length
4,260 words
Claims
1 theorems
Status
Draft
Target
Proceedings of the American Mathematical Society