OAI/NumberTheory/TwoPoint/Halasz/HalaszDoubleEstimate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Sum the actual geometric prime bands. The central terms retain the Halász saving, and both kinds of error have summable band weights.

  1. theorem OAI.TwoPointCorrelations.halasz_double_convolution_estimate line 14

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszDoubleEstimate.lean:14 (same declaration text).