OAI/NumberTheory/CubicMoment/Angular/AngularSmallConductorLogSaving.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The part of the small-conductor range above a fixed logarithmic power has arbitrary logarithmic saving, without any roughness or height restriction. All coefficients remain the actual prime convolution.

  1. theorem OAI.CubicFirstMoment.angular_small_conductor_log_saving line 15