OAI/NumberTheory/CubicMoment/Angular/AngularRoughNoncubeLowHeight.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

At low height the cube part of an arbitrary noncube frequency is removed exactly and charged to the proved excluded-prime estimate.

  1. theorem OAI.CubicFirstMoment.angular_rough_noncube_low_height line 15