OAI/NumberTheory/CubicMoment/Estimates/LargeTupleExponents.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Normalized logarithmic prime sizes in the actual large-row support. They form a positive partition of one uniformly away from two thirds.

  1. def OAI.CubicFirstMoment.largePrimeTupleProduct line 13
  2. def OAI.CubicFirstMoment.largePrimeTupleExponent line 17
  3. lemma OAI.CubicFirstMoment.largePrimeTupleNorm_prod line 21
  4. lemma OAI.CubicFirstMoment.largePrimeTupleExponent_sum line 28
  5. lemma OAI.CubicFirstMoment.largePrimeTupleExponent_bounds line 39