OAI/NumberTheory/CubicMoment/Angular/AngularDyadicNoncubeMoment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Fixed norm dyads in the actual noncube estimate. Their factor of two is absorbed by a strictly smaller exponent neighborhood.

  1. theorem OAI.CubicFirstMoment.angular_dyadic_full_noncube line 16