OAI/NumberTheory/CubicMoment/Estimates/PrimeIndicatorPowers.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The elementary power margins used to return from a global cutoff at 2Y to the original exceptional conductor neighborhoods.

  1. lemma OAI.CubicFirstMoment.twice_rpow_le_mul_rpow line 11
  2. lemma OAI.CubicFirstMoment.first_prime_error_rows line 19
  3. lemma OAI.CubicFirstMoment.balanced_prime_error_rows line 30
  4. lemma OAI.CubicFirstMoment.absorb_prime_coordinate_error line 41