theorem DirichletCharacter.IsPrimitive.norm_weighted_fourierKernel_sum_le_four_mul_q_mul_one_add_log {q : ℕ} [NeZero q] {χ : DirichletCharacter ℂ q} (_hχ : χ.IsPrimitive) (hq : 1 < q) (M : ℕ) : ∑ j : ZMod q, ‖χ⁻¹ (-j) * ∑ n ∈ Finset.range M, ZMod.stdAddChar (j * ↑n)‖ ≤ 4 * ↑q * (1 + Real.log ↑q)

Explicit scan-free weighted Fourier-kernel bound with generous constant 4.

theorem DirichletCharacter.IsPrimitive.norm_sum_range_le_four_mul_sqrt_q_mul_one_add_log {q : ℕ} [NeZero q] {χ : DirichletCharacter ℂ q} (hχ : χ.IsPrimitive) (hq : 1 < q) (M : ℕ) : ‖∑ n ∈ Finset.range M, χ ↑n‖ ≤ 4 * √↑q * (1 + Real.log ↑q)

Primitive-character prefix bound deduced from exact Fourier completion and the weighted kernel estimate.

theorem DirichletCharacter.IsPrimitive.norm_LFunction_one_sub_harmonic_sum_le_eight_mul_sqrt_q_mul_one_add_log_div {q : ℕ} [NeZero q] {χ : DirichletCharacter ℂ q} (hχ : χ.IsPrimitive) (hχne : χ ≠ 1) (hq : 1 < q) {m : ℕ} (hm : 1 ≤ m) : ‖LFunction χ 1 - ∑ k ∈ Finset.range m, DirichletLAbelWeightVariation.cpowWeight 1 ↑k * χ ↑k‖ ≤ 8 * √↑q * (1 + Real.log ↑q) / ↑m

Integrated harmonic-tail bound from the explicit primitive prefix estimate.

theorem DirichletCharacter.IsPrimitive.abs_LFunction_one_re_sub_quadraticHarmonicTruncation_le_eight_mul_sqrt_q_mul_one_add_log_div {q : ℕ} [NeZero q] {χ : DirichletCharacter ℂ q} (hχ : χ.IsPrimitive) (hχne : χ ≠ 1) (hq : 1 < q) {m : ℕ} (hm : 1 ≤ m) : |(LFunction χ 1).re - χ.quadraticHarmonicTruncation m| ≤ 8 * √↑q * (1 + Real.log ↑q) / ↑m

Real quadratic truncation form of the same explicit harmonic-tail bound.