theorem AnalyticNumberTheory.LargeSieve.norm_logDerivative_le_on_quadraticConditionalPerronHorizontal (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 : 3 ≤ T) (hSiegel : c * ↑q ^ (-η) ≤ (DirichletCharacter.LFunction χ 1).re) (ht : |t| = T) (hσleft : dirichletLTwistedSmoothedQuadraticConditionalLeft A c η q T ≤ σ) (hσright : σ ≤ dirichletLTwistedSmoothedQuadraticConditionalRight A c η q T) : ‖deriv (DirichletCharacter.LFunction χ) (↑σ + Complex.I * ↑t) / DirichletCharacter.LFunction χ (↑σ + Complex.I * ↑t)‖ ≤ 2 * (128 * dirichletLQuadraticConditionalCentralH q T ^ 2 / (c * ↑q ^ (-η)) + dirichletLQuadraticConditionalFixedH q (dirichletLQuadraticConditionalCentralHeight c η q T) T ^ 12 / (A * ↑q ^ (-2 * η)))

On either horizontal edge of the quadratic Perron rectangle, the logarithmic derivative is bounded by twice the left-band budget. The part to the right of 1 is paid by transporting the annular lower bound at 1 over the quarter-width extension.

theorem AnalyticNumberTheory.LargeSieve.exists_dirichletLTwistedSmoothedQuadraticConditionalContourNormBounds {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) : ∃ C > 0, ∀ (Z : ℝ), 0 < Z → (∀ (x u : ℝ), 0 < x → x ≤ 1 → u ≠ 0 → ‖riemannZeta (1 + ↑x + Complex.I * ↑u)‖ ≤ Z * (1 + Real.log (|u| + 2) + 1 / |u|)) → ∀ {q : ℕ} [inst : NeZero q] (χ : DirichletCharacter ℂ q) {A c η T ε X : ℝ}, χ ^ 2 = 1 → χ ≠ 1 → 0 < A → A ≤ c / 256 → A ≤ 1 / 2 → A ≤ 1 / (16 * Z * 192 ^ 4) → 0 < c → 0 < η → 3 ≤ T → c * ↑q ^ (-η) ≤ (DirichletCharacter.LFunction χ 1).re → 0 < ε → ε < 1 → 1 ≤ X → have Q := 128 * dirichletLQuadraticConditionalCentralH q T ^ 2 / (c * ↑q ^ (-η)) + dirichletLQuadraticConditionalFixedH q (dirichletLQuadraticConditionalCentralHeight c η q T) T ^ 12 / (A * ↑q ^ (-2 * η)); have a := dirichletLTwistedSmoothedQuadraticConditionalLeft A c η q T; have b := dirichletLTwistedSmoothedQuadraticConditionalRight A c η q T; ‖VIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) a (-T) T‖ ≤ C * T * Q * X ^ a / ε ∧ ‖HIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) a b T‖ ≤ C * Q * X ^ b / (ε * (1 + T ^ 2)) ∧ ‖HIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) a b (-T)‖ ≤ C * Q * X ^ b / (ε * (1 + T ^ 2))

Genuine Bochner norms for the left and both horizontal edges of the quadratic conditional rectangle.