The harmonic tail of the genuine character pair

This modern partial-summation argument combines square-root cancellation with the proved Mellin continuation. The constant in the harmonic approximation is the actual product of L-values at one.

theorem DirichletCharacter.LFunction_one_mul_sub_characterPair_harmonic_eq {q : ℕ} [NeZero q] (ψ η : DirichletCharacter ℂ q) (hψ : ψ ≠ 1) (hη : η ≠ 1) {m : ℕ} (hm : 1 ≤ m) : LFunction ψ 1 * LFunction η 1 - ∑ n ∈ Finset.Icc 1 m, ((toArithmeticFunction fun (x : ℕ) => ψ ↑x) * toArithmeticFunction fun (x : ℕ) => η ↑x) n / ↑n = (∫ (t : ℝ) in Set.Ioi ↑m, ψ.characterPairKernel η 1 t) - ψ.characterPairSummatory η ↑m / ↑m

An exact tail identity with the actual product of L-values.

theorem DirichletCharacter.norm_characterPairKernel_one_le {q : ℕ} [NeZero q] (ψ η : DirichletCharacter ℂ q) (hψ : ψ ≠ 1) (hη : η ≠ 1) {t : ℝ} (ht : 0 < t) : ‖ψ.characterPairKernel η 1 t‖ ≤ 3 * ↑q * t ^ (-3 / 2)

theorem DirichletCharacter.norm_integral_Ioi_characterPairKernel_one_le {q : ℕ} [NeZero q] (ψ η : DirichletCharacter ℂ q) (hψ : ψ ≠ 1) (hη : η ≠ 1) {x : ℝ} (hx : 0 < x) : ‖∫ (t : ℝ) in Set.Ioi x, ψ.characterPairKernel η 1 t‖ ≤ 6 * ↑q / √x

The convergent integral tail costs at most 6 q / sqrt m.

theorem DirichletCharacter.norm_LFunction_one_mul_sub_characterPair_harmonic_le {q : ℕ} [NeZero q] (ψ η : DirichletCharacter ℂ q) (hψ : ψ ≠ 1) (hη : η ≠ 1) {m : ℕ} (hm : 1 ≤ m) : ‖LFunction ψ 1 * LFunction η 1 - ∑ n ∈ Finset.Icc 1 m, ((toArithmeticFunction fun (x : ℕ) => ψ ↑x) * toArithmeticFunction fun (x : ℕ) => η ↑x) n / ↑n‖ ≤ 9 * ↑q / √↑m

Quantitative conditional harmonic convergence to the actual L-value product, uniform at the common modulus.