theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_complexKernel_tail_bound {a t σ : ℝ} (ha : 0 < a) (ht : 0 < t) (N : ℕ) : ‖1 / ((↑σ + ↑t * Complex.I) * (1 + (↑σ + ↑t * Complex.I) / ↑a) ^ N)‖ ≤ a ^ N / t ^ (N + 1)

Imaginary-part bounds retain the full true high-tail exponent.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_mellinKernel_tail_bound {x : ℕ} (hx : 1 < x) {t σ : ℝ} (ht : 0 < t) : ‖chen1973MellinKernel (↑x) (↑σ + ↑t * Complex.I)‖ ≤ chen1973PerronScale ↑x ^ (chen1973PerronOrder ↑x + 1) / t ^ (chen1973PerronOrder ↑x + 2)

The genuine production kernel inherits the lossless high-tail estimate.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_weightedKernel_tail_bound {x : ℕ} (hx : 1 < x) {d t σ : ℝ} (hd : 1 ≤ d) (ht : chen1973PerronScale ↑x ≤ t) (r : ℕ) : ‖chen1973MellinKernel (↑x) (↑σ + ↑t * Complex.I)‖ * (1 + Real.log (d * (1 + t))) ^ r ≤ chen1973PerronScale ↑x ^ (chen1973PerronOrder ↑x + 1) / t ^ (chen1973PerronOrder ↑x + 2) * (1 + Real.log (d * (1 + chen1973PerronScale ↑x)) + Real.log (t / chen1973PerronScale ↑x)) ^ r

Polynomial logarithmic weight on the actual production kernel's high tail.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_weightedKernel_tail_integrable_and_bound {x : ℕ} (hx : 1 < x) {d σ : ℝ} (hd : 1 ≤ d) (r : ℕ) : have a := chen1973PerronScale ↑x; have N := chen1973PerronOrder ↑x + 1; have D := 1 + Real.log (d * (1 + a)); have f := fun (t : ℝ) => ‖chen1973MellinKernel (↑x) (↑σ + ↑t * Complex.I)‖ * (1 + Real.log (d * (1 + t))) ^ r; MeasureTheory.IntegrableOn f (Set.Ioi a) MeasureTheory.volume ∧ ∫ (t : ℝ) in Set.Ioi a, f t ≤ ∑ j ∈ Finset.range (r + 1), ↑(r.choose j) * D ^ (r - j) * (↑j.factorial / ↑N ^ (j + 1))

The actual weighted Mellin kernel is integrable on its high tail, with an explicit budget from the exact logarithmic moments. No integrability input or zero-free/logarithmic-derivative premise is used in this kernel theorem.