OAI/NumberTheory/CubicMoment/Estimates/IdealPrimeReplacement.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact separation of prime ideals from higher prime powers in the actual von Mangoldt prefix.

  1. def OAI.CubicFirstMoment.idealPrimeChebyshev line 12
  2. lemma OAI.CubicFirstMoment.idealVonMangoldt_single_prime line 16
  3. lemma OAI.CubicFirstMoment.idealVonMangoldt_support line 21
  4. lemma OAI.CubicFirstMoment.single_prime_ne_higher line 30
  5. theorem OAI.CubicFirstMoment.idealMangoldtSum_sub_prime line 41
  6. theorem OAI.CubicFirstMoment.idealMangoldt_prime_replacement_bound line 69