Quantitative quadratic logarithmic derivatives on the annulus and whole strip

The (3,4,1) value product gives more than nonvanishing on a fixed height annulus. After paying the principal Euler correction and the zeta pole-plus-log factor, it forces an explicit lower bound for the quadratic L-value. Combining that bound with the production derivative estimate gives a quantitative L'/L bound. The final theorem joins this annular estimate to the central-band bound; no compactness argument is used.

theorem AnalyticNumberTheory.LargeSieve.norm_LFunction_ge_on_quadraticConditionalAnnulus (Z : ℝ) (hZ : 0 < Z) (hzeta : ∀ (x u : ℝ), 0 < x → x ≤ 1 → u ≠ 0 → ‖riemannZeta (1 + ↑x + Complex.I * ↑u)‖ ≤ Z * (1 + Real.log (|u| + 2) + 1 / |u|)) {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) (hχ : χ ≠ 1) {A η τ T β t : ℝ} (hA : 0 < A) (hAhalf : A ≤ 1 / 2) (hAsmall : A ≤ 1 / (16 * Z * 192 ^ 4)) (hη : 0 < η) (hτ : 0 < τ) (hτT : τ ≤ T) (hβ : dirichletLQuadraticConditionalFixedLeft A η q τ T ≤ β) (hβone : β ≤ 1) (htlow : τ ≤ |t|) (htT : |t| ≤ T) : have H := dirichletLQuadraticConditionalFixedH q τ T; have x := A * ↑q ^ (-2 * η) / H ^ 12; 64 * H ^ 2 * x ≤ ‖DirichletCharacter.LFunction χ (↑β + Complex.I * ↑t)‖

On a fixed nonzero-height annulus the value product supplies an explicit lower bound of size H² x, where x is the fixed power-width. All factors in the value product are bounded by the actual principal Euler-correction and pole-plus-log estimates.

theorem AnalyticNumberTheory.LargeSieve.norm_logDerivative_le_on_quadraticConditionalAnnulus (Z : ℝ) (hZ : 0 < Z) (hzeta : ∀ (x u : ℝ), 0 < x → x ≤ 1 → u ≠ 0 → ‖riemannZeta (1 + ↑x + Complex.I * ↑u)‖ ≤ Z * (1 + Real.log (|u| + 2) + 1 / |u|)) {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) (hχ : χ ≠ 1) {A η τ T β t : ℝ} (hA : 0 < A) (hAhalf : A ≤ 1 / 2) (hAsmall : A ≤ 1 / (16 * Z * 192 ^ 4)) (hη : 0 < η) (hτ : 0 < τ) (hτT : τ ≤ T) (hβ : dirichletLQuadraticConditionalFixedLeft A η q τ T ≤ β) (hβone : β ≤ 1) (htlow : τ ≤ |t|) (htT : |t| ≤ T) : ‖deriv (DirichletCharacter.LFunction χ) (↑β + Complex.I * ↑t) / DirichletCharacter.LFunction χ (↑β + Complex.I * ↑t)‖ ≤ dirichletLQuadraticConditionalFixedH q τ T ^ 12 / (A * ↑q ^ (-2 * η))

Quantitative L'/L bound throughout a fixed annulus. The inverse value cost is displayed as H^12 / (A q^(-2η)).

theorem AnalyticNumberTheory.LargeSieve.norm_logDerivative_le_on_quadraticConditionalWholeBand (Z : ℝ) (hZ : 0 < Z) (hzeta : ∀ (x u : ℝ), 0 < x → x ≤ 1 → u ≠ 0 → ‖riemannZeta (1 + ↑x + Complex.I * ↑u)‖ ≤ Z * (1 + Real.log (|u| + 2) + 1 / |u|)) {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) (hχ : χ ≠ 1) {A c η T β t : ℝ} (hA : 0 < A) (hAc : A ≤ c / 256) (hAhalf : A ≤ 1 / 2) (hAsmall : A ≤ 1 / (16 * Z * 192 ^ 4)) (hc : 0 < c) (hη : 0 < η) (hT : 0 < T) (hSiegel : c * ↑q ^ (-η) ≤ (DirichletCharacter.LFunction χ 1).re) (hβ : 1 - dirichletLQuadraticConditionalCrossZeroWidth A c η q T ≤ β) (hβone : β ≤ 1) (htT : |t| ≤ T) : ‖deriv (DirichletCharacter.LFunction χ) (↑β + Complex.I * ↑t) / DirichletCharacter.LFunction χ (↑β + Complex.I * ↑t)‖ ≤ 128 * dirichletLQuadraticConditionalCentralH q T ^ 2 / (c * ↑q ^ (-η)) + dirichletLQuadraticConditionalFixedH q (dirichletLQuadraticConditionalCentralHeight c η q T) T ^ 12 / (A * ↑q ^ (-2 * η))

One quantitative bound on the complete cross-zero rectangle to the left of 1: the first summand pays the central band and the second the two annuli.

theorem AnalyticNumberTheory.LargeSieve.exists_quadraticConditionalWholeBand_logDerivativeBound (c η : ℝ) (hc : 0 < c) (hη : 0 < η) : ∃ (A : ℝ), 0 < A ∧ ∀ (q : ℕ) [inst : NeZero q] (χ : DirichletCharacter ℂ q) (T β t : ℝ), χ ^ 2 = 1 → χ ≠ 1 → 0 < T → c * ↑q ^ (-η) ≤ (DirichletCharacter.LFunction χ 1).re → 1 - dirichletLQuadraticConditionalCrossZeroWidth A c η q T ≤ β → β ≤ 1 → |t| ≤ T → ‖deriv (DirichletCharacter.LFunction χ) (↑β + Complex.I * ↑t) / DirichletCharacter.LFunction χ (↑β + Complex.I * ↑t)‖ ≤ 128 * dirichletLQuadraticConditionalCentralH q T ^ 2 / (c * ↑q ^ (-η)) + dirichletLQuadraticConditionalFixedH q (dirichletLQuadraticConditionalCentralHeight c η q T) T ^ 12 / (A * ↑q ^ (-2 * η))

Closed quantitative headline: the zeta constant and a positive common width are selected before the modulus, character, height and point.