OAI/NumberTheory/CubicGauss/ScalarBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Scalar exponent inequalities for cubic-sieve recurrences.

  1. lemma OAI.CubicFirstMoment.SieveScalar.monomial line 14
  2. lemma OAI.CubicFirstMoment.SieveScalar.main_power line 23
  3. lemma OAI.CubicFirstMoment.SieveScalar.mixed_one line 44
  4. lemma OAI.CubicFirstMoment.SieveScalar.mixed_two line 67
  5. lemma OAI.CubicFirstMoment.SieveScalar.scale_epsilon line 87