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.sum_Ioc_norm_zetaMul_div_sqrt_le {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (hquad : χ ^ 2 = 1) (m : ℕ) : ∑ n ∈ Finset.Ioc 0 m, ‖χ.zetaMul n‖ / √↑n ≤ 18 * ↑q * √↑m

Partial summation of the positive coefficients with the square-root weight.

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) : ‖χ.twoCharacterResidue ψ‖ ≤ 8 * ↑q ^ 3

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.