OAI/NumberTheory/TwoPointCorrelations/HalaszLocalMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Localize the Halasz distance hypothesis to the frequency window actually used by a reciprocal-count cofactor. This allows a distant frequency to be treated even when the minimizing twist is close to zero.

  1. theorem OAI.TwoPointCorrelations.halasz_local_count_prefix line 14