A conductor-logarithmic global nonquadratic zero-free region #
The de la Vallée Poussin product lower bound is combined directly with the natural-order conductor-height value and derivative estimates. In particular, the resulting width contains no positive power of the modulus.
Doubling the height at most doubles the integral height block.
theorem
AnalyticNumberTheory.LargeSieve.dirichletLConductorHeightCutoff_two_mul_le_sq
{q : ℕ}
[NeZero q]
(χ : DirichletCharacter ℂ q)
(hχ : χ ≠ 1)
(t : ℝ)
:
The cutoff at doubled height is bounded by the square of the original cutoff once the character is nonprincipal.
theorem
AnalyticNumberTheory.LargeSieve.norm_LFunction_ne_zero_of_nonquadratic_conductorLog
{q : ℕ}
[NeZero q]
(χ : DirichletCharacter ℂ q)
(hχsq : χ ^ 2 ≠ 1)
{β t : ℝ}
(hβ :
β ∈ Set.Ico
(1 - 1 / (274877906944 * (1 + Real.log ↑(DirichletLGlobalConductorLogValueBound.dirichletLConductorHeightCutoff q t)) ^ 9))
1)
:
A nonquadratic character has no zero in a purely conductor-logarithmic left neighbourhood of one.