OAI/NumberTheory/CubicMoment/Angular/AngularLargeCorePolynomialHeight.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite large-core contribution has every logarithmic saving throughout the fixed polynomial height window required by Mellin truncation.

  1. theorem OAI.CubicFirstMoment.angular_large_core_cutoff_polynomial_height line 17