OAI/NumberTheory/CubicMoment/Estimates/LargeTuplePartition.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite smooth norm partition of the literal large-row prime tuples. Every original support condition stays inside each summand.

  1. def OAI.CubicFirstMoment.largePrimeTupleBox line 14
  2. def OAI.CubicFirstMoment.largePrimeTupleTerm line 19
  3. def OAI.CubicFirstMoment.largePrimeTupleNorm line 32
  4. lemma OAI.CubicFirstMoment.largePrimeTupleNorm_bounds line 36
  5. lemma OAI.CubicFirstMoment.distinguishedPrimeTupleLow_eq_sum line 48
  6. def OAI.CubicFirstMoment.largePrimeTuplePiece line 56
  7. theorem OAI.CubicFirstMoment.distinguishedPrimeTupleLow_partition line 62