OAI/NumberTheory/DirichletL/PrimeCounting/AnnularPrimeMass.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.PNT.AnnularPrimeMass.cumulative line 16
  2. def OAI.SevenEighths.PNT.AnnularPrimeMass.scaledCumulative line 18
  3. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.cumulative_ratio_tendsto line 20
  4. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.scaledCumulative_tendsto line 34
  5. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.cumulative_nonneg line 45
  6. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.scaledCumulative_bound line 48
  7. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.measurable_cumulative line 67
  8. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.measurable_scaledCumulative line 70
  9. def OAI.SevenEighths.PNT.AnnularPrimeMass.annularSum line 74
  10. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.annularSum_div_eq_integral line 77
  11. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.integral_scaledCumulative_tendsto line 119
  12. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.annularSum_div_tendsto line 138
  13. def OAI.SevenEighths.PNT.AnnularPrimeMass.annularPrimeIdeals line 161
  14. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.mem_annularPrimeIdeals line 164
  15. def OAI.SevenEighths.PNT.AnnularPrimeMass.primeAnnularSum line 170
  16. def OAI.SevenEighths.PNT.AnnularPrimeMass.primeLogAnnularSum line 173
  17. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.primeLogAnnularSum_eq line 176
  18. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.primeClassCoeff_chebyshev line 198
  19. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.primeLogAnnularSum_div_tendsto line 210
  20. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.norm_bounds_of_mem_annularPrimeIdeals line 221
  21. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.ratio_mem_of_mem_annularPrimeIdeals line 229
  22. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.log_norm_difference_bound line 236
  23. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.annularPrime_card_div_bound line 250
  24. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.primeAnnularSum_log_error_bound line 284
  25. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.primeAnnularSum_log_error_tendsto line 316
  26. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.primeAnnularSum_log_div_tendsto line 335
  27. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.contDiff_powerWeight line 345
  28. def OAI.SevenEighths.PNT.AnnularPrimeMass.weightedPrimeAnnularSum line 360
  29. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.weightedPrimeAnnularSum_normalization line 364
  30. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.weightedPrimeAnnularSum_tendsto line 385
  31. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.weightedPrimeAnnularSum_nat_tendsto line 411
  32. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.exists_positive_support_annulus line 419
  33. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.mem_annularPrimeIdeals_of_weight_ne_zero line 437
  34. def OAI.SevenEighths.PNT.AnnularPrimeMass.primeWeightTerm line 452
  35. def OAI.SevenEighths.PNT.AnnularPrimeMass.weightedPrimeSum line 455
  36. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.primeWeightTerm_support_subset line 458
  37. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.primeWeightTerm_hasFiniteSupport line 470
  38. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.weightedPrimeSum_eq_annular line 477
  39. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.weightedPrimeSum_tendsto line 488
  40. def OAI.SevenEighths.PNT.AnnularPrimeMass.weightedPrimeSumDeleted line 499
  41. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.finite_prime_weights_eventually_zero line 503
  42. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.fixed_prime_deletion_eventually_eq line 517
  43. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.finite_prime_deleted_mass_eventually_zero line 528
  44. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.weightedPrimeSumDeleted_tendsto line 534
  45. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.weightedPrimeSumDeleted_eq_annular line 544
  46. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.powerWeight_integral_pos line 565
  47. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.weightedPrimeSumDeleted_eventually_lower_bound line 584
  48. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.weightedPrimeSumDeleted_eventually_pos line 605
  49. theorem OAI.SevenEighths.PNT.AnnularPrimeMass.weightedPrimeSum_nat_tendsto line 617