OAI/NumberTheory/DirichletL/PrimeCounting/RayAsymptotic.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.PNT.RayAsymptotic.classCoeff line 15
  2. theorem OAI.SevenEighths.PNT.RayAsymptotic.sum_coeff line 17
  3. theorem OAI.SevenEighths.PNT.RayAsymptotic.average_coeff line 31
  4. theorem OAI.SevenEighths.PNT.RayAsymptotic.classCoeff_LSeries line 39
  5. def OAI.SevenEighths.PNT.RayAsymptotic.principalRegularization line 53
  6. theorem OAI.SevenEighths.PNT.RayAsymptotic.principalRegularization_eventuallyEq line 57
  7. theorem OAI.SevenEighths.PNT.RayAsymptotic.principalRegularization_analyticAt line 64
  8. theorem OAI.SevenEighths.PNT.RayAsymptotic.principalRegularization_analyticAt_of_local line 72
  9. theorem OAI.SevenEighths.PNT.RayAsymptotic.principalRegularization_logDeriv line 85
  10. def OAI.SevenEighths.PNT.RayAsymptotic.regularizedFamily line 95
  11. def OAI.SevenEighths.PNT.RayAsymptotic.remainder line 99
  12. structure OAI.SevenEighths.PNT.RayAsymptotic.AnalyticFamily line 104
  13. theorem OAI.SevenEighths.PNT.RayAsymptotic.regularizedFamily_analyticAt line 114
  14. theorem OAI.SevenEighths.PNT.RayAsymptotic.regularizedFamily_ne_zero line 127
  15. theorem OAI.SevenEighths.PNT.RayAsymptotic.remainder_continuousOn line 141
  16. theorem OAI.SevenEighths.PNT.RayAsymptotic.regularizedFamily_logDeriv line 152
  17. theorem OAI.SevenEighths.PNT.RayAsymptotic.remainder_eqOn line 163
  18. theorem OAI.SevenEighths.PNT.RayAsymptotic.classCoeff_ratio_tendsto line 184
  19. def OAI.SevenEighths.PNT.RayAsymptotic.quotientClassCoeff line 199
  20. theorem OAI.SevenEighths.PNT.RayAsymptotic.quotient_sum_coeff line 201
  21. theorem OAI.SevenEighths.PNT.RayAsymptotic.quotient_average_coeff line 216
  22. theorem OAI.SevenEighths.PNT.RayAsymptotic.quotientClassCoeff_LSeries line 226
  23. def OAI.SevenEighths.PNT.RayAsymptotic.quotientRemainder line 242
  24. theorem OAI.SevenEighths.PNT.RayAsymptotic.quotientRemainder_continuousOn line 248
  25. theorem OAI.SevenEighths.PNT.RayAsymptotic.quotientRemainder_eqOn line 260
  26. theorem OAI.SevenEighths.PNT.RayAsymptotic.quotientClassCoeff_ratio_tendsto line 286