OAI/NumberTheory/CubicMoment/Angular/AngularFullSmoothFactor.lean

GitHub source file

7 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.primaryAngularShortSmoothSum line 14
  2. lemma OAI.CubicFirstMoment.primaryAngularShortSmoothSum_eq_polynomial line 21
  3. lemma OAI.CubicFirstMoment.primaryAngularShortSmoothSum_zeta line 34
  4. lemma OAI.CubicFirstMoment.primaryAngularShortSmoothSum_log line 40
  5. lemma OAI.CubicFirstMoment.primaryAngularShortSmoothSum_moebius line 51
  6. lemma OAI.CubicFirstMoment.primaryAngularShortSmoothSum_classify line 73
  7. theorem OAI.CubicFirstMoment.first_angular_short_full_smooth_partition_power line 85