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).
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.
Inspect dependencies
AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.IsPrimitive.abs_quadratic_convolution_sub_LValue_main_le · compiled type and proof/definition references.
Real-endpoint version, with the floor error paid by the actual harmonic tail estimate at one. This is the summatory input for partial summation.
Inspect dependencies
AnalyticNumberTheory.LargeSieve.Bombieri1965Theorem4.IsPrimitive.abs_quadratic_convolution_floor_sub_LValue_main_le · compiled type and proof/definition references.