theorem AnalyticNumberTheory.LargeSieve.test_int_gamma {q : ℂ} (hq : 0 < q.re) (n : ℕ) : MeasureTheory.IntegrableOn (fun (u : ℝ) => Complex.exp (-q * ↑u) * ↑(chenGammaCDF n u)) (Set.Ioi 0) MeasureTheory.volume

theorem AnalyticNumberTheory.LargeSieve.test_int_gamma_value {q : ℂ} (hq : 0 < q.re) (n : ℕ) : ∫ (u : ℝ) in Set.Ioi 0, Complex.exp (-q * ↑u) * ↑(chenGammaCDF n u) = 1 / (q * (1 + q) ^ (n + 1))

theorem AnalyticNumberTheory.LargeSieve.test_scaled_integrable {q : ℂ} (hq : 0 < q.re) {A : ℝ} (hA : 0 < A) (n : ℕ) : MeasureTheory.IntegrableOn (fun (u : ℝ) => Complex.exp (-q * ↑u) * ↑(chenGammaCDF n (A * u))) (Set.Ioi 0) MeasureTheory.volume

theorem AnalyticNumberTheory.LargeSieve.test_scaled_value {q : ℂ} (hq : 0 < q.re) {A : ℝ} (hA : 0 < A) (n : ℕ) : ∫ (u : ℝ) in Set.Ioi 0, Complex.exp (-q * ↑u) * ↑(chenGammaCDF n (A * u)) = 1 / (q * (1 + q / ↑A) ^ (n + 1))

theorem AnalyticNumberTheory.LargeSieve.chen_cpow_exp_neg (s : ℂ) (u : ℝ) : ↑(Real.exp (-u)) ^ (s - 1) * ↑(Real.exp (-u)) = Complex.exp (-s * ↑u)

theorem AnalyticNumberTheory.LargeSieve.mellin_eq_integral_exp_neg (f : ℝ → ℂ) (s : ℂ) : mellin f s = ∫ (u : ℝ), Complex.exp (-s * ↑u) * f (Real.exp (-u))

theorem AnalyticNumberTheory.LargeSieve.chen1973GammaDensityPrimitive_exp_neg {x : ℝ} (_hx : 1 < x) (u : ℝ) : chen1973GammaDensityPrimitive x (Real.exp (-u)) = if u ≤ 0 then 0 else ↑(chenGammaCDF (chen1973PerronOrder x) (chen1973PerronScale x * u))

theorem AnalyticNumberTheory.LargeSieve.mellin_chen1973GammaDensityPrimitive {x : ℝ} (hx : 1 < x) {s : ℂ} (hs : 0 < s.re) : mellin (chen1973GammaDensityPrimitive x) s = chen1973MellinKernel x s

theorem AnalyticNumberTheory.LargeSieve.mellinConvergent_chen1973GammaDensityPrimitive {x : ℝ} (hx : 1 < x) {s : ℂ} (hs : 0 < s.re) : MellinConvergent (chen1973GammaDensityPrimitive x) s

theorem AnalyticNumberTheory.LargeSieve.continuousOn_chen1973GammaDensityPrimitive (x : ℝ) : ContinuousOn (chen1973GammaDensityPrimitive x) (Set.Ioi 0)

The Gamma primitive is continuous throughout the positive half-line, including the glued endpoint r = 1.

theorem AnalyticNumberTheory.LargeSieve.continuousAt_chen1973GammaDensityPrimitive (x r : ℝ) (hr : 0 < r) : ContinuousAt (chen1973GammaDensityPrimitive x) r

Pointwise positive-argument continuity required by Mellin inversion.

theorem AnalyticNumberTheory.LargeSieve.Chen1973BromwichIdentity (x : ℝ) (hx : 1 < x) (y : ℝ) : 0 < y → ↑(1 / (2 * Real.pi)) * ∫ (t : ℝ), chen1973BromwichIntegrand x y t = ↑(chen1973PerronKernelFinite x y)

Chen's unconditional Bromwich identity. The Mellin transform formula, convergence on re s = 2, and positive-argument continuity are all proved in this module rather than supplied by callers.