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).