OAI/NumberTheory/TwoPoint/Fourier/MinorArcPrimeRanges.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Verifying every dyadic hypothesis from the actual prime range.

  1. lemma OAI.TwoPointCorrelations.minor_arc_prime_range_dyadics line 12
  2. theorem OAI.TwoPointCorrelations.minor_arc_typical_prime_range_saving line 47