A conductor-uniform lower bound for actual quadratic L-values

This modern fixed-witness argument proves the Siegel lower bound without an assumed zero-repulsion, exceptional-zero, or L-value lower-bound premise. Either a fixed left neighborhood has no primitive quadratic real zero, or one actual witness in that neighborhood is chosen before every target.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.exists_uniform_quadratic_LFunction_one_lower_bound (η : ℝ) (hη : 0 < η) : ∃ (c : ℝ), 0 < c ∧ ∀ (q : ℕ) [inst : NeZero q] (χ : DirichletCharacter ℂ q), χ.IsPrimitive → χ ≠ 1 → χ ^ 2 = 1 → c * ↑q ^ (-η) ≤ (DirichletCharacter.LFunction χ 1).re

For each positive exponent, one positive constant bounds the actual L-value of every primitive nonprincipal quadratic character, at every nonzero conductor. The constant is not asserted to be effective.