noncomputable def AnalyticNumberTheory.LargeSieve.chenLaplaceMoment (q : ℂ) (n : ℕ) (u : ℝ) : ℂ

The complex Laplace moment used in the Mellin transform of Chen's kernel.

Equations

• AnalyticNumberTheory.LargeSieve.chenLaplaceMoment q n u = Complex.exp (-q * ↑u) * ↑u ^ n

theorem AnalyticNumberTheory.LargeSieve.integrableOn_chenLaplaceMoment {q : ℂ} (hq : 0 < q.re) (n : ℕ) : MeasureTheory.IntegrableOn (chenLaplaceMoment q n) (Set.Ioi 0) MeasureTheory.volume

Integrability of the complex Laplace moment in the right half-plane.

theorem AnalyticNumberTheory.LargeSieve.integral_chenLaplaceMoment {q : ℂ} (hq : 0 < q.re) (n : ℕ) : ∫ (u : ℝ) in Set.Ioi 0, chenLaplaceMoment q n u = ↑n.factorial / q ^ (n + 1)

The elementary complex Laplace moment formula ∫₀∞ exp (-q u) uⁿ du = n! / qⁿ⁺¹, valid for re q > 0.