OAI/NumberTheory/CubicMoment/Estimates/LargeTupleResidualPartition.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

An exact partition of the remaining large tuples. A boundary box retains its sharp distinguished-product cutoff; an exceptional high box has no surviving ordinary tuple. No contribution is discarded.

  1. def OAI.CubicFirstMoment.largePrimeTupleBoundarySum line 13
  2. def OAI.CubicFirstMoment.largePrimeTupleExceptionalHighSum line 19
  3. lemma OAI.CubicFirstMoment.largePrimeTuplePiece_low_zero line 27
  4. theorem OAI.CubicFirstMoment.distinguishedPrimeTupleLow_residual_partition line 35