OAI/NumberTheory/CubicMoment/Estimates/LargeTupleSupport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual support geometry of the large distinguished rows. Every prime is rough, and the complementary primes inherit the X^(31/50) bound from the original large distinguished product.

  1. lemma OAI.CubicFirstMoment.largePrimeTupleTerm_membership line 14
  2. lemma OAI.CubicFirstMoment.largePrimeTupleTerm_factors_ne_zero line 27
  3. lemma OAI.CubicFirstMoment.largePrimeTupleTerm_product_range line 39
  4. lemma OAI.CubicFirstMoment.largePrimeTupleNorm_rough_bound line 46
  5. lemma OAI.CubicFirstMoment.largePrimeTupleNorm_upper_bound line 68