OAI/NumberTheory/CubicMoment/Estimates/DyadicNoncubeMoment.lean

GitHub source file

3 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. lemma OAI.CubicFirstMoment.shifted_distance_bound line 14
  2. lemma OAI.CubicFirstMoment.noncube_dyadic_shift_absorption line 28
  3. theorem OAI.CubicFirstMoment.dyadic_full_noncube line 46