OAI/NumberTheory/CubicMoment/Estimates/LargeTupleExceptionalHigh.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The remaining high exceptional boxes split exactly into the flat subfamily and its complement. Both are negligible on the stated scale.

  1. def OAI.CubicFirstMoment.largeTupleExceptionalSelector line 15
  2. def OAI.CubicFirstMoment.largePrimeTupleExceptionalNonflatSum line 21
  3. lemma OAI.CubicFirstMoment.largePrimeTupleExceptionalHigh_split line 28
  4. theorem OAI.CubicFirstMoment.largePrimeTupleExceptionalHighSum_isLittleO line 61
  5. lemma OAI.CubicFirstMoment.largePrimeTupleExceptionalHighSum_zero line 123