OAI/NumberTheory/CubicMoment/Estimates/LongDistinguishedSaving.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exclusion and arbitrary logarithmic saving for the actual smooth weight of a distinguished free prime. The bounds retain the derivative cost and are uniform in the two detector scales.

  1. theorem OAI.CubicFirstMoment.long_distinguished_prime_excluded_bound line 16
  2. theorem OAI.CubicFirstMoment.long_distinguished_prime_saving line 56