OAI/NumberTheory/CubicMoment/Estimates/FullSmoothFactor.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact classification of the full smooth factors from the short inverse. The short Möbius alternative vanishes once the dyad lies above its support.

  1. def OAI.CubicFirstMoment.primaryShortSmoothSum line 13
  2. lemma OAI.CubicFirstMoment.primaryShortSmoothSum_eq_polynomial line 20
  3. lemma OAI.CubicFirstMoment.primaryShortSmoothSum_zeta line 33
  4. lemma OAI.CubicFirstMoment.primaryShortSmoothSum_log line 39
  5. lemma OAI.CubicFirstMoment.primaryShortSmoothSum_moebius line 50
  6. lemma OAI.CubicFirstMoment.primaryShortSmoothSum_classify line 72
  7. lemma OAI.CubicFirstMoment.full_dyad_above_sqrt line 84
  8. theorem OAI.CubicFirstMoment.first_short_full_smooth_partition_power line 98