theorem AnalyticNumberTheory.LargeSieve.norm_deriv_LFunction_le_modulus_mul_linear_height {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) {σ t : ℝ} (hσlower : 1 / 2 ≤ σ) (_hσupper : σ ≤ 2) : ‖deriv (DirichletCharacter.LFunction χ) (↑σ + Complex.I * ↑t)‖ ≤ ↑q * (2 + 4 * ‖↑σ + Complex.I * ↑t‖)

A deliberately crude, but global, vertical growth estimate. The naturally ordered Abel representation at cutoff one is enough: on 1/2 ≤ σ ≤ 2, L' has at most linear growth in the height.

theorem AnalyticNumberTheory.LargeSieve.norm_chen1973Lemma6Eq17ShiftIntegrand_le_inv_one_add_sq {d x H : ℕ} [NeZero d] (χ : PrimitiveCharacter d) (hχ : ↑χ ≠ 1) (hx : 3 ≤ x) {y σ t : ℝ} (hy : 0 < y) (hσlower : chen1973Lemma6Beta x ≤ σ) (hσupper : σ ≤ chen1973Lemma6Alpha x) : ‖chen1973Lemma6Eq17ShiftIntegrand x H y χ (↑σ + Complex.I * ↑t)‖ ≤ (↑d * ∑ n ∈ Finset.Icc 1 H, ‖↑(ArithmeticFunction.moebius n) * ↑χ ↑n‖) * Real.exp (2 * |Real.log y|) * (chen1973PerronScale ↑x ^ (chen1973PerronOrder ↑x + 1) * (2 / chen1973Lemma6Beta x + 4)) / (1 + t ^ 2)

A uniform 1/(1+t²) majorant on the whole closed strip. The linear Abel growth of L' is cancelled by the explicit s in Chen's kernel; the remaining kernel power has order at least two once x ≥ 3.

theorem AnalyticNumberTheory.LargeSieve.integrable_chen1973Lemma6Eq17_verticalSection {d x H : ℕ} [NeZero d] (χ : PrimitiveCharacter d) (hχ : ↑χ ≠ 1) (hx : 3 ≤ x) {y σ : ℝ} (hy : 0 < y) (hσlower : chen1973Lemma6Beta x ≤ σ) (hσupper : σ ≤ chen1973Lemma6Alpha x) : MeasureTheory.Integrable (chen1973VerticalSection (chen1973Lemma6Eq17ShiftIntegrand x H y χ) σ) MeasureTheory.volume

Both boundary sections are Bochner integrable; in fact the same proof works for every vertical line in the closed strip.

theorem AnalyticNumberTheory.LargeSieve.norm_chen1973Lemma6Eq17_horizontalSection_le_inv_one_add_sq {d x H : ℕ} [NeZero d] (χ : PrimitiveCharacter d) (hχ : ↑χ ≠ 1) (hx : 3 ≤ x) {y T : ℝ} (hy : 0 < y) : ‖chen1973HorizontalSection (chen1973Lemma6Eq17ShiftIntegrand x H y χ) (chen1973Lemma6Beta x) (chen1973Lemma6Alpha x) T‖ ≤ (↑d * ∑ n ∈ Finset.Icc 1 H, ‖↑(ArithmeticFunction.moebius n) * ↑χ ↑n‖) * Real.exp (2 * |Real.log y|) * (chen1973PerronScale ↑x ^ (chen1973PerronOrder ↑x + 1) * (2 / chen1973Lemma6Beta x + 4)) / (1 + T ^ 2)

Explicit horizontal-edge decay. Each edge has length α-β=1/2; the triangle inequality for their difference therefore costs exactly one copy of the common pointwise majorant.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq17_LDerivS_contour_shift_unconditional {d x H : ℕ} [NeZero d] (χ : PrimitiveCharacter d) (hχ : ↑χ ≠ 1) (hx : 3 ≤ x) {y : ℝ} (hy : 0 < y) : ∫ (t : ℝ), chen1973VerticalSection (chen1973Lemma6Eq17ShiftIntegrand x H y χ) (chen1973Lemma6Alpha x) t = ∫ (t : ℝ), chen1973VerticalSection (chen1973Lemma6Eq17ShiftIntegrand x H y χ) (chen1973Lemma6Beta x) t

Unconditional equation-(17) contour shift for the actual nonprincipal primitive L'·S kernel. No integrability or horizontal-decay premise remains at the call site.