OAI/NumberTheory/CubicMoment/Estimates/IdealPrimePowerError.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The exact prime-power deletion error has the classical square-root size with two logarithms.

  1. def OAI.CubicFirstMoment.idealPrimePowerErrorConstant line 11
  2. lemma OAI.CubicFirstMoment.idealPrimePowerErrorConstant_pos line 13
  3. lemma OAI.CubicFirstMoment.idealPrimePower_log_count line 18
  4. theorem OAI.CubicFirstMoment.idealMangoldt_prime_replacement_log_bound line 36