Weighted quadratic convolution and its actual continued constant

This modern partial-summation argument keeps the finite sum and its tail explicit. The constant is the actual continued product, not a free parameter.

noncomputable def AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.quadraticConvolutionWeightedSum {q : ℕ} (χ : DirichletCharacter ℂ q) (β x : ℝ) : ℝ

The finite weighted sum of the actual convolution coefficients.

Equations

• AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.quadraticConvolutionWeightedSum χ β x = ∑ n ∈ Finset.Icc 1 ⌊x⌋₊, χ.quadraticSiegelConvolution n * ↑n ^ (-β)

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.quadraticConvolutionWeightedSum_eq_abel {q : ℕ} (χ : DirichletCharacter ℂ q) (β x : ℝ) : quadraticConvolutionWeightedSum χ β x = x ^ (-β) * χ.quadraticSiegelConvolutionSummatory ⌊x⌋₊ + β * ∫ (t : ℝ) in Set.Ioc 1 x, χ.quadraticSiegelConvolutionSummatory ⌊t⌋₊ * t ^ (-β - 1)

Exact Abel summation, valid for any real exponent.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.quadraticConvolutionErrorKernel_ofReal {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (β : ℝ) {t : ℝ} (ht : 0 ≤ t) : quadraticConvolutionErrorKernel χ (↑β) t = ↑(quadraticConvolutionError χ t * t ^ (-β - 1))

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.IsPrimitive.integrableOn_real_quadraticConvolutionErrorKernel {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hprim : χ.IsPrimitive) (hχ : χ ≠ 1) {β : ℝ} (hβ : 1 / 2 < β) : MeasureTheory.IntegrableOn (fun (t : ℝ) => quadraticConvolutionError χ t * t ^ (-β - 1)) (Set.Ioi 1) MeasureTheory.volume

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.IsPrimitive.re_riemannZeta_mul_LFunction_eq_real_errorIntegral {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hprim : χ.IsPrimitive) (hχ : χ ≠ 1) (hquad : χ ^ 2 = 1) {β : ℝ} (hβ : 1 / 2 < β) (hβ1 : β ≠ 1) : (riemannZeta ↑β * DirichletCharacter.LFunction χ ↑β).re = (DirichletCharacter.LFunction χ 1).re * β / (β - 1) + β * ∫ (t : ℝ) in Set.Ioi 1, quadraticConvolutionError χ t * t ^ (-β - 1)

The real form of the Mellin constant identification.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.IsPrimitive.abs_quadraticConvolutionError_tail_le {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hprim : χ.IsPrimitive) (hχ : χ ≠ 1) {β x : ℝ} (hβ : 1 / 2 < β) (hx : 1 ≤ x) : |∫ (t : ℝ) in Set.Ioi x, quadraticConvolutionError χ t * t ^ (-β - 1)| ≤ 81 * ↑q * x ^ (1 / 2 - β) / (β - 1 / 2)

Explicit tail payment for the actual summatory error.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.IsPrimitive.quadraticConvolutionWeightedSum_eq_product_add_tail {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hprim : χ.IsPrimitive) (hχ : χ ≠ 1) (hquad : χ ^ 2 = 1) {β x : ℝ} (hβ : 1 / 2 < β) (hβ1 : β ≠ 1) (hx : 1 ≤ x) : quadraticConvolutionWeightedSum χ β x = (DirichletCharacter.LFunction χ 1).re * x ^ (1 - β) / (1 - β) + (riemannZeta ↑β * DirichletCharacter.LFunction χ ↑β).re + quadraticConvolutionError χ x * x ^ (-β) - β * ∫ (t : ℝ) in Set.Ioi x, quadraticConvolutionError χ t * t ^ (-β - 1)

Weighted finite expansion with the actual continued product as constant. The error is exactly one endpoint term minus one convergent tail integral.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.IsPrimitive.abs_quadraticConvolutionWeightedSum_sub_main_sub_product_le {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hprim : χ.IsPrimitive) (hχ : χ ≠ 1) (hquad : χ ^ 2 = 1) {β x : ℝ} (hβ : 1 / 2 < β) (hβ1 : β ≠ 1) (hx : 1 ≤ x) : |quadraticConvolutionWeightedSum χ β x - (DirichletCharacter.LFunction χ 1).re * x ^ (1 - β) / (1 - β) - (riemannZeta ↑β * DirichletCharacter.LFunction χ ↑β).re| ≤ 81 * ↑q * (1 + β / (β - 1 / 2)) * x ^ (1 / 2 - β)

Uniform explicit weighted asymptotic for every β > 1/2, except the pole. All dependence on the exponent is displayed.