OAI/NumberTheory/TwoPoint/Halasz/HalaszGroupedEstimate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Apply the full triple-convolution estimate to one actual logarithmic band, with its adaptive denominator and finite cofactor prime cutoff.

  1. theorem OAI.TwoPointCorrelations.halasz_grouped_double_estimate line 14

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