OAI/NumberTheory/PrimeGaps/SingularSeries.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargePrimeGaps.residueCount line 13
  2. def OAI.LargePrimeGaps.singularLocal line 16
  3. def OAI.LargePrimeGaps.singularSeries line 19
  4. def OAI.LargePrimeGaps.singularTruncation line 22
  5. theorem OAI.LargePrimeGaps.residueCount_le_card line 25
  6. theorem OAI.LargePrimeGaps.residueCount_le_modulus line 28
  7. theorem OAI.LargePrimeGaps.singularLocal_nonneg line 38
  8. theorem OAI.LargePrimeGaps.singularLocal_empty line 48
  9. theorem OAI.LargePrimeGaps.singularLocal_singleton line 51
  10. theorem OAI.LargePrimeGaps.bernoulli_second_order line 61
  11. theorem OAI.LargePrimeGaps.generic_local_error line 80
  12. theorem OAI.LargePrimeGaps.residueCount_eq_card_of_large line 106
  13. theorem OAI.LargePrimeGaps.singularLocal_generic_error line 121
  14. theorem OAI.LargePrimeGaps.singularLocal_summable_error line 127
  15. theorem OAI.LargePrimeGaps.singularSeries_multipliable line 141
  16. theorem OAI.LargePrimeGaps.singularSeries_nonneg line 149
  17. theorem OAI.LargePrimeGaps.singularSeries_empty line 152
  18. theorem OAI.LargePrimeGaps.singularSeries_singleton line 155
  19. def OAI.LargePrimeGaps.tupleLocal line 160
  20. theorem OAI.LargePrimeGaps.missing_residue_card line 163
  21. theorem OAI.LargePrimeGaps.avoiding_tuple_count line 174
  22. theorem OAI.LargePrimeGaps.missing_residue_sum line 183
  23. theorem OAI.LargePrimeGaps.tupleLocal_sum line 199
  24. def OAI.LargePrimeGaps.differenceProduct line 217
  25. theorem OAI.LargePrimeGaps.differenceProduct_pos line 220
  26. theorem OAI.LargePrimeGaps.prime_dvd_differenceProduct_of_collision line 229
  27. theorem OAI.LargePrimeGaps.residueCount_eq_card_of_not_dvd line 240
  28. theorem OAI.LargePrimeGaps.differenceProduct_le line 247
  29. theorem OAI.LargePrimeGaps.abs_log_le_two_abs_sub_one line 261
  30. theorem OAI.LargePrimeGaps.abs_log_one_sub_le line 276
  31. theorem OAI.LargePrimeGaps.singularLocal_ge_half line 281
  32. theorem OAI.LargePrimeGaps.singularLocal_log_generic line 301
  33. theorem OAI.LargePrimeGaps.singularLocal_log_bound line 314
  34. theorem OAI.LargePrimeGaps.sum_reciprocal_sq_le line 340
  35. theorem OAI.LargePrimeGaps.prime_divisor_reciprocal_sum_le line 406
  36. def OAI.LargePrimeGaps.singularTailBound line 436
  37. theorem OAI.LargePrimeGaps.singularLocal_log_sum_bound line 440