OAI/NumberTheory/CubicMoment/Estimates/LargeTupleFullSupport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

High boxes are literal full independent prime sums. The original finite prime cutoff is removed only after the coordinate support bounds show that all nonzero weights fit inside it.

  1. def OAI.CubicFirstMoment.largeTupleVector line 16
  2. lemma OAI.CubicFirstMoment.largeTupleVector_prod line 19
  3. lemma OAI.CubicFirstMoment.largeTupleVector_norm line 24
  4. lemma OAI.CubicFirstMoment.largeTupleVector_split line 28
  5. lemma OAI.CubicFirstMoment.largeTuple_coordinate_support line 33
  6. def OAI.CubicFirstMoment.largeTupleIndependentSum line 50
  7. theorem OAI.CubicFirstMoment.largePrimeTuplePiece_high_full line 57