theorem
AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_termVertical_integrable_of_logDerivative_bound
{x d : ℕ}
(hx : 3 ≤ x)
(hd : 1 < d)
(χ : PrimitiveCharacter d)
{pp : ℕ × ℕ}
(hy : 0 < ↑x / (↑pp.1 * ↑pp.2))
{σ M : ℝ}
(hσ : 0 < σ)
(r : ℕ)
(hderiv :
∀ (t : ℝ),
‖chen1973PrimitiveLDeriv d (↑σ + ↑t * Complex.I) χ / chen1973Lemma6PrimitiveLValue d (↑σ + ↑t * Complex.I) χ‖ ≤ M * (1 + Real.log (↑d * (1 + |t|))) ^ r)
:
Integrability on an arbitrary positive line from an actual pointwise bound.
theorem
AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation21_levelZero_eventually_of_logDerivative_and_horizontal
{M c : ℝ}
(hM : 0 ≤ M)
(hc : 0 < c)
(r : ℕ)
:
∃ (x₀ : ℕ),
∀ x ≥ x₀,
∀ (L B k m l₂ : ℕ),
Chen1973Lemma6Eq21SourceParameters x L B k m l₂ →
Chen1973Lemma6Eq21ZeroFreeInput x L c →
(∀ d ∈ chen1973Lemma6ConductorBlock x L 0,
∀ (χ : PrimitiveCharacter d) (t : ℝ),
‖chen1973PrimitiveLDeriv d (chen1973Lemma6Eq21Line x t) χ / chen1973Lemma6PrimitiveLValue d (chen1973Lemma6Eq21Line x t) χ‖ ≤ M * (1 + Real.log (↑d * (1 + |t|))) ^ r) →
(∀ d ∈ chen1973Lemma6ConductorBlock x L 0,
∀ (χ : PrimitiveCharacter d),
∀ pp ∈ chen1973Lemma6PrimePairShell x B k m,
∃ (C : ℝ),
0 ≤ C ∧ ∀ (T : ℝ),
0 ≤ T →
‖chen1973HorizontalSection (chen1973Lemma6Eq21TermShiftIntegrand x d χ pp)
(chen1973Lemma6Eq21Sigma x) (chen1973Lemma6Alpha x) T‖ ≤ C / (1 + T ^ 2)) →
chen1973Lemma6NmBlockActual x L 0 B k m ≤ ↑x / Real.log ↑x ^ 20
Source-level terminal with the vertical estimate and both vertical integrability premises removed. The full-height zero-free strip, the actual left-line logarithmic-derivative bound, and horizontal decay remain explicit.