theorem AnalyticNumberTheory.LargeSieve.norm_twistedSmoothedPerron_horizontal_le_of_logDeriv_bound {ν : ℝ → ℝ} {M ε : ℝ} (hM : 0 ≤ M) (hε : 0 < ε) (hMellin : ∀ (s : ℂ), 1 / 2 ≤ s.re → s.re ≤ 2 → ‖mellin (fun (x : ℝ) => ↑(Smooth1 ν ε x)) s‖ ≤ M * (ε * ‖s‖ ^ 2)⁻¹) {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) {a b T t X J : ℝ} (ha : 1 / 2 ≤ a) (hab : a ≤ b) (hb : b ≤ 2) (hT : 1 ≤ T) (ht : |t| = T) (hX : 1 ≤ X) (hJ : 0 ≤ J) (hlog : ∀ (σ : ℝ), a ≤ σ → σ ≤ b → ‖deriv (DirichletCharacter.LFunction χ) (↑σ + ↑t * Complex.I) / DirichletCharacter.LFunction χ (↑σ + ↑t * Complex.I)‖ ≤ J) : ‖HIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) a b t‖ ≤ 4 * M * J * X ^ b / (ε * (1 + T ^ 2))

A horizontal Mellin--Bochner estimate, independent of the character's zero-free region. The caller supplies the Mellin decay and the log-derivative bound; the proof pays for the height, complex power, and interval length.

theorem AnalyticNumberTheory.LargeSieve.exists_dirichletLTwistedSmoothedContourNormBounds {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) : ∃ C > 0, ∀ {q : ℕ} [inst : NeZero q] (χ : DirichletCharacter ℂ q) {T d ε X : ℝ}, χ ^ 2 ≠ 1 → 3 ≤ T → 0 < d → d ≤ 1 → 0 < ε → ε < 1 → 1 ≤ X → ‖VIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) (dirichletLTwistedSmoothedConductorLogFinalLeft q T) (-T) T‖ ≤ C * T * dirichletLTwistedSmoothedConductorLogLM q T ^ 11 * X ^ dirichletLTwistedSmoothedConductorLogFinalLeft q T / ε ∧ ‖HIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) (dirichletLTwistedSmoothedConductorLogFinalLeft q T) (dirichletLTwistedSmoothedConductorLogRight d) T‖ ≤ C * dirichletLTwistedSmoothedConductorLogLM q T ^ 11 * X ^ (1 + d) / (ε * (1 + T ^ 2)) ∧ ‖HIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) (dirichletLTwistedSmoothedConductorLogFinalLeft q T) (dirichletLTwistedSmoothedConductorLogRight d) (-T)‖ ≤ C * dirichletLTwistedSmoothedConductorLogLM q T ^ 11 * X ^ (1 + d) / (ε * (1 + T ^ 2))

Genuine Bochner interval estimates for all three non-right edges of the final conductor-logarithmic rectangle. The constant is selected before every arithmetic and contour parameter, so it depends only on the fixed smoothing function ν (through MellinOfSmooth1b).