OAI/NumberTheory/TwoPoint/Halasz/HalaszPublishedPrime.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The precise published prime-supported sparse estimate needed for the extra-prime argument. HalaszPrimeSparseInput specializes Matomäki--Radziwiłł, Multiplicative functions in short intervals, Annals 183 (2016), Lemma 11 (arXiv:1501.04585v4), to T=exp L and epsilon=1/12. Replacing log Y by log p costs at most an absolute factor on [Y,2Y].

  1. def OAI.TwoPointCorrelations.HalaszPrimeSparseInput line 15
  2. lemma OAI.TwoPointCorrelations.halasz_sparse_prime_error line 25
  3. theorem OAI.TwoPointCorrelations.HalaszPrimeSparseInput.short_prime_energy line 65