OAI/NumberTheory/PrimeGaps/BoxMeans.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargePrimeGaps.distinctBox line 13
  2. def OAI.LargePrimeGaps.truncatedBoxMean line 16
  3. def OAI.LargePrimeGaps.distinctTruncatedBoxMean line 19
  4. def OAI.LargePrimeGaps.singularBoxMean line 22
  5. theorem OAI.LargePrimeGaps.siftedTuple_boxTuple line 25
  6. theorem OAI.LargePrimeGaps.truncatedBoxMean_bounds line 32
  7. theorem OAI.LargePrimeGaps.distinctTruncatedBoxMean_nonneg line 63
  8. theorem OAI.LargePrimeGaps.distinctTruncatedBoxMean_le line 71
  9. theorem OAI.LargePrimeGaps.truncatedBoxMean_sub_distinct_le line 79
  10. def OAI.LargePrimeGaps.boxTruncationError line 115
  11. theorem OAI.LargePrimeGaps.distinctTruncatedBoxMean_error line 118
  12. def OAI.LargePrimeGaps.uniformSingularTailBound line 135
  13. theorem OAI.LargePrimeGaps.singularTailBound_le_uniform line 139
  14. def OAI.LargePrimeGaps.boxDiameterBound line 166
  15. theorem OAI.LargePrimeGaps.uniformSingularTailBound_nonneg line 169
  16. theorem OAI.LargePrimeGaps.singularBoxMean_sub_truncation line 176
  17. theorem OAI.LargePrimeGaps.singularBoxMean_error line 214
  18. def OAI.LargePrimeGaps.singularCutoffScale line 233
  19. def OAI.LargePrimeGaps.singularCutoff line 235
  20. theorem OAI.LargePrimeGaps.singularCutoffScale_pos line 237
  21. theorem OAI.LargePrimeGaps.singularCutoff_tendsto line 241
  22. theorem OAI.LargePrimeGaps.singularCutoff_ratio_tendsto line 245
  23. theorem OAI.LargePrimeGaps.log_div_singularCutoff_tendsto line 252
  24. theorem OAI.LargePrimeGaps.primorial_singularCutoff_power_bound line 257
  25. theorem OAI.LargePrimeGaps.primorial_singularCutoff_ratio_tendsto line 277
  26. theorem OAI.LargePrimeGaps.primorial_singularCutoff_div_tendsto line 296
  27. theorem OAI.LargePrimeGaps.log_mul_div_singularCutoff_tendsto line 300
  28. theorem OAI.LargePrimeGaps.uniformSingularTailBound_tendsto line 311
  29. theorem OAI.LargePrimeGaps.boxTruncationError_tendsto line 325
  30. def OAI.LargePrimeGaps.singularBoxError line 338
  31. theorem OAI.LargePrimeGaps.singularBoxError_tendsto line 343
  32. theorem OAI.LargePrimeGaps.singularBoxMean_error_eventually line 351
  33. theorem OAI.LargePrimeGaps.singularBoxMean_uniform line 365