OAI/NumberTheory/PrimeGaps/DetectorMoments.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LargePrimeGaps.extra_cumulative_pair_limit line 27
  2. theorem OAI.LargePrimeGaps.extra_cumulative_square_limit line 75
  3. theorem OAI.LargePrimeGaps.extra_cumulative_cross_limit line 90
  4. theorem OAI.LargePrimeGaps.orderedWeight_extra_limit line 106
  5. theorem OAI.LargePrimeGaps.distinctBox_pair_iff line 151
  6. theorem OAI.LargePrimeGaps.sum_distinctBox_pair line 169
  7. theorem OAI.LargePrimeGaps.sum_first_interval line 182
  8. theorem OAI.LargePrimeGaps.sum_first_offdiagonal line 191
  9. theorem OAI.LargePrimeGaps.extraAverage_pair_identity line 206
  10. theorem OAI.LargePrimeGaps.unorderedWeight_extra_pair_limit line 231
  11. theorem OAI.LargePrimeGaps.unorderedWeight_detector_bound line 249
  12. theorem OAI.LargePrimeGaps.index_density_of_bombieriVinogradov line 288