theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_verticalIntegral_bound_of_logDerivative_bound {x d : ℕ} (hx : 3 ≤ x) (hd : 1 < d) (χ : PrimitiveCharacter d) {pp : ℕ × ℕ} (hy : 1 < ↑x / (↑pp.1 * ↑pp.2)) {M : ℝ} (hM : 0 ≤ M) (r : ℕ) (hderiv : ∀ (t : ℝ), ‖chen1973PrimitiveLDeriv d (chen1973Lemma6Eq21Line x t) χ / chen1973Lemma6PrimitiveLValue d (chen1973Lemma6Eq21Line x t) χ‖ ≤ M * (1 + Real.log (↑d * (1 + |t|))) ^ r) : have a := chen1973PerronScale ↑x; have N := chen1973PerronOrder ↑x + 1; have D := 1 + Real.log (↑d * (1 + a)); have σ := chen1973Lemma6Eq21Sigma x; have y := ↑x / (↑pp.1 * ↑pp.2); have budget := (σ⁻¹ + Real.log a) * D ^ r + ∑ j ∈ Finset.range (r + 1), ↑(r.choose j) * D ^ (r - j) * (↑j.factorial / ↑N ^ (j + 1)); MeasureTheory.Integrable (fun (t : ℝ) => chen1973VerticalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp) σ t) MeasureTheory.volume ∧ ‖(↑(Real.log y))⁻¹ * chen1973Lemma6Eq21VerticalIntegral x d χ pp‖ ≤ M / (Real.pi * Real.log y) * budget * y ^ σ

An actual primitive vertical integral bound from a pointwise logarithmic- derivative estimate. Integrability is proved, not supplied or totalized away.