Exact logarithmic moments for the true equation-(21) Mellin tail

This file proves the positive-ray moments and their finite binomial sum. It does not assume or prove a logarithmic-derivative bound. Integrability is established by Gamma convergence and change of variables, not totalization.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_expMoment_integrable (N j : ℕ) (hN : 0 < N) : MeasureTheory.IntegrableOn (fun (w : ℝ) => w ^ j * Real.exp (-(↑N * w))) (Set.Ioi 0) MeasureTheory.volume

Gamma moment used to prove the true Mellin tail integrable before evaluating it.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_expMoment_integral (N j : ℕ) (hN : 0 < N) : ∫ (w : ℝ) in Set.Ioi 0, w ^ j * Real.exp (-(↑N * w)) = ↑j.factorial / ↑N ^ (j + 1)

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_logTail_integrable (N j : ℕ) (hN : 0 < N) : MeasureTheory.IntegrableOn (fun (v : ℝ) => Real.log v ^ j / v ^ (N + 1)) (Set.Ioi 1) MeasureTheory.volume

Logarithmic tail moment on the unit ray.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_logTail_integral (N j : ℕ) (hN : 0 < N) : ∫ (v : ℝ) in Set.Ioi 1, Real.log v ^ j / v ^ (N + 1) = ↑j.factorial / ↑N ^ (j + 1)

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_scaledLogTail_integrable {a : ℝ} (ha : 0 < a) (N j : ℕ) (hN : 0 < N) : MeasureTheory.IntegrableOn (fun (t : ℝ) => a ^ N / t ^ (N + 1) * Real.log (t / a) ^ j) (Set.Ioi a) MeasureTheory.volume

Scale cancellation in the true high-tail moment, including integrability.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_scaledLogTail_integral {a : ℝ} (ha : 0 < a) (N j : ℕ) (hN : 0 < N) : ∫ (t : ℝ) in Set.Ioi a, a ^ N / t ^ (N + 1) * Real.log (t / a) ^ j = ↑j.factorial / ↑N ^ (j + 1)

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_shiftedLogTail_integrable {a : ℝ} (ha : 0 < a) (D : ℝ) (N r : ℕ) (hN : 0 < N) : MeasureTheory.IntegrableOn (fun (t : ℝ) => a ^ N / t ^ (N + 1) * (D + Real.log (t / a)) ^ r) (Set.Ioi a) MeasureTheory.volume

Arbitrary polynomial logarithmic growth remains integrable in the true tail.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_shiftedLogTail_integral {a : ℝ} (ha : 0 < a) (D : ℝ) (N r : ℕ) (hN : 0 < N) : ∫ (t : ℝ) in Set.Ioi a, a ^ N / t ^ (N + 1) * (D + Real.log (t / a)) ^ r = ∑ j ∈ Finset.range (r + 1), ↑(r.choose j) * D ^ (r - j) * (↑j.factorial / ↑N ^ (j + 1))

Exact full high-tail budget, with the scale cancelling and no radial loss.