OAI/NumberTheory/CubicMoment/Estimates/TwistedSmoothBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The application-sized primitive cubic moment, with the fixed logarithmic losses absorbed into an arbitrary positive power.

  1. theorem OAI.CubicFirstMoment.full_smooth_twisted_primitive_cubic_bound line 14