theorem AnalyticNumberTheory.LargeSieve.integral_lower_middle_upper (f : ℝ → ℂ) {T : ℝ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hT : 0 ≤ T) : ((∫ (t : ℝ) in Set.Iic (-T), f t) + ∫ (t : ℝ) in Set.Ioc (-T) T, f t) + ∫ (t : ℝ) in Set.Ici T, f t = ∫ (t : ℝ), f t

theorem AnalyticNumberTheory.LargeSieve.norm_verticalIntegral'_le_of_finite_contour_bounds (F : ℂ → ℂ) {a b T Vl Hu Hl Tl Tu : ℝ} (hT : 0 ≤ T) (hf : MeasureTheory.Integrable (fun (t : ℝ) => F (↑b + ↑t * Complex.I)) MeasureTheory.volume) (hshift : VIntegral F b (-T) T - VIntegral F a (-T) T = HIntegral F a b T - HIntegral F a b (-T)) (hleft : ‖VIntegral F a (-T) T‖ ≤ Vl) (htop : ‖HIntegral F a b T‖ ≤ Hu) (hbottom : ‖HIntegral F a b (-T)‖ ≤ Hl) (htlow : ‖∫ (t : ℝ) in Set.Iic (-T), F (↑b + ↑t * Complex.I)‖ ≤ Tl) (htupper : ‖∫ (t : ℝ) in Set.Ici T, F (↑b + ↑t * Complex.I)‖ ≤ Tu) : ‖VerticalIntegral' F b‖ ≤ Tl + (Vl + Hu + Hl) + Tu

Normalize a finite contour shift after bounding its three non-right edges and both tails of the integrable right line. No zero-free or arithmetic hypothesis is needed once the exact shift identity has been proved.

theorem AnalyticNumberTheory.LargeSieve.exists_dirichletLTwistedSmoothedNonquadraticErrorAssembly {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (νpos : ∀ x > 0, 0 ≤ ν x) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, ν x / x = 1) : ∃ K > 0, ∀ {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) {T d ε X : ℝ}, χ ^ 2 ≠ 1 → 3 ≤ T → 0 < d → d ≤ 1 → 0 < ε → ε < 1 → 1 ≤ X → ‖χ.twistedSmoothedPsi ν ε X‖ ≤ K * (T * dirichletLTwistedSmoothedConductorLogLM q T ^ 11 * X ^ dirichletLTwistedSmoothedConductorLogFinalLeft q T / ε + dirichletLTwistedSmoothedConductorLogLM q T ^ 11 * X ^ (1 + d) / (ε * (1 + T ^ 2)) + X ^ (1 + d) * (1 + d⁻¹ ^ 2) / (ε * T))

Premise-free assembly of the nonquadratic smoothed Perron error. The three terms are respectively the final left edge, the two horizontal edges, and the two tails of the full right vertical line.