Weighted sums of the genuine two-character convolution

Modern Abel summation identifies the actual continued four-factor product as the constant term. The summatory error supplies an explicit endpoint and tail remainder. Positivity is used only for the lower bound on the finite sum. No zero existence or uniform Siegel bound is assumed or asserted.

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

The finite weighted sum of the real parts of the actual coefficients. For two quadratic characters these are the coefficients themselves.

Equations

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

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

Exact Abel summation, without any quadraticity hypothesis.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.re_twoCharacterErrorKernel_ofReal {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (β : ℝ) {t : ℝ} (ht : 0 ≤ t) : (twoCharacterErrorKernel χ ψ (↑β) t).re = (twoCharacterError χ ψ t).re * t ^ (-β - 1)

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.integrableOn_re_twoCharacterErrorKernel {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (hχquad : χ ^ 2 = 1) (hψ : ψ ≠ 1) (hprod : χ * ψ ≠ 1) {β : ℝ} (hβ : 3 / 4 < β) : MeasureTheory.IntegrableOn (fun (t : ℝ) => (twoCharacterError χ ψ t).re * t ^ (-β - 1)) (Set.Ioi 1) MeasureTheory.volume

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.re_twoCharacter_product_eq_errorIntegral {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (hχquad : χ ^ 2 = 1) (hψ : ψ ≠ 1) (hprod : χ * ψ ≠ 1) {β : ℝ} (hβ : 3 / 4 < β) (hβ1 : β ≠ 1) : (riemannZeta ↑β * DirichletCharacter.LFunction χ ↑β * DirichletCharacter.LFunction ψ ↑β * DirichletCharacter.LFunction (χ * ψ) ↑β).re = (χ.twoCharacterResidue ψ).re * β / (β - 1) + β * ∫ (t : ℝ) in Set.Ioi 1, (twoCharacterError χ ψ t).re * t ^ (-β - 1)

Real-part specialization of the actual continued constant.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.abs_re_twoCharacterError_le {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (hχquad : χ ^ 2 = 1) (hψ : ψ ≠ 1) (hprod : χ * ψ ≠ 1) {t : ℝ} (ht : 1 ≤ t) : |(twoCharacterError χ ψ t).re| ≤ 308 * ↑q ^ 3 * t ^ (3 / 4)

The real-part error inherits the proved complex norm bound.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.abs_re_twoCharacterError_tail_le {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (hχquad : χ ^ 2 = 1) (hψ : ψ ≠ 1) (hprod : χ * ψ ≠ 1) {β x : ℝ} (hβ : 3 / 4 < β) (hx : 1 ≤ x) : |∫ (t : ℝ) in Set.Ioi x, (twoCharacterError χ ψ t).re * t ^ (-β - 1)| ≤ 308 * ↑q ^ 3 * x ^ (3 / 4 - β) / (β - 3 / 4)

An explicit bound for the actual convergent error tail.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.twoCharacterWeightedSum_eq_product_add_tail {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (hχquad : χ ^ 2 = 1) (hψ : ψ ≠ 1) (hprod : χ * ψ ≠ 1) {β x : ℝ} (hβ : 3 / 4 < β) (hβ1 : β ≠ 1) (hx : 1 ≤ x) : twoCharacterWeightedSum χ ψ β x = (χ.twoCharacterResidue ψ).re * x ^ (1 - β) / (1 - β) + (riemannZeta ↑β * DirichletCharacter.LFunction χ ↑β * DirichletCharacter.LFunction ψ ↑β * DirichletCharacter.LFunction (χ * ψ) ↑β).re + (twoCharacterError χ ψ x).re * x ^ (-β) - β * ∫ (t : ℝ) in Set.Ioi x, (twoCharacterError χ ψ t).re * t ^ (-β - 1)

Exact finite expansion with the actual continued product as constant, and with the endpoint and tail terms both displayed.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.abs_twoCharacterWeightedSum_sub_main_sub_product_le {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (hχquad : χ ^ 2 = 1) (hψ : ψ ≠ 1) (hprod : χ * ψ ≠ 1) {β x : ℝ} (hβ : 3 / 4 < β) (hβ1 : β ≠ 1) (hx : 1 ≤ x) : |twoCharacterWeightedSum χ ψ β x - (χ.twoCharacterResidue ψ).re * x ^ (1 - β) / (1 - β) - (riemannZeta ↑β * DirichletCharacter.LFunction χ ↑β * DirichletCharacter.LFunction ψ ↑β * DirichletCharacter.LFunction (χ * ψ) ↑β).re| ≤ 308 * ↑q ^ 3 * (1 + β / (β - 3 / 4)) * x ^ (3 / 4 - β)

The explicit weighted asymptotic, valid for every β > 3/4, apart from the pole.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.one_le_twoCharacterWeightedSum {q : ℕ} (χ ψ : DirichletCharacter ℂ q) (hχquad : χ ^ 2 = 1) (hψquad : ψ ^ 2 = 1) (β : ℝ) {x : ℝ} (hx : 1 ≤ x) : 1 ≤ twoCharacterWeightedSum χ ψ β x

Positivity of every actual coefficient, and the coefficient at one, imply the finite weighted sum is at least one for every real exponent.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.twoCharacter_weighted_error_at_large_endpoint_le {q : ℕ} [NeZero q] {β : ℝ} (hβ : 7 / 8 ≤ β) : 308 * ↑q ^ 3 * (1 + β / (β - 3 / 4)) * ((5000 * ↑q ^ 3) ^ 8) ^ (3 / 4 - β) ≤ 1 / 2

The explicit endpoint (5000 q^3)^8 pays the entire error uniformly for β ≥ 7/8. The proof uses monotonicity of real powers, not a finite scan.

theorem AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.twoCharacterResidue_re_lower_bound_of_real_zero {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (hψ : ψ ≠ 1) (hχquad : χ ^ 2 = 1) (hψquad : ψ ^ 2 = 1) (hne : χ ≠ ψ) {β : ℝ} (hβ : 7 / 8 ≤ β) (hβ1 : β < 1) (hzero : DirichletCharacter.LFunction χ ↑β = 0 ∨ DirichletCharacter.LFunction ψ ↑β = 0 ∨ DirichletCharacter.LFunction (χ * ψ) ↑β = 0) : (1 - β) / (2 * ((5000 * ↑q ^ 3) ^ 8) ^ (1 - β)) ≤ (χ.twoCharacterResidue ψ).re

A residue lower bound conditional on an actual real zero of one of the three L-functions. No zero existence is included in the statement.