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.

theorem AnalyticNumberTheory.LargeSieve.dirichletLHeightBlock_two_mul_le (t : ℝ) : DirichletLGlobalConductorLogValueBound.dirichletLHeightBlock (2 * t) ≤ 2 * DirichletLGlobalConductorLogValueBound.dirichletLHeightBlock t

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 : ℝ) : DirichletLGlobalConductorLogValueBound.dirichletLConductorHeightCutoff q (2 * t) ≤ DirichletLGlobalConductorLogValueBound.dirichletLConductorHeightCutoff q t ^ 2

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) : DirichletCharacter.LFunction χ (↑β + Complex.I * ↑t) ≠ 0

A nonquadratic character has no zero in a purely conductor-logarithmic left neighbourhood of one.