The unprimitive one-character input to the fourfold asymptotic

This modern hyperbola argument uses complete periods, rather than Pólya--Vinogradov. Its constant is uniform in the actual common modulus.

theorem DirichletCharacter.sum_Ioc_zetaMul_eq_sqrt_hyperbola {q : ℕ} (χ : DirichletCharacter ℂ q) (N : ℕ) : ∑ n ∈ Finset.Ioc 0 N, χ.zetaMul n = ∑ a ∈ Finset.Ioc 0 N.sqrt, χ ↑a * ↑(N / a) + ∑ b ∈ Finset.Ioc 0 N.sqrt, ∑ a ∈ Finset.Ioc 0 (N / b), χ ↑a - ↑N.sqrt * ∑ a ∈ Finset.Ioc 0 N.sqrt, χ ↑a

Hyperbola identity specialized to the genuine convolution ζ * χ.

theorem DirichletCharacter.norm_LFunction_one_sub_sum_Ioc_div_le {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (m : ℕ) : ‖LFunction χ 1 - ∑ n ∈ Finset.Ioc 0 m, χ ↑n / ↑n‖ ≤ 2 * ↑q / (↑m + 1)

theorem DirichletCharacter.norm_sum_Ioc_zetaMul_sub_harmonic_main_le {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (N : ℕ) : ‖∑ n ∈ Finset.Ioc 0 N, χ.zetaMul n - ↑N * ∑ n ∈ Finset.Ioc 0 N.sqrt, χ ↑n / ↑n‖ ≤ 3 * ↑q * ↑N.sqrt

Complete-period control of the two short arms and the floor error.

theorem DirichletCharacter.norm_sum_Ioc_zetaMul_sub_LFunction_main_le {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (N : ℕ) : ‖∑ n ∈ Finset.Ioc 0 N, χ.zetaMul n - ↑N * LFunction χ 1‖ ≤ 7 * ↑q * √↑N

A uniform, actual complex main term for every nonprincipal character, including imprimitive characters at the common modulus.

theorem DirichletCharacter.norm_LFunction_one_le_two_mul_modulus {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) : ‖LFunction χ 1‖ ≤ 2 * ↑q

A uniform bound on the actual L-value, also valid for imprimitive characters.

theorem DirichletCharacter.sum_Ioc_norm_zetaMul_le_nine_mul_modulus {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (hquad : χ ^ 2 = 1) (N : ℕ) : ∑ n ∈ Finset.Ioc 0 N, ‖χ.zetaMul n‖ ≤ 9 * ↑q * ↑N

Linear growth of the positive quadratic coefficients with a uniform constant.