OAI/NumberTheory/CubicMoment/Estimates/PrimeCoordinateErrors.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Actual prime-indicator replacement errors in the two exceptional regions.

  1. def OAI.CubicFirstMoment.primeCoordinateError line 12
  2. theorem OAI.CubicFirstMoment.first_primeCoordinateError_moment line 19
  3. theorem OAI.CubicFirstMoment.balanced_primeCoordinateError_moment line 56