OAI/NumberTheory/PrimeGaps/MangoldtBounds.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LargePrimeGaps.theta_le_vonMangoldt line 13
  2. theorem OAI.LargePrimeGaps.sum_vonMangoldt_sub_theta line 18
  3. theorem OAI.LargePrimeGaps.residueSlice_nonneg line 24
  4. theorem OAI.LargePrimeGaps.residueSlice_primepower_error line 27
  5. theorem OAI.LargePrimeGaps.residueSlice_theta_le line 47
  6. theorem OAI.LargePrimeGaps.residueSlice_theta_shift_error line 65
  7. def OAI.LargePrimeGaps.endpointError line 87
  8. theorem OAI.LargePrimeGaps.endpointClassError_le line 92
  9. def OAI.LargePrimeGaps.BombieriVinogradov line 101
  10. theorem OAI.LargePrimeGaps.residueSlice_vonMangoldt_endpoint_error line 107
  11. theorem OAI.LargePrimeGaps.markedClassError_le_endpointErrors line 122
  12. theorem OAI.LargePrimeGaps.markedError_le_endpointErrors line 152
  13. theorem OAI.LargePrimeGaps.sum_markedError_le_endpointErrors line 174
  14. def OAI.LargePrimeGaps.powerModulus line 185
  15. theorem OAI.LargePrimeGaps.eventually_rpow_le_BV_range line 187
  16. theorem OAI.LargePrimeGaps.endpoint_error_sum_nonneg line 202
  17. theorem OAI.LargePrimeGaps.endpoint_sum_log_decay line 205
  18. theorem OAI.LargePrimeGaps.polylog_shift_eventually_le line 256
  19. theorem OAI.LargePrimeGaps.log_shift_bound line 272
  20. theorem OAI.LargePrimeGaps.power_log_identity line 281
  21. theorem OAI.LargePrimeGaps.primepower_shift_tail_log_decay line 288
  22. theorem OAI.LargePrimeGaps.marked_error_sum_log_decay line 356
  23. theorem OAI.LargePrimeGaps.harmonic_nonneg_real line 379
  24. theorem OAI.LargePrimeGaps.harmonic_le_twice_log line 383
  25. theorem OAI.LargePrimeGaps.powerModulus_le line 391
  26. theorem OAI.LargePrimeGaps.marked_error_weight_budget line 399
  27. def OAI.LargePrimeGaps.weightedErrorSum line 426
  28. theorem OAI.LargePrimeGaps.weightedErrorSum_nonneg line 430
  29. theorem OAI.LargePrimeGaps.weightedErrorSum_sq_bound line 436
  30. theorem OAI.LargePrimeGaps.weightedErrorSum_log_decay line 453
  31. theorem OAI.LargePrimeGaps.marked_arithmetic_error_log_decay line 495