OAI/NumberTheory/PrimeGaps/Profiles.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargePrimeGaps.weightedMarkedError line 9
  2. theorem OAI.LargePrimeGaps.dyadic_theta_error_le_markedError_one line 14
  3. theorem OAI.LargePrimeGaps.dyadic_theta_error_le_weightedMarkedError line 22
  4. def OAI.LargePrimeGaps.reciprocalBump line 38
  5. def OAI.LargePrimeGaps.reciprocalProfile line 45
  6. theorem OAI.LargePrimeGaps.reciprocalBump_eq_zero_left line 48
  7. theorem OAI.LargePrimeGaps.reciprocalBump_eq_zero_right line 55
  8. theorem OAI.LargePrimeGaps.reciprocalProfile_zero_left line 62
  9. theorem OAI.LargePrimeGaps.reciprocalProfile_zero_right line 66
  10. theorem OAI.LargePrimeGaps.reciprocalProfile_eq_inv line 70
  11. theorem OAI.LargePrimeGaps.reciprocalProfile_nonneg line 79
  12. theorem OAI.LargePrimeGaps.reciprocalProfile_smooth line 85
  13. theorem OAI.LargePrimeGaps.reciprocalProfile_compact line 96
  14. theorem OAI.LargePrimeGaps.reciprocalProfile_tsupport line 102
  15. theorem OAI.LargePrimeGaps.reciprocalProfile_integrable line 112
  16. theorem OAI.LargePrimeGaps.reciprocalProfile_sq_integrable line 117
  17. theorem OAI.LargePrimeGaps.reciprocalProfile_moment_integrable line 122
  18. theorem OAI.LargePrimeGaps.reciprocalProfile_mass_lower line 128
  19. theorem OAI.LargePrimeGaps.reciprocalProfile_sq_mass_pos line 141
  20. theorem OAI.LargePrimeGaps.reciprocalProfile_moment_upper line 149
  21. theorem OAI.LargePrimeGaps.exists_normalized_reciprocal_profile line 187
  22. theorem OAI.LargePrimeGaps.exists_small_first_moment_profile line 265
  23. def OAI.LargePrimeGaps.scaledProfileDensity line 298
  24. def OAI.LargePrimeGaps.productProfile line 301
  25. def OAI.LargePrimeGaps.productDensity line 304
  26. def OAI.LargePrimeGaps.coordinateSum line 307
  27. theorem OAI.LargePrimeGaps.productProfile_sq line 309
  28. theorem OAI.LargePrimeGaps.scaledProfileDensity_integral line 315
  29. theorem OAI.LargePrimeGaps.scaledProfileDensity_moment line 322
  30. theorem OAI.LargePrimeGaps.productDensity_integral line 335
  31. theorem OAI.LargePrimeGaps.productDensity_nonneg line 339
  32. theorem OAI.LargePrimeGaps.coordinate_mul_productDensity line 343
  33. theorem OAI.LargePrimeGaps.coordinate_productDensity_integrable line 349
  34. theorem OAI.LargePrimeGaps.coordinate_productDensity_integral line 363
  35. theorem OAI.LargePrimeGaps.coordinateSum_productDensity_integrable line 380
  36. theorem OAI.LargePrimeGaps.coordinateSum_productDensity_integral line 386
  37. theorem OAI.LargePrimeGaps.productDensity_ne_zero_coordinates line 395
  38. theorem OAI.LargePrimeGaps.productDensity_ne_zero_sum_nonneg line 401
  39. theorem OAI.LargePrimeGaps.productDensity_compact line 406
  40. theorem OAI.LargePrimeGaps.productDensity_continuous line 413
  41. theorem OAI.LargePrimeGaps.productDensity_integrable line 418
  42. theorem OAI.LargePrimeGaps.poly_productDensity_integrable line 422
  43. theorem OAI.LargePrimeGaps.one_coordinate_productDensity line 428
  44. theorem OAI.LargePrimeGaps.two_coordinate_productDensity line 435
  45. theorem OAI.LargePrimeGaps.one_coordinate_productDensity_integral line 449
  46. theorem OAI.LargePrimeGaps.two_coordinate_productDensity_integral line 464