OAI/NumberTheory/CubicMoment/Estimates/ScaleFirstGeometry.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

On the manuscript's scale-first high branch, every actual prime is below X^(131/200) up to a fixed constant. This is still strictly below the two-thirds barrier needed by the proved grouping alternative.

  1. lemma OAI.CubicFirstMoment.uncutPrimeTupleTerm_factors_ne_zero line 12
  2. lemma OAI.CubicFirstMoment.uncutPrimeTupleTerm_product_range line 22
  3. lemma OAI.CubicFirstMoment.uncutPrimeTupleNorm_rough line 29
  4. lemma OAI.CubicFirstMoment.uncutPrimeTupleNorm_high_upper line 51
  5. lemma OAI.CubicFirstMoment.uncutPrimeTuple_high_exponents line 89