Mellin continuation of the quadratic convolution

This is a modern analytic argument using the proved square-root error in the summatory convolution, rather than a transcription of Bombieri's proof.

noncomputable def AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.quadraticConvolutionError {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (t : ℝ) : ℝ

The actual summatory error, with the actual value of the Dirichlet L-function.

Equations

• AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.quadraticConvolutionError χ t = χ.quadraticSiegelConvolutionSummatory ⌊t⌋₊ - t * (DirichletCharacter.LFunction χ 1).re

noncomputable def AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.quadraticConvolutionErrorKernel {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (s : ℂ) (t : ℝ) : ℂ

The integrand in the continued convolution formula.

Equations

• AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.quadraticConvolutionErrorKernel χ s t = ↑(AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.quadraticConvolutionError χ t) * ↑t ^ (-(s + 1))

noncomputable def AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.quadraticConvolutionErrorIntegral {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (s : ℂ) : ℂ

The Mellin error integral, with lower endpoint one.

Equations

• AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.quadraticConvolutionErrorIntegral χ s = ∫ (t : ℝ) in Set.Ioi 1, AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.quadraticConvolutionErrorKernel χ s t

noncomputable def AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.quadraticConvolutionCutoffError {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) : ℝ → ℂ

Cutoff used only to apply the ordinary Mellin transform API.

Equations

• AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.quadraticConvolutionCutoffError χ = (Set.Ioi 1).indicator fun (t : ℝ) => ↑(AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.quadraticConvolutionError χ t)

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.measurable_quadraticConvolutionError {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) : Measurable (quadraticConvolutionError χ)

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.measurable_quadraticConvolutionCutoffError {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) : Measurable (quadraticConvolutionCutoffError χ)

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.IsPrimitive.abs_quadraticConvolutionError_le {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hprim : χ.IsPrimitive) (hχ : χ ≠ 1) {t : ℝ} (ht : 1 ≤ t) : |quadraticConvolutionError χ t| ≤ 81 * ↑q * √t

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.IsPrimitive.norm_quadraticConvolutionCutoffError_le {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hprim : χ.IsPrimitive) (hχ : χ ≠ 1) (t : ℝ) : ‖quadraticConvolutionCutoffError χ t‖ ≤ 81 * ↑q * √t

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.IsPrimitive.locallyIntegrable_quadraticConvolutionCutoffError {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hprim : χ.IsPrimitive) (hχ : χ ≠ 1) : MeasureTheory.LocallyIntegrable (quadraticConvolutionCutoffError χ) MeasureTheory.volume

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.IsPrimitive.quadraticConvolutionCutoffError_isBigO_atTop {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hprim : χ.IsPrimitive) (hχ : χ ≠ 1) : quadraticConvolutionCutoffError χ =O[Filter.atTop] fun (t : ℝ) => t ^ (1 / 2)

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.quadraticConvolutionCutoffError_isBigO_zero {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (b : ℝ) : quadraticConvolutionCutoffError χ =O[nhdsWithin 0 (Set.Ioi 0)] fun (t : ℝ) => t ^ b

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.mellin_quadraticConvolutionCutoffError {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (s : ℂ) : mellin (quadraticConvolutionCutoffError χ) (-s) = quadraticConvolutionErrorIntegral χ s

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.IsPrimitive.mellinConvergent_quadraticConvolutionCutoffError {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hprim : χ.IsPrimitive) (hχ : χ ≠ 1) {s : ℂ} (hs : 1 / 2 < s.re) : MellinConvergent (quadraticConvolutionCutoffError χ) (-s)

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.IsPrimitive.integrableOn_quadraticConvolutionErrorKernel {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hprim : χ.IsPrimitive) (hχ : χ ≠ 1) {s : ℂ} (hs : 1 / 2 < s.re) : MeasureTheory.IntegrableOn (quadraticConvolutionErrorKernel χ s) (Set.Ioi 1) MeasureTheory.volume

Absolute convergence of the genuine summatory-error integral in Re s > 1/2.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.IsPrimitive.differentiableAt_quadraticConvolutionErrorIntegral {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hprim : χ.IsPrimitive) (hχ : χ ≠ 1) {s : ℂ} (hs : 1 / 2 < s.re) : DifferentiableAt ℂ (quadraticConvolutionErrorIntegral χ) s

Holomorphy comes from the Mellin transform convergence strip, not from an assumed identity with a continued L-function.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.quadraticSiegelConvolution_ofReal_eq_zetaMul {q : ℕ} (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) (n : ℕ) : ↑(χ.quadraticSiegelConvolution n) = χ.zetaMul n

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.quadraticSiegelConvolutionSummatory_ofReal_eq_sum_zetaMul {q : ℕ} (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) (n : ℕ) : ↑(χ.quadraticSiegelConvolutionSummatory n) = ∑ k ∈ Finset.Icc 1 n, χ.zetaMul k

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.IsPrimitive.quadraticSiegelConvolutionSummatory_isBigO {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hprim : χ.IsPrimitive) (hχ : χ ≠ 1) : χ.quadraticSiegelConvolutionSummatory =O[Filter.atTop] fun (n : ℕ) => ↑n ^ 1

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.IsPrimitive.sum_zetaMul_isBigO {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hprim : χ.IsPrimitive) (hχ : χ ≠ 1) (hquad : χ ^ 2 = 1) : (fun (n : ℕ) => ∑ k ∈ Finset.Icc 1 n, χ.zetaMul k) =O[Filter.atTop] fun (n : ℕ) => ↑n ^ 1

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.IsPrimitive.riemannZeta_mul_LFunction_eq_errorIntegral_of_one_lt_re {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hprim : χ.IsPrimitive) (hχ : χ ≠ 1) (hquad : χ ^ 2 = 1) {s : ℂ} (hs : 1 < s.re) : riemannZeta s * DirichletCharacter.LFunction χ s = ↑(DirichletCharacter.LFunction χ 1).re * s / (s - 1) + s * quadraticConvolutionErrorIntegral χ s

Identification with the ordinary absolutely convergent Dirichlet product. This is the starting open set for analytic continuation.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.IsPrimitive.riemannZeta₁_mul_LFunction_eq_errorIntegral {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hprim : χ.IsPrimitive) (hχ : χ ≠ 1) (hquad : χ ^ 2 = 1) {s : ℂ} (hs : 1 / 2 < s.re) : riemannZeta₁ s * DirichletCharacter.LFunction χ s = ↑(DirichletCharacter.LFunction χ 1).re * s + (s - 1) * s * quadraticConvolutionErrorIntegral χ s

The pole-cleared product identity on the entire half-plane Re s > 1/2. The equality on Re s > 1 is continued by the identity theorem, using the holomorphic Mellin error and the entire regularization riemannZeta₁.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.IsPrimitive.riemannZeta_mul_LFunction_eq_errorIntegral {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hprim : χ.IsPrimitive) (hχ : χ ≠ 1) (hquad : χ ^ 2 = 1) {s : ℂ} (hs : 1 / 2 < s.re) (hs1 : s ≠ 1) : riemannZeta s * DirichletCharacter.LFunction χ s = ↑(DirichletCharacter.LFunction χ 1).re * s / (s - 1) + s * quadraticConvolutionErrorIntegral χ s

The actual continued product, represented by an absolutely convergent summatory-error integral throughout Re s > 1/2, away from its pole.