Uniform cancellation in the genuine two-character pair

This modern argument uses the classical two-variable hyperbola decomposition and complete character periods. It does not use primitivity, quadraticity, or coprime conductors. The pair is the actual Dirichlet convolution, not a nonnegative majorant. This is an unweighted summatory estimate, not yet a weighted main-term formula for the fourfold convolution.

theorem DirichletCharacter.sum_Ioc_convolution_eq_sqrt_hyperbola (f g : ArithmeticFunction ℂ) (N : ℕ) : ∑ n ∈ Finset.Ioc 0 N, (f * g) n = ∑ a ∈ Finset.Ioc 0 N.sqrt, f a * ∑ b ∈ Finset.Ioc 0 (N / a), g b + ∑ b ∈ Finset.Ioc 0 N.sqrt, g b * ∑ a ∈ Finset.Ioc 0 (N / b), f a - (∑ a ∈ Finset.Ioc 0 N.sqrt, f a) * ∑ b ∈ Finset.Ioc 0 N.sqrt, g b

Exact two-variable hyperbola identity at the integer square root.

theorem DirichletCharacter.norm_sum_Ioc_character_le_min {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (N : ℕ) : ‖∑ n ∈ Finset.Ioc 0 N, χ ↑n‖ ≤ min ↑N ↑q

Character sums up to a natural endpoint are bounded both by their length and, for a nonprincipal character, by the full modulus.

theorem DirichletCharacter.sum_Ioc_characterArithmeticFunction {q : ℕ} (χ : DirichletCharacter ℂ q) (N : ℕ) : ∑ n ∈ Finset.Ioc 0 N, (toArithmeticFunction fun (x : ℕ) => χ ↑x) n = ∑ n ∈ Finset.Ioc 0 N, χ ↑n

Character arithmetic-function sums agree with character sums on positive indices.

theorem DirichletCharacter.norm_sum_Ioc_character_pair_convolution_le_three_mul_nat_sqrt {q : ℕ} [NeZero q] (ψ η : DirichletCharacter ℂ q) (hψ : ψ ≠ 1) (hη : η ≠ 1) (N : ℕ) : ‖∑ n ∈ Finset.Ioc 0 N, ((toArithmeticFunction fun (x : ℕ) => ψ ↑x) * toArithmeticFunction fun (x : ℕ) => η ↑x) n‖ ≤ 3 * ↑q * ↑N.sqrt

Uniform cancellation for two arbitrary nonprincipal characters at a common nonzero modulus: the constant is 3, even with the integer square root. The overlap costs at most q * sqrt N, not q², because one short sum is bounded by its length.

theorem DirichletCharacter.norm_sum_Icc_character_pair_convolution_le_three_mul_sqrt {q : ℕ} [NeZero q] (ψ η : DirichletCharacter ℂ q) (hψ : ψ ≠ 1) (hη : η ≠ 1) (N : ℕ) : ‖∑ n ∈ Finset.Icc 1 N, ((toArithmeticFunction fun (x : ℕ) => ψ ↑x) * toArithmeticFunction fun (x : ℕ) => η ↑x) n‖ ≤ 3 * ↑q * √↑N

The standard real-square-root form of the genuine pair summatory bound.

theorem DirichletCharacter.norm_sum_Icc_floor_character_pair_convolution_le_three_mul_sqrt {q : ℕ} [NeZero q] (ψ η : DirichletCharacter ℂ q) (hψ : ψ ≠ 1) (hη : η ≠ 1) {X : ℝ} (hX : 0 ≤ X) : ‖∑ n ∈ Finset.Icc 1 ⌊X⌋₊, ((toArithmeticFunction fun (x : ℕ) => ψ ↑x) * toArithmeticFunction fun (x : ℕ) => η ↑x) n‖ ≤ 3 * ↑q * √X

The same bound at a real endpoint, including endpoints below 1.

theorem DirichletCharacter.norm_sum_Icc_character_twist_zetaMul_le_three_mul_sqrt {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (hψ : ψ ≠ 1) (hχψ : χ * ψ ≠ 1) (N : ℕ) : ‖∑ n ∈ Finset.Icc 1 N, ψ ↑n * χ.zetaMul n‖ ≤ 3 * ↑q * √↑N

Cancellation for the actual pair b = ψ * (χψ) in the fourfold convolution, written as its exact twist ψ(n) (ζ * χ)(n).

theorem DirichletCharacter.norm_sum_Icc_floor_character_twist_zetaMul_le_three_mul_sqrt {q : ℕ} [NeZero q] (χ ψ : DirichletCharacter ℂ q) (hψ : ψ ≠ 1) (hχψ : χ * ψ ≠ 1) {X : ℝ} (hX : 0 ≤ X) : ‖∑ n ∈ Finset.Icc 1 ⌊X⌋₊, ψ ↑n * χ.zetaMul n‖ ≤ 3 * ↑q * √X

Real-endpoint form for the actual twisted pair.