OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/PrimeWeight.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryAnalyticCentering.primeWeight line 27
  2. lemma OAI.OrdinaryAnalyticCentering.primeWeight_nonneg line 28
  3. lemma OAI.OrdinaryAnalyticCentering.divisorWeight_pos line 32
  4. lemma OAI.OrdinaryAnalyticCentering.count_by_primeFactors line 34
  5. lemma OAI.OrdinaryAnalyticCentering.product_primeWeight line 43
  6. lemma OAI.OrdinaryAnalyticCentering.euler_product line 56
  7. lemma OAI.OrdinaryAnalyticCentering.retained_mass line 70
  8. lemma OAI.OrdinaryAnalyticCentering.Lā‚€_nonneg line 90