OAI/NumberTheory/TwoPoint/ShortIntervals/MRTNoSmallMeasure.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual no-small frequency class is covered by large values in any selected band, in particular the final band. All moment costs remain explicit.

  1. def OAI.TwoPointCorrelations.mrtShortPrimeLargeCost line 15
  2. theorem OAI.TwoPointCorrelations.mrt_short_prime_large_measure line 18
  3. theorem OAI.TwoPointCorrelations.mrt_no_small_log_measure line 48