OAI/NumberTheory/CubicMoment/Estimates/PrimeLogReplacement.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Exact replacement of a prime indicator by von Mangoldt divided by log norm. The discrepancy is bounded and is supported on actual higher primary prime powers.

  1. def OAI.CubicFirstMoment.normalizedVonMangoldt line 12
  2. def OAI.CubicFirstMoment.primeIndicator line 15
  3. def OAI.CubicFirstMoment.primeLogCorrection line 17
  4. lemma OAI.CubicFirstMoment.prime_norm_gt_one line 20
  5. lemma OAI.CubicFirstMoment.normalizedVonMangoldt_at_prime line 26
  6. lemma OAI.CubicFirstMoment.normalizedVonMangoldt_nonneg line 31
  7. lemma OAI.CubicFirstMoment.normalizedVonMangoldt_le_one line 36
  8. lemma OAI.CubicFirstMoment.primeLogCorrection_at_prime line 47
  9. lemma OAI.CubicFirstMoment.primeLogCorrection_bounds line 52
  10. lemma OAI.CubicFirstMoment.primeIndicator_eq_normalized_sub_correction line 60
  11. lemma OAI.CubicFirstMoment.primeLogCorrection_support line 65
  12. lemma OAI.CubicFirstMoment.primeLogCorrection_mem_largePrimePowerSupport line 76