OAI/NumberTheory/PrimeGaps/DivisorSums.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargePrimeGaps.logCoordinates line 9
  2. def OAI.LargePrimeGaps.divisorCoefficient line 12
  3. def OAI.LargePrimeGaps.divisorSum line 16
  4. def OAI.LargePrimeGaps.HasBudget line 20
  5. theorem OAI.LargePrimeGaps.divisorCoefficient_ne_zero_iff line 23
  6. theorem OAI.LargePrimeGaps.logCoordinates_nonneg line 31
  7. theorem OAI.LargePrimeGaps.divisor_product_bound line 35
  8. theorem OAI.LargePrimeGaps.divisor_coordinate_bound line 54
  9. theorem OAI.LargePrimeGaps.abs_divisorCoefficient_le line 65
  10. theorem OAI.LargePrimeGaps.divisorSum_eq_bounded line 77
  11. def OAI.LargePrimeGaps.residueStarts line 107
  12. theorem OAI.LargePrimeGaps.residueStarts_card_error line 110
  13. def OAI.LargePrimeGaps.tupleModulus line 181
  14. theorem OAI.LargePrimeGaps.tupleModulus_pos line 183
  15. theorem OAI.LargePrimeGaps.tupleModulus_dvd_prod line 188
  16. theorem OAI.LargePrimeGaps.tupleModulus_le_prod line 192
  17. theorem OAI.LargePrimeGaps.modEq_lcm_iff line 196
  18. theorem OAI.LargePrimeGaps.tuple_divisibility_iff_modEq line 210
  19. def OAI.LargePrimeGaps.tupleCompatible line 222
  20. theorem OAI.LargePrimeGaps.compatible_of_solution line 225
  21. def OAI.LargePrimeGaps.localCompatible line 231
  22. theorem OAI.LargePrimeGaps.localCompatible_of_tupleCompatible line 235
  23. theorem OAI.LargePrimeGaps.squarefree_dvd_of_prime_dvd line 243
  24. theorem OAI.LargePrimeGaps.tupleCompatible_of_localCompatible line 252
  25. theorem OAI.LargePrimeGaps.tupleCompatible_iff_localCompatible line 291
  26. def OAI.LargePrimeGaps.tupleStarts line 296
  27. theorem OAI.LargePrimeGaps.tupleStarts_eq_residueStarts line 299
  28. theorem OAI.LargePrimeGaps.tupleStarts_eq_empty_of_incompatible line 307
  29. theorem OAI.LargePrimeGaps.tupleStarts_card_error line 315
  30. theorem OAI.LargePrimeGaps.tupleModulus_squarefree line 322
  31. theorem OAI.LargePrimeGaps.not_prime_on_nonreduced_class line 334
  32. def OAI.LargePrimeGaps.tupleDensity line 344
  33. theorem OAI.LargePrimeGaps.tupleStarts_density_error line 348
  34. theorem OAI.LargePrimeGaps.sum_divisibility_eq_counts line 356
  35. theorem OAI.LargePrimeGaps.finite_density_sum_error line 367
  36. def OAI.LargePrimeGaps.positiveProductTuples line 398
  37. theorem OAI.LargePrimeGaps.positiveProductTuples_card_bound line 401
  38. theorem OAI.LargePrimeGaps.positiveProductTuples_card_log_bound line 444