OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/Core.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryAnalyticCentering.core line 27
  2. def OAI.OrdinaryAnalyticCentering.center line 30
  3. def OAI.OrdinaryAnalyticCentering.A line 33
  4. def OAI.OrdinaryAnalyticCentering.Pā‚€ line 34
  5. def OAI.OrdinaryAnalyticCentering.J line 35
  6. def OAI.OrdinaryAnalyticCentering.coreMean line 36
  7. def OAI.OrdinaryAnalyticCentering.Lā‚€ line 37
  8. def OAI.OrdinaryAnalyticCentering.cut line 39
  9. def OAI.OrdinaryAnalyticCentering.divisorWeight line 41
  10. def OAI.OrdinaryAnalyticCentering.kernel line 43
  11. def OAI.OrdinaryAnalyticCentering.rawSum line 47
  12. def OAI.OrdinaryAnalyticCentering.centeredSum line 51
  13. def OAI.OrdinaryAnalyticCentering.Admissible line 54