OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/CorePrime.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.OrdinaryAnalyticCentering.core_prime line 28
  2. lemma OAI.OrdinaryAnalyticCentering.center_prime line 29
  3. lemma OAI.OrdinaryAnalyticCentering.core_center_disjoint line 30
  4. lemma OAI.OrdinaryAnalyticCentering.prime_lower line 34
  5. def OAI.OrdinaryAnalyticCentering.centralPrimes line 46
  6. def OAI.OrdinaryAnalyticCentering.corePrimes line 47
  7. def OAI.OrdinaryAnalyticCentering.retained line 48
  8. def OAI.OrdinaryAnalyticCentering.removed line 49
  9. def OAI.OrdinaryAnalyticCentering.choices line 50
  10. lemma OAI.OrdinaryAnalyticCentering.mem_choices line 53
  11. lemma OAI.OrdinaryAnalyticCentering.centralPrimes_subset line 57
  12. lemma OAI.OrdinaryAnalyticCentering.corePrimes_subset line 61
  13. lemma OAI.OrdinaryAnalyticCentering.parts_union line 65
  14. lemma OAI.OrdinaryAnalyticCentering.parts_disjoint line 73
  15. lemma OAI.OrdinaryAnalyticCentering.retained_pos line 75
  16. lemma OAI.OrdinaryAnalyticCentering.retained_factors line 79
  17. lemma OAI.OrdinaryAnalyticCentering.removed_factors line 83
  18. lemma OAI.OrdinaryAnalyticCentering.retained_mul_removed line 85
  19. lemma OAI.OrdinaryAnalyticCentering.retained_core line 88
  20. lemma OAI.OrdinaryAnalyticCentering.retained_omitted line 106
  21. lemma OAI.OrdinaryAnalyticCentering.retained_weight line 113
  22. lemma OAI.OrdinaryAnalyticCentering.cut_dilation line 119
  23. lemma OAI.OrdinaryAnalyticCentering.prod_prime_indicator line 128
  24. lemma OAI.OrdinaryAnalyticCentering.centered_product line 140
  25. lemma OAI.OrdinaryAnalyticCentering.kernel_expansion line 154