OAI/NumberTheory/CubicMoment/Estimates/PrimeErrorPointwise.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A pointwise power saving for the actual repeated-prime error. This allows low-height character estimates to pass from independent prime products to their squarefree restriction.

  1. lemma OAI.CubicFirstMoment.twistedErrorPrimePolynomial_pointwise_sq line 15
  2. theorem OAI.CubicFirstMoment.primeConvolutionError_cutoff_bound line 35
  3. theorem OAI.CubicFirstMoment.primeConvolutionError_pointwise_bound line 76