OAI/NumberTheory/CubicMoment/Estimates/RoughKummerLowHeight.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The full nonprincipal rough-prime convolution at low height, with the numerator measured at the actual full length, including its ramified and unit factors. All prime and squarefree restrictions remain in the conclusion.

  1. theorem OAI.CubicFirstMoment.rough_kummer_low_height line 15