OAI/NumberTheory/TwoPoint/Halasz/HalaszHighPrimeInput.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The high-frequency part of the published prime-repulsion argument. The explicit input is the weaker constant 1/10 in (A.5)--(A.6) of Matomäki--Radziwiłł--Tao, An averaged form of Chowla's conjecture, arXiv:1503.05121v3, proof of Lemma A.4(ii), with the quantitative Vinogradov--Korobov estimate supplying prime-phase cancellation.

  1. def OAI.TwoPointCorrelations.HalaszHighPrimeInput line 14
  2. theorem OAI.TwoPointCorrelations.HalaszHighPrimeInput.distance_off_unit line 19
  3. theorem OAI.TwoPointCorrelations.HalaszHighPrimeInput.distance_cutoff line 45