A sublinear error for the genuine fourfold convolution #
This modern hyperbola argument combines the actual one-character main term, positivity, and the harmonic tail of the actual second pair.
theorem
DirichletCharacter.norm_sum_Ioc_twoCharacterConvolution_sub_residue_main_le
{q : ℕ}
[NeZero q]
(χ ψ : DirichletCharacter ℂ q)
(hχ : χ ≠ 1)
(hquad : χ ^ 2 = 1)
(hψ : ψ ≠ 1)
(hprod : χ * ψ ≠ 1)
(N : ℕ)
:
‖∑ n ∈ Finset.Ioc 0 N, (χ.twoCharacterConvolution ψ) n - ↑N * χ.twoCharacterResidue ψ‖ ≤ 300 * ↑q ^ 2 * ↑N ^ (3 / 4)
A genuinely sublinear uniform error, with the actual product of three L-values as main-term coefficient. The second character need not be quadratic; its two pair factors must be nonprincipal.
theorem
DirichletCharacter.norm_sum_Icc_twoCharacterConvolution_sub_residue_main_le
{q : ℕ}
[NeZero q]
(χ ψ : DirichletCharacter ℂ q)
(hχ : χ ≠ 1)
(hψ : ψ ≠ 1)
(hχquad : χ ^ 2 = 1)
(hψquad : ψ ^ 2 = 1)
(hne : χ ≠ ψ)
(N : ℕ)
:
‖∑ n ∈ Finset.Icc 1 N, (χ.twoCharacterConvolution ψ) n - ↑N * χ.twoCharacterResidue ψ‖ ≤ 300 * ↑q ^ 2 * ↑N ^ (3 / 4)
The common-level, distinct quadratic case, with no primitive or coprime conductor hypothesis.
theorem
DirichletCharacter.norm_twoCharacterResidue_le_eight_mul_modulus_cubed
{q : ℕ}
[NeZero q]
(χ ψ : DirichletCharacter ℂ q)
(hχ : χ ≠ 1)
(hψ : ψ ≠ 1)
(hprod : χ * ψ ≠ 1)
:
A crude uniform norm bound for the actual residue, used only to pay the change from a natural endpoint to a real endpoint.
theorem
DirichletCharacter.norm_sum_Icc_floor_twoCharacterConvolution_sub_residue_main_le
{q : ℕ}
[NeZero q]
(χ ψ : DirichletCharacter ℂ q)
(hχ : χ ≠ 1)
(hψ : ψ ≠ 1)
(hχquad : χ ^ 2 = 1)
(hψquad : ψ ^ 2 = 1)
(hne : χ ≠ ψ)
{X : ℝ}
(hX : 1 ≤ X)
:
‖∑ n ∈ Finset.Icc 1 ⌊X⌋₊, (χ.twoCharacterConvolution ψ) n - ↑X * χ.twoCharacterResidue ψ‖ ≤ 308 * ↑q ^ 3 * X ^ (3 / 4)
Real-endpoint version of the genuine fourfold main term. The additional power of the common modulus pays only the endpoint displacement.