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