OAI/NumberTheory/DirichletL/PrimeLogProfile.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.PrimeLogProfile.safeInverse line 10
  2. theorem OAI.SevenEighths.PrimeLogProfile.safeInverse_eq line 13
  3. theorem OAI.SevenEighths.PrimeLogProfile.safeInverse_smooth line 22
  4. def OAI.SevenEighths.PrimeLogProfile.profile line 45
  5. theorem OAI.SevenEighths.PrimeLogProfile.profile_support line 48
  6. theorem OAI.SevenEighths.PrimeLogProfile.profile_smooth line 53
  7. def OAI.SevenEighths.PrimeLogProfile.logFamily line 71
  8. theorem OAI.SevenEighths.PrimeLogProfile.logFamily_smooth line 74
  9. theorem OAI.SevenEighths.PrimeLogProfile.logFamily_eq line 83
  10. theorem OAI.SevenEighths.PrimeLogProfile.logFamily_support line 89
  11. theorem OAI.SevenEighths.PrimeLogProfile.uniform_mellin_decay line 98
  12. theorem OAI.SevenEighths.PrimeLogProfile.profile_eq_log_division line 129