Ryota Mori

Weil positivity on the window of width log 15

Weil's criterion states that the Riemann Hypothesis holds if and only if Weil's quadratic form Q is nonnegative on all admissible test functions. Restricting the support to a fixed interval [−L, L] gives a weaker, unconditional question. We prove that Q(f) ≥ 2−2904‖f‖22 for every...

A μ^{9/2} log μ upper bound for windowed Weil forms

Let λmin(λ) be the bottom of the spectrum of Weil's quadratic form restricted to test functions supported in the multiplicative window [λ−1,λ], and put μ=λ2. By Weil's criterion, the Riemann Hypothesis is equivalent to λmin(λ) ≥ 0 for all λ. In previous papers we proved, without...

Weil positivity on a window of width log 5: a formal proof in Lean 4

Weil's criterion expresses the Riemann Hypothesis as the positivity of a quadratic form W attached to the nontrivial zeros of the Riemann zeta function. For test functions supported in a fixed window, positivity is an unconditional and much weaker statement. We give a proof, form...