OAI/NumberTheory/TwoPoint/Halasz/HalaszLargeMinimum.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A large minimum gives the same cofactor saving at every frequency; no prime-repulsion input is needed in this case.

  1. lemma OAI.TwoPointCorrelations.halasz_large_minimum_cutoff line 11
  2. theorem OAI.TwoPointCorrelations.halasz_large_minimum_actual_cofactor line 32
  3. theorem OAI.TwoPointCorrelations.halasz_large_minimum_extra_cofactor line 80