OAI/NumberTheory/PrimeGaps/Detectors.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LargePrimeGaps.pattern_singular_sum line 27
  2. theorem OAI.LargePrimeGaps.ker_comp_injective line 39
  3. theorem OAI.LargePrimeGaps.numericPattern_int_ker line 45
  4. theorem OAI.LargePrimeGaps.shiftFamily_eq_of_ker line 50
  5. def OAI.LargePrimeGaps.equalityPatternFamily line 62
  6. theorem OAI.LargePrimeGaps.equalityPatternFamily_sign_sum line 65
  7. theorem OAI.LargePrimeGaps.translated_shiftFamily line 86
  8. theorem OAI.LargePrimeGaps.divisorSum_fin_zero line 98
  9. theorem OAI.LargePrimeGaps.divisorSum_singleton_at_prime line 110
  10. theorem OAI.LargePrimeGaps.theta_div_log_le_upper line 118
  11. theorem OAI.LargePrimeGaps.singleton_divisor_majorant line 127
  12. theorem OAI.LargePrimeGaps.sum_square_diagonal_offdiag line 138
  13. theorem OAI.LargePrimeGaps.detector_square_majorant line 147
  14. def OAI.LargePrimeGaps.patternBoxShifts line 180
  15. theorem OAI.LargePrimeGaps.patternBoxShifts_family line 184
  16. theorem OAI.LargePrimeGaps.patternBoxShifts_image line 202
  17. theorem OAI.LargePrimeGaps.surjective_shiftFamily_sign_sum line 216
  18. theorem OAI.LargePrimeGaps.box_sum_scaled_norm_le line 232
  19. theorem OAI.LargePrimeGaps.box_sum_errors_tendsto_zero line 258
  20. theorem OAI.LargePrimeGaps.natural_boxDiameterBound line 273
  21. theorem OAI.LargePrimeGaps.unmarked_box_pattern_limit line 284
  22. theorem OAI.LargePrimeGaps.average_mono line 356
  23. theorem OAI.LargePrimeGaps.average_add line 360
  24. theorem OAI.LargePrimeGaps.average_const_mul line 365
  25. theorem OAI.LargePrimeGaps.average_finset_sum line 369
  26. theorem OAI.LargePrimeGaps.weighted_detector_square_majorant line 374
  27. theorem OAI.LargePrimeGaps.detector_log_ratio_tendsto line 411
  28. theorem OAI.LargePrimeGaps.exists_normalized_singleton_profile line 440
  29. theorem OAI.LargePrimeGaps.exists_detector_profile line 467