Small actual quadratic L-values force near-one real zeros

The weighted positive convolution supplies the sign change. The zeta sign near its pole follows from the actual regularized zeta function. This modern argument does not assume a Siegel lower bound or the existence of an exceptional zero.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.one_le_quadraticConvolutionWeightedSum {q : ℕ} (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) (β : ℝ) {x : ℝ} (hx : 1 ≤ x) : 1 ≤ quadraticConvolutionWeightedSum χ β x

The coefficient at one gives a lower bound for every positive weighted prefix.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.quadraticConvolution_weighted_error_at_cutoff_le {q : ℕ} [NeZero q] {β : ℝ} (hβ : 3 / 4 ≤ β) : 81 * ↑q * (1 + β / (β - 1 / 2)) * ((648 * ↑q) ^ 4) ^ (1 / 2 - β) ≤ 1 / 2

The explicit cutoff pays the weighted error by one half uniformly for all exponents at least three quarters.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.IsPrimitive.re_zeta_mul_LFunction_pos_of_small_value {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hprim : χ.IsPrimitive) (hχ : χ ≠ 1) (hquad : χ ^ 2 = 1) {ε : ℝ} (hε : 0 < ε) (hε4 : ε ≤ 1 / 4) (hsmall : (DirichletCharacter.LFunction χ 1).re ≤ ε / (4 * (648 * ↑q) ^ (4 * ε))) : 0 < (riemannZeta ↑(1 - ε) * DirichletCharacter.LFunction χ ↑(1 - ε)).re

A small L-value makes the actual continued zeta-L product positive at the selected point to the left of one.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.exists_zeta_negative_left_neighborhood : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 1 / 4 ∧ ∀ (ε : ℝ), 0 < ε → ε ≤ ε₀ → (riemannZeta ↑(1 - ε)).re < 0

The genuine regularized zeta value gives a fixed left neighborhood where the Riemann zeta function has negative real part.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.exists_uniform_small_value_real_zero_neighborhood : ∃ (ε₀ : ℝ), 0 < ε₀ ∧ ε₀ ≤ 1 / 4 ∧ ∀ (ε : ℝ), 0 < ε → ε ≤ ε₀ → ∀ (q : ℕ) [inst : NeZero q] (χ : DirichletCharacter ℂ q), χ.IsPrimitive → χ ≠ 1 → χ ^ 2 = 1 → (DirichletCharacter.LFunction χ 1).re ≤ ε / (4 * (648 * ↑q) ^ (4 * ε)) → ∃ β ∈ Set.Ioo (1 - ε) 1, DirichletCharacter.LFunction χ ↑β = 0

One outer zeta neighborhood works for all conductors and characters. The small-value threshold is explicit and the produced zero belongs to the actual L-function, strictly between 1-ε and one.