OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/LogCoef.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryPrimeSupply.logCoef line 24
  2. theorem OAI.OrdinaryPrimeSupply.logCoef_nonneg line 26
  3. theorem OAI.OrdinaryPrimeSupply.logCoef_le_one line 29
  4. theorem OAI.OrdinaryPrimeSupply.logCoef_abscissa line 36
  5. theorem OAI.OrdinaryPrimeSupply.logMul_logCoef line 43
  6. def OAI.OrdinaryPrimeSupply.smoothMass line 64
  7. theorem OAI.OrdinaryPrimeSupply.hasDerivAt_smoothMass line 67
  8. def OAI.OrdinaryPrimeSupply.regularPart line 76
  9. theorem OAI.OrdinaryPrimeSupply.series_real_eq_regular line 78
  10. theorem OAI.OrdinaryPrimeSupply.hasDerivAt_adjusted line 91
  11. theorem OAI.OrdinaryPrimeSupply.regularPart_continuousOn line 100
  12. theorem OAI.OrdinaryPrimeSupply.smoothMass_log_bound line 106
  13. theorem OAI.OrdinaryPrimeSupply.real_LSeries_eq_tsum line 138
  14. theorem OAI.OrdinaryPrimeSupply.smoothMass_eq_tsum line 152
  15. theorem OAI.OrdinaryPrimeSupply.residueSeries_eq line 156
  16. theorem OAI.OrdinaryPrimeSupply.logCoef_mul_log line 162
  17. theorem OAI.OrdinaryPrimeSupply.residueSeries_summable line 171
  18. theorem OAI.OrdinaryPrimeSupply.smoothSeries_summable line 176
  19. theorem OAI.OrdinaryPrimeSupply.scaled_residueSeries_bound line 181
  20. theorem OAI.OrdinaryPrimeSupply.exp_sub_one_le_three_mul line 197
  21. theorem OAI.OrdinaryPrimeSupply.rpow_one_add line 206
  22. theorem OAI.OrdinaryPrimeSupply.small_smoothing line 210
  23. theorem OAI.OrdinaryPrimeSupply.tail_smoothing line 219
  24. def OAI.OrdinaryPrimeSupply.cutoffTerm line 224
  25. def OAI.OrdinaryPrimeSupply.sharpMass line 227
  26. theorem OAI.OrdinaryPrimeSupply.cutoffTerm_summable line 230
  27. theorem OAI.OrdinaryPrimeSupply.tsum_cutoffTerm line 239
  28. theorem OAI.OrdinaryPrimeSupply.smoothing_parameters line 247
  29. theorem OAI.OrdinaryPrimeSupply.cutoffTerm_upper line 255
  30. theorem OAI.OrdinaryPrimeSupply.smoothTerm_upper line 279
  31. theorem OAI.OrdinaryPrimeSupply.sharp_smooth_bound line 309
  32. theorem OAI.OrdinaryPrimeSupply.sharpMass_loglog_bound line 331
  33. def OAI.OrdinaryPrimeSupply.primeMass line 345
  34. theorem OAI.OrdinaryPrimeSupply.logCoef_prime line 349
  35. def OAI.OrdinaryPrimeSupply.nonprimeTerm line 356
  36. theorem OAI.OrdinaryPrimeSupply.nonprimeTerm_nonneg line 358
  37. theorem OAI.OrdinaryPrimeSupply.nonprimeTerm_summable line 362
  38. theorem OAI.OrdinaryPrimeSupply.sharpMass_eq_primeMass_add line 388
  39. theorem OAI.OrdinaryPrimeSupply.sharp_prime_bound line 400
  40. theorem OAI.OrdinaryPrimeSupply.primeMass_loglog_bound line 407
  41. def OAI.OrdinaryPrimeSupply.primeRange line 419
  42. theorem OAI.OrdinaryPrimeSupply.mem_primeRange line 422
  43. def OAI.OrdinaryPrimeSupply.logPrimeWindow line 428
  44. def OAI.OrdinaryPrimeSupply.logWindowMass line 431
  45. theorem OAI.OrdinaryPrimeSupply.mem_logPrimeWindow line 433
  46. theorem OAI.OrdinaryPrimeSupply.primeRange_mono line 444
  47. theorem OAI.OrdinaryPrimeSupply.window_upper line 450
  48. theorem OAI.OrdinaryPrimeSupply.window_lower line 473
  49. theorem OAI.OrdinaryPrimeSupply.logWindowMass_bound line 499
  50. theorem OAI.OrdinaryPrimeSupply.mod_five_window_supplies line 521
  51. theorem OAI.OrdinaryPrimeSupply.logPrimeWindow_filter_not_dvd line 541