OAI/NumberTheory/CubicMoment/Estimates/TailPrimeGeometry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

All coordinate assumptions for the independent Gauss-tail prime box follow from one surviving original tuple.

  1. theorem OAI.CubicFirstMoment.tailPrimeTuplePiece_rough_scales line 13
  2. lemma OAI.CubicFirstMoment.tailPrimeTuplePiece_witness line 44
  3. theorem OAI.CubicFirstMoment.eventually_tailPrimeTuple_coordinate_envelope line 55
  4. theorem OAI.CubicFirstMoment.eventually_tailPrimeTuplePiece_full line 74