The actual one-character convolution main term #
The floor-sum discrepancy and the genuine harmonic tail give a uniform
O(q sqrt X) error for the summatory convolution 1 * chi. This is an
unconditional arithmetic input to the weighted positive-convolution route,
not a lower-bound assumption on L(1, chi).
theorem
AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.IsPrimitive.abs_quadratic_convolution_sub_LValue_main_le
{q : ℕ}
[NeZero q]
(χ : DirichletCharacter ℂ q)
(hprim : χ.IsPrimitive)
(hχ : χ ≠ 1)
(X : ℕ)
:
Uniform main-term estimate for the real convolution summatory function. Quadraticity is not needed for the error estimate itself; it makes the coefficients nonnegative when this is used in the Siegel argument.
theorem
AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.IsPrimitive.abs_quadratic_convolution_floor_sub_LValue_main_le
{q : ℕ}
[NeZero q]
(χ : DirichletCharacter ℂ q)
(hprim : χ.IsPrimitive)
(hχ : χ ≠ 1)
{x : ℝ}
(hx : 1 ≤ x)
:
Real-endpoint version, with the floor error paid by the actual harmonic tail estimate at one. This is the summatory input for partial summation.