OAI/NumberTheory/CubicMoment/Estimates/PrimeSmoothingScale.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Choosing a cutoff width after its finite derivative order is known. The same exponential saving absorbs the cutoff cost and the contour tail.

  1. def OAI.CubicFirstMoment.primeSmoothingRate line 10
  2. def OAI.CubicFirstMoment.primeSmoothingParameter line 11
  3. lemma OAI.CubicFirstMoment.primeSmoothingRate_pos line 14
  4. lemma OAI.CubicFirstMoment.primeSmoothingRate_bounds line 18
  5. lemma OAI.CubicFirstMoment.primeContour_ratio_bounds line 36
  6. lemma OAI.CubicFirstMoment.primeSmoothingParameter_ge_one line 49
  7. lemma OAI.CubicFirstMoment.primeSmoothing_absorbs_shift line 54
  8. lemma OAI.CubicFirstMoment.primeSmoothing_absorbs_tail line 66
  9. lemma OAI.CubicFirstMoment.primeSmoothing_absorbs_sqrt line 80
  10. lemma OAI.CubicFirstMoment.primeSmoothing_inverse line 98