OAI/NumberTheory/CubicMoment/Angular/AngularLongDistinguishedSaving.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.angular_long_distinguished_prime_excluded_bound line 18
  2. theorem OAI.CubicFirstMoment.angular_long_distinguished_prime_saving line 59