OAI/NumberTheory/CubicMoment/Estimates/IdealMangoldtDyadic.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact sharp dyadic ideal sums and the two endpoint errors of the logarithmic smooth cutoff. All ideals, including those above three, remain.

  1. def OAI.CubicFirstMoment.idealMangoldtDyadic line 15
  2. lemma OAI.CubicFirstMoment.idealMangoldtDyadic_eq_sum line 19
  3. lemma OAI.CubicFirstMoment.idealMangoldtSmooth_dyadic_eq_sum line 34
  4. theorem OAI.CubicFirstMoment.idealMangoldt_dyadic_smoothing_error line 48